Abstract
We consider infinitary two-player perfect information games defined over graphs of configurations of a pushdown automaton. We show how to solve such games when winning conditions are Boolean combinations of a Büchi condition and a new condition that we call unboundedness. An infinite play satisfies the unboundedness condition if there is no bound on the size of the stack during the play. We show that the problem of deciding a winner in such games is EXPTIME-complete.
This research has been partially supported by the European Community Research Training Network “Games and Automata for Synthesis and Validation” (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.
Similar content being viewed by others
References
Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers 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., Serre, O., Walukiewicz, I.: Pushdown games with the unboundedness and regular conditions: full version with complete proofs, http://www.labri.fr/~igw/publications.html
Cachat, T.: Symbolic strategy synthesis 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.: Uniform solution of parity games on prefix-recognizable graphs. In: Kucera, A., Mayr, R. (eds.) Proceedings of the 4th International Workshop on Verification of Infinite-State Systems. Electronic Notes in Theoretical Computer Science, vol. 68, Elsevier Science Publishers, Amsterdam (2002)
Cachat, T., Duparc, J., Thomas, W.: Solving pushdown games with a sigma-3 winning condition. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 322–336. Springer, Heidelberg (2002)
Emerson, E., Jutla, C., Sistla, A.: On model-checking for the mu-calculus and its fragments. Theoretical Computer Science 258(1-2), 491–522 (2001)
Emerson, E.A., Jutla, C., Sistla, A.: On model-checking for fragments of μ-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, Springer, Heidelberg (1993)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. FOCS 1991, pp. 368–377 (1991)
Esparza, J., Podelski, A.: Efficient algorithms for pre star and post star on interprocedural parallel flow graphs. In: POPL 2000: Principles of Programming Languages (2000)
Kupferman, O., Vardi, M.: 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., Schupp, P.: The theory of ends, pushdown automata and secondorder logic. Theoretical Computer Science 37, 51–75 (1985)
Muller, D., Schupp, P.: Alternating automata on infinite trees. Theoretical Computer Science 54, 267–276 (1987)
Serre, O.: Note on winning positions on pushdown games with ω-regular conditions. Information Processing Letters 85, 285–291 (2003)
Thomas, W.: Automata on infinite objects. In: van Leeuven, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–192. Elsevier, Amsterdam (1990)
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)
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 3, Springer, Heidelberg (1997)
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
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouquet, AJ., Serre, O., Walukiewicz, I. (2003). Pushdown Games with Unboundedness and Regular Conditions. In: Pandya, P.K., Radhakrishnan, J. (eds) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2003. Lecture Notes in Computer Science, vol 2914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24597-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-24597-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20680-4
Online ISBN: 978-3-540-24597-1
eBook Packages: Springer Book Archive