We prove two tight bounds on complexity of deciding graph games with winning conditions defined by formulas from fragments of LTL. Our first result is that deciding LTL_+ (◇, ∧, ∨) games is in PSPACE. This is a tight bound: the problem is known to be PSPACE-hard even for the much weaker logic LTL_+(◇, ∧). We use a method based on a notion of, as we call it, persistent strategy: we prove that in games with positive winning condition the opponent has a winning strategy if and only if he has a persistent winning strategy. The best upper bound one can prove for our problem with the Buechi automata technique, is EXPSPACE. This means that we identify a natural fragment of LTL for which the algorithm resulting from the Biichi automata tool is one exponent worse than optimal. As our second result we show that the problem is EXPSPACE-hard if the winning condition is from the logic LTL_+(◇, ○, ∧, ∨). This solves an open problem from [AT01], where the authors use the Biichi automata technique to show an EXPSPACE algorithm deciding more general LTL(◇, ○, ∧, ∨) games, but do not prove optimality of this upper bound.
展开▼
