Abstract
We consider the complexity of infinite games played on finite graphs. We establish a framework in which the expressiveness and succinctness of different types of winning conditions can be compared. We show that the problem of deciding the winner in Muller games is PSPACE-complete. This is then used to establish PSPACE-completeness for Emerson-Lei games and for games described by Zielonka DAGs. Adaptations of the proof show PSPACE-completeness for the emptiness problem for Muller automata as well as the model-checking problem for such automata on regular trees. We also show co-NP-completeness for two classes of union-closed games: games specified by a basis and superset Muller games.
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.
References
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295–311 (1969)
Dziembowski, S., Jurdziński, M., Walukiewicz, I.: How much memory is needed to win infinite games? In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pp. 99–110 (1997)
Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs (extended abstract). In: Proceedings for the 29th IEEE Symposium on Foundations of Computer Science, pp. 328–337 (1988)
Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time strikes back. In: Proceedings of the 12th Annual ACM Symposium on Principles of Porgramming Languages, pp. 84–96 (1985)
Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Ishihara, H., Khoussainov, B.: Complexity of some infinite games played on finite graphs. In: Kučera, L. (ed.) WG 2002. LNCS, vol. 2573, pp. 270–281. Springer, Heidelberg (2002)
La Torre, S., Murano, A., Napoli, M.: Weak muller acceptance conditions for tree automata. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 240–254. Springer, Heidelberg (2002)
McNaughton, R.: Finite-state infinite games. Technical report, Project MAC, Massachusetts Institute of Technology, USA (1965)
McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65(2), 149–184 (1993)
Nerode, A., Remmel, J.B., Yakhnis, A.: McNaughton games and extracting strategies for concurrent programs. Annals of Pure and Applied Logic 78(1-3), 203–242 (1996)
Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003)
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
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hunter, P., Dawar, A. (2005). Complexity Bounds for Regular Games. In: Jȩdrzejowicz, J., Szepietowski, A. (eds) Mathematical Foundations of Computer Science 2005. MFCS 2005. Lecture Notes in Computer Science, vol 3618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11549345_43
Download citation
DOI: https://doi.org/10.1007/11549345_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28702-5
Online ISBN: 978-3-540-31867-5
eBook Packages: Computer ScienceComputer Science (R0)