Complexity Bounds for Regular Games
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.
KeywordsModel Check Condition Type Complexity Bound Winning Strategy Truth Assignment
Unable to display preview. Download preview PDF.
- 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.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.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
- 8.McNaughton, R.: Finite-state infinite games. Technical report, Project MAC, Massachusetts Institute of Technology, USA (1965)Google Scholar