Optimal Complexity Bounds for Positive LTL

Abstract. 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+(3,∧,∨) games is in PSPACE. This is a tight bound: the problem is known to be PSPACE-hard even for the much weaker logic LTL+(3,∧). 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 Büchi automata technique, is EXPSPACE. This means that we identify a nat-ural fragment of LTL for which the algorithm resulting from the Büchi 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+(3, d,∧,∨). This solves an open problem from [AT01], where the authors use the Büchi au-tomata technique to show an EXPSPACE algorithm deciding more gen-eral LTL(3, d,∧,∨) games, but do not prove optimality of this upper bound