Abstract
We consider parity games played on special pushdown graphs, namely those generated by one-counter processes. For parity games on pushdown graphs, it is known from [23] that deciding the winner is an ExpTime-complete problem. An important corollary of this result is that the μ-calculus model checking problem for pushdown processes is ExpTime-complete. As one-counter processes are special cases of pushdown processes, it follows that deciding the winner in a parity game played on the transition graph of a one-counter process can be achieved in ExpTime. Nevertheless the proof for the ExpTime-hardness lower bound of [23] cannot be adapted to that case. Therefore, a natural question is whether the ExpTime upper bound can be improved in this special case. In this paper, we adapt techniques from [11,4] and provide a PSpace upper bound and a DP-hard lower bound for this problem. We also give two important consequences of this result. First, we improve the best upper bound known for model-checking one-counter processes against μ-calculus. Second, we show how these games can be used to solve pushdown games with winning conditions that are Boolean combinations of a parity condition on the control states with conditions on the stack height.
This research has been partially supported by the European Community Research Training Network “Games and Automata for Synthesis and Validation” (GAMES), (contract HPRN-CT-2002-00283), see www.games.rwth-aachen.de.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Arnold, A., Niwiński, D.: Rudiments of mu-calculus. In: Studies in Logic and the Foundations of Mathematics, vol. 146, Elsevier, Amsterdam (2001)
Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controlers with partial observation. Theoretical Computer Science 303(1), 7–34 (2003)
Bouquet, A., Serre, O., Walukiewicz, I.: Pushdown games with the unboundedness and regular conditions. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 88–99. Springer, Heidelberg (2003)
Cachat, T.: Two-way tree automata solving pushdown games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 303–317. Springer, Heidelberg (2002)
Cachat, T., Duparc, J., Thomas, W.: Solving 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)
Emerson, E.A., Jutla, C., Sistla, A.: On model-checking for fragments of mu-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)
Gimbert, H.: Parity and exploration games on infinite graphs. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 56–70. Springer, Heidelberg (2004)
Jančar, P., Kučera, A., Moller, F.: Zdeněk Sawa. DP lower bounds for equivalence-checking and model-checking of one-counter automata 188, 1–19 (2004)
Kucera, A.: Efficient verification algorithms for one-counter processes. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 317–328. Springer, Heidelberg (2000)
Kupferman, O., Piterman, N., Vardi, M.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 519–535. Springer, Heidelberg (2001)
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)
Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)
Löding, C.: Methods for the transformation of ω-automata: Complexity and connection to second order logic. Diplomata thesis, Christian-Albrechts-University of Kiel (1998)
Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)
Martin, D.A.: Borel determinacy. Annals of Mathematics 102, 363–371 (1975)
Papadimitriou, C.: Complexity Theory. Addison-Wesley, Reading (1994)
Piterman, N.: Extending temporal logic with ω-automata. Master’s thesis, The Weizmann Institute of Science (2000)
Serre, O.: Contribution à l’étude des jeux sur des graphe de processus à pile. PhD thesis, Université Paris VII (November 2004)
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.: Parity games played on transition graphs of one-counter processes: full version with complete proofs, http://www.liafa.jussieu.fr/~serre
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)
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 157, 234–263 (2000)
Walukiewicz, I.: A landscape with games in the background. In: Proceeding of LICS 2004, pp. 356–366. IEEE Computer Society, Los Alamitos (2004)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Serre, O. (2006). Parity Games Played on Transition Graphs of One-Counter Processes. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_23
Download citation
DOI: https://doi.org/10.1007/11690634_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)