## Deterministic Generators and Games for LTL Fragments

*Rajeev Alur and Salvatore La Torre*
Deciding infinite two-player games on finite graphs with the winning condition
specified by a linear temporal logic (LTL) formula, is known to
be 2Exptime-complete. In this paper, we identify LTL fragments of lower
complexity. Solving LTL games typically involves
a doubly-exponential translation from
LTL formulas to *deterministic* omega-automata.
First, we show that the *longest distance* (length of the longest
simple path) of the generator is also an important parameter, by
giving an O(d log n)-space procedure to solve a Buchi game on a
graph with n vertices and longest distance d.
Then, for the LTL fragment with only eventualities and conjunctions,
we provide a translation to deterministic generators of exponential size and
linear longest distance, show both of these bounds to be optimal, and prove
the corresponding games to be Pspace-complete.
Introducing *next* modalities in this fragment,
we provide a translation to deterministic
generators still of exponential size but
also with exponential longest distance, show both of these bounds to be
optimal, and prove
the corresponding games to be Exptime-complete.
For the fragment resulting by further adding disjunctions,
we provide a translation to deterministic generators of doubly-exponential
size and exponential longest distance, show both of these bounds to be
optimal, and prove the corresponding games to be Expspace.
Finally, we show tightness of the double-exponential
bound on the size as well as the longest distance
for deterministic generators for LTL even in the absence of *next*
and *until* modalities.

*16th IEEE Symposium on Logic in Computer Science*
(LICS'01), 2001.