Abstract
We study infinite two-player games over pushdown graphs with a winning condition that refers explicitly to the infinity of the game graph: A play is won by player 0 if some vertex is visited infinity often during the play. We show that the set of winning plays is a proper ∑3-set in the Borel hierarchy, thus transcending the Boolean closure of ∑2-sets which arises with the standard automata theoretic winning conditions (such as the Muller, Rabin, or parity condition). We also show that this ∑3-game over pushdown graphs can be solved effectively (by a computation of the winning region of player 0 and his memoryless winning strategy). This seems to be a first example of an effectively solvable game beyond the second level of the Borel hierarchy.
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
A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, CONCUR’ 97, LNCS 1243, pp 135–150, 1997.
J. R. Büchi, Landweber L.H., Solving sequential conditions by finite-state strategy. Transactions of the American Mathematical Society vol. 138 (1969) 295–311.
J. R. Büchi, State-strategies for games in F σδ ∩ G δσ J. Symbolic Logic 48 (1983), no. 4, 1171–1198.
T. Cachat, Symbolic strategy synthesis for games on pushdown graphs, in: ICALP’02, Springer LNCS (to appear). http://www-i7.informatik.rwth-aachen.de/~cachat/
E. A. Emerson and C. S. Jutla, Tree automata, mu-calculus and determinacy, FoCS’ 91, IEEE Computer Society Press (1991), pp. 368–377.
O. Finkel, Topological properties of omega context-free languages, Theoret. Comput. Sci. 262 (2001), no. 1–2, 669–697.
O. Finkel, Wadge hierarchy of omega context-free languages, Theoret. Comput. Sci. 269 (2001), no. 1–2, 283–315.
J. E. Hopcroft and J. D. Ullman, Formal Languages and their relation to automata, Addison-Wesley, 1969.
A. S. Kechris, Classical descriptive set theory, Graduate texts in mathematics, vol 156, Springer Verlag (1994).
O. Kupferman and M. Y. Vardi, An Automata-Theoretic Approach to Reasoning about Infinite-State Systems, CAV 2000, LNCS 1855, 2000.
S. Seibert, Effektive Strategiekonstruktionen für Gale-Stewart-Spiele auf Transitionsgraphen, Technical Report 9611, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany, July 1996.
C. Stirling, Modal and Temporal Properties of Processes, Springer (Texts in Computer Science), 2001.
W. Thomas, On the synthesis of strategies in infinite games, STACS’ 95, LNCS 900, pp. 1–13, 1995.
W. Thomas, Languages, automata, and logic, in Handbook of Formal Language Theory (G. Rozenberg, A. Salomaa, Eds.), Vol 3, Springer-Verlag, Berlin 1997, pp. 389–455.
W. W. Wadge Reducibility and Determinateness on the Baire Space Ph.D. Thesis, University of California, Berkeley, 1984.
I. Walukiewicz, Pushdown processes: games and model checking, CAV’ 96, LNCS 1102, pp 62–74, 1996. Full version in Information and Computation 157, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cachat, T., Duparc, J., Thomas, W. (2002). Solving Pushdown Games with a ∑3 Winning Condition. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_22
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive