Abstract
This paper examines two players’ turn-based perfect-information games played on infinite graphs. Our attention is focused on the classes of games where winning conditions are boolean combinations of the following two conditions: (1) the first one states that an infinite play is won by player 0 if during the play infinitely many different vertices were visited, (2) the second one is the well known parity condition generalized to a countable number of priorities.
We show that, in most cases, both players have positional winning strategies and we characterize their respective winning sets. In the special case of pushdown graphs, we use these results to show that the sets of winning positions are regular and we show how to compute them as well as positional winning strategies in exponential time.
This research was supported by European Research Training Network: Games and Automata for Synthesis and Validation.
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
Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controlers with partial observation. Theoretical Computer Science 303(1), 7–34 (2003)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Bouquet, A.-J., Serre, O., Walukiewicz, I.: Pushdown games with unboundedness and regular conditions. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 88–99. Springer, Heidelberg (2003)
Cachat, T.: Symbolic strategy for games on pushdown graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 704–715. Springer, Heidelberg (2002)
Cachat, T., Duparc, J., Thomas, W.: Pushdown games with a σ 3 winning condition. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 322–336. Springer, Heidelberg (2002)
Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 100–113. Springer, Heidelberg (2003)
de Alfaro, L., Henzinger, T.A.: Concurrent ω-regular games. In: LICS 2000, pp. 142–154. IEEE Computer Society Press, Los Alamitos (2000)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: FOCS 1998, pp. 564–575. IEEE Computer Society Press, Los Alamitos (1998)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. of 32th FOCS, pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)
Gimbert, H.: Parity and exploration games on infinite graphs, www.liafa.jussieu.fr/~hugo (full version)
Grädel, E.: Positional determinacy of infinite games. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 4–18. Springer, Heidelberg (2004)
Kupferman, O., Piterman, N., Vardi, M.: Pushdown specifictaions. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, Springer, Heidelberg (2002)
Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to reasoning about infinite state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 36–52. Springer, Heidelberg (2000)
Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata and second order logic. Thoretical Computer Science 37, 51–75 (1985)
Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata. Theoretical Computer Science 141, 69–107 (1995)
Piterman, N., Vardi, M.: From bidirectionnality to alternation. Theoretical Computer Science 295, 295–321 (2003)
Serre, O.: Games with winning conditions of high borel complexity. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1150–1162. Springer, Heidelberg (2004)
Serre, O.: Note on winning positions on pushdown games with omega-regular conditions. Information Processing Letters 85(6), 285–291 (2003)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Y. Vardi, M.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)
Walukiewicz, I.: Pushdown processes: Games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996)
Walukiewicz, I.: Pushdown processes: Games and model checking. Information and Computation 164(2), 234–263 (2001)
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
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gimbert, H. (2004). Parity and Exploration Games on Infinite Graphs. In: Marcinkowski, J., Tarlecki, A. (eds) Computer Science Logic. CSL 2004. Lecture Notes in Computer Science, vol 3210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30124-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-30124-0_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23024-3
Online ISBN: 978-3-540-30124-0
eBook Packages: Springer Book Archive