Deciding Games in LTL Fragments

Salvatore la Torre
Dipartimento di Informatica ed Applicazioni, Università degli Studi di Salerno, Italy
Friday, 19 March, 2004 (All day)
NO

Pnueli and Rosner showed that deciding two-player games over finite graphs with winning conditions specified as an LTL formula is 2EXPTIME-complete. Recent papers have shown the complexity bounds for this decision problem in various fragments of LTL. In this talk, we will survey on these results.

A surprising result is that disallowing next and until, and retaining only the always and eventually operators in the specifications, deciding LTL games is still 2EXPTIME-hard. This clearly contrasts with the complexity bounds of model checking that is NP-complete for this fragment while is PSPACE-complete in the general case. To achieve this result new techniques for encoding Turing machine computations using games are introduced.

The complexity can be reduced to EXPSPACE-complete, disallowing in this fragment the always in the scope of the eventually operator and vice-versa. Note that the complexity stays unchanged if the next operator is added. Also, it is interesting that if the only temporal operator is either the always or the eventually operator, and Boolean negation is allowed only at the level of the atomic propositions, deciding games becomes PSPACE-complete. Thus the Boolean closure of such specifications causes the complexity to raise from PSPACE-complete to EXPSPACE-complete.

Finally, if the winning condition is a Boolean combination of formulas of the form ``eventually p'' and ``infinitely often p'', for a state-formula p, then the game can be decided still in PSPACE, and also a matching lower bound is established. Such conditions include safety and reachability specifications on game graphs augmented with fairness conditions for the two players.