TY - CHAP
T1 - Playing games with boxes and diamonds
AU - Alur, Rajeev
AU - La Torre, Salvatore
AU - Madhusudan, P.
PY - 2003
Y1 - 2003
N2 - 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. The previously known hardness proofs encode Turing machine computations using the next and/or until operators. Furthermore, in the case of model checking, disallowing next and until, and retaining only the always and eventually operators, lowers the complexity from PSPACE to NP. Whether such a reduction in complexity is possible for deciding games has been an open problem. In this paper, we provide a negative answer to this question. We introduce new techniques for encoding Turing machine computations using games, and show that deciding games for the LTL fragment with only the always and eventually operators is 2EXPTIME-hard. We also prove- that if in this fragment we do not allow the eventually operator in the scope of the always operator and vice-versa, deciding games is EXPSPACE-hard, matching the previously known upper bound. On the positive side, we show that 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 in PSPACE, and also establish a matching lower bound. Such conditions include safety and reachability specifications on game graphs augmented with fairness conditions for the two players.
AB - 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. The previously known hardness proofs encode Turing machine computations using the next and/or until operators. Furthermore, in the case of model checking, disallowing next and until, and retaining only the always and eventually operators, lowers the complexity from PSPACE to NP. Whether such a reduction in complexity is possible for deciding games has been an open problem. In this paper, we provide a negative answer to this question. We introduce new techniques for encoding Turing machine computations using games, and show that deciding games for the LTL fragment with only the always and eventually operators is 2EXPTIME-hard. We also prove- that if in this fragment we do not allow the eventually operator in the scope of the always operator and vice-versa, deciding games is EXPSPACE-hard, matching the previously known upper bound. On the positive side, we show that 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 in PSPACE, and also establish a matching lower bound. Such conditions include safety and reachability specifications on game graphs augmented with fairness conditions for the two players.
UR - http://www.scopus.com/inward/record.url?scp=35248822590&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35248822590&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-45187-7_8
DO - 10.1007/978-3-540-45187-7_8
M3 - Chapter
AN - SCOPUS:35248822590
SN - 3540407537
SN - 9783540407539
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 128
EP - 143
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Amadio, Roberto
A2 - Lugiez, Denis
PB - Springer
ER -