Regular Strategies in Pushdown Reachability Games

  • A. Carayol
  • M. Hague
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8762)


We show that positional winning strategies in pushdown reachability games can be implemented by deterministic finite state automata of exponential size. Such automata read the stack and control state of a given pushdown configuration and output the set of winning moves playable from that position.

This result can originally be attributed to Kupferman, Piterman and Vardi using an approach based on two-way tree automata. We present a more direct approach that builds upon the popular saturation technique. Saturation for analysing pushdown systems has been successfully implemented by Moped and WALi. Thus, our approach has the potential for practical applications to controller-synthesis problems.


Winning Strategy Tree Automaton Positional Strategy Winning Region Exponential Size 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with slam. Commun. ACM 54(7), 68–76 (2011)CrossRefGoogle Scholar
  2. 2.
    Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: SPIN, pp. 113–130 (2000)Google Scholar
  3. 3.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)Google Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Cachat, T.: Games on Pushdown Graphs and Extensions. PhD thesis, RWTH Aachen (2003)Google Scholar
  6. 6.
    Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: FOCS, pp. 368–377 (1991)Google Scholar
  7. 7.
    Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: INFINITY, vol. 9, pp. 27–37 (1997)Google Scholar
  9. 9.
    Hague, M., Ong, C.-H.L.: Winning regions of pushdown parity games: A saturation method. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 384–398. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Jones, N.D., Muchnick, S.S.: Even simple programs are hard to analyze. J. ACM 24, 338–350 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Kupferman, O., Piterman, N., Vardi, M.Y.: An automata-theoretic approach to infinite-state systems. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 202–259. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  12. 12.
    Piterman, N., Vardi, M.Y.: Global model-checking of infinite-state systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 387–400. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Schwoon, S.: Model-checking Pushdown Systems. PhD thesis, Technical University of Munich (2002)Google Scholar
  14. 14.
    Serre, O.: Note on winning positions on pushdown games with [omega]-regular conditions. Inf. Process. Lett. 85(6), 285–291 (2003)CrossRefzbMATHGoogle Scholar
  15. 15.
    Serre, O.: Contribution à létude des jeux sur des graphes de processus á pile. PhD thesis, Université Paris 7 – Denis Diderot, UFR dinformatique (2004)Google Scholar
  16. 16.
    Suwimonteerabuth, D., Berger, F., Schwoon, S., Esparza, J.: jMoped: A test environment for java programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 164–167. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A java bytecode checker based on moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 541–545. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  18. 18.
    Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 141–153. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
  20. 20.
    Walukiewicz, I.: Pushdown processes: Games and model-checking. Inf. Comput. 164(2), 234–263 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1-2), 135–183 (1998)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • A. Carayol
    • 1
    • 2
  • M. Hague
    • 1
    • 2
  1. 1.LIGMUniversité Paris-Est & CNRSFrance
  2. 2.Royal Holloway University of LondonUK

Personalised recommendations