Abstract
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.
Detailed proofs are available at http://www.cis.upenn.edu/ madhusud/
Supported in part by ARO URI award DAAD19-01-1-0473, NSF awards CCR9970925 and ITR/SY 0121431. The second author was also supported by the MIUR grant project “Metodi Formali per la Sicurezza e il Tempo” (MEFISTO) and MIUR grant ex-60% 2002.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Alur, R., de Alfaro, L., Henzinger, T., Mang, F.: Automating modular verification. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 82–97. Springer, Heidelberg (1999)
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 1–42 (2002)
Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. In: Proc. of LICS 2001, pp. 291–302 (2001)
Chandra, A., Kozen, D., Stockmeyer, L.: Alternation. Journal of the ACM 28(1), 114–133 (1981)
Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. Distinguished Dissertation Series. MIT Press, Cambridge (1989)
Emerson, E., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. of FOCS 1988, pp. 328–337 (1988)
Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineeri ng 23(5), 279–295 (1997)
Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Kupferman, O., Vardi, M.: Module checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 75–86. Springer, Heidelberg (1996)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer, Heidelberg (1991)
Marcinkowski, J., Truderung, T.: Optimal complexity bounds for positive ltl games. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 262–275. Springer, Heidelberg (2002)
Pnueli, A.: The temporal logic of programs. In: Proc. of FOCS 1977, pp. 46–77 (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. of POPL 1989, pp. 179–190 (1989)
Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. The Journal of the ACM 32, 733–749 (1985)
Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: Proc. 17th Symp. on Theory of Computing, pp. 240–251 (1985)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., La Torre, S., Madhusudan, P. (2003). Playing Games with Boxes and Diamonds . In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-45187-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40753-9
Online ISBN: 978-3-540-45187-7
eBook Packages: Springer Book Archive