Complexity Bounds for Regular Games

(Extended Abstract)
  • Paul Hunter
  • Anuj Dawar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3618)


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.


Model Check Condition Type Complexity Bound Winning Strategy Truth Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295–311 (1969)MathSciNetGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)zbMATHCrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    McNaughton, R.: Finite-state infinite games. Technical report, Project MAC, Massachusetts Institute of Technology, USA (1965)Google Scholar
  9. 9.
    McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic 65(2), 149–184 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200, 135–183 (1998)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Paul Hunter
    • 1
  • Anuj Dawar
    • 1
  1. 1.University of Cambridge Computer LaboratoryCambridgeUK

Personalised recommendations