A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct

Authors Shibashis Guha , Ismaël Jecker , Karoliina Lehtinen , Martin Zimmermann

Thumbnail PDF


  • Filesize: 0.78 MB
  • 20 pages

Document Identifiers

Author Details

Shibashis Guha
  • Tata Institute of Fundamental Research, Mumbai, India
Ismaël Jecker
  • IST Austria, Klosterneuburg, Austria
Karoliina Lehtinen
  • CNRS, Aix-Marseille University and University of Toulon, LIS, Marseille, France
Martin Zimmermann
  • University of Liverpool, UK

Cite AsGet BibTex

Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 53:1-53:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


We study the expressiveness and succinctness of good-for-games pushdown automata (GFG-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. We prove that GFG-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that GFG-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than GFG-PDA. We also study GFGness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show GFGness to be ExpTime-complete. GFG-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than GFG-VPA. Both of these lower bounds are tight. Finally, we study the complexity of resolving nondeterminism in GFG-PDA. Every GFG-PDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of GFG-VPA, but not those of GFG-PDA. GFG-PDA with finite-state resolvers are determinisable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Pushdown Automata
  • Good-for-games
  • Synthesis
  • Succintness


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Shaull Almagor and Orna Kupferman. Good-enough synthesis. In Shuvendu K. Lahiri and Chao Wang, editors, CAV 2020, Part II, volume 12225 of LNCS, pages 541-563. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_28.
  2. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In László Babai, editor, STOC 2004, pages 202-211. ACM, 2004. URL: https://doi.org/10.1145/1007352.1007390.
  3. Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In Sumit Ganguly and Paritosh Pandya, editors, FSTTCS 2018, volume 122 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.16.
  4. Henrik Björklund and Wim Martens. The tractability frontier for NFA minimization. Journal of Computer and System Sciences, 78(1):198-210, 2012. Google Scholar
  5. Henrik Björklund, Martin Schuster, Thomas Schwentick, and Joscha Kulbatzki. On optimum left-to-right strategies for active context-free games. In Wang-Chiew Tan, Giovanna Guerrini, Barbara Catania, and Anastasios Gounaris, editors, ICDT 2013, pages 105-116. ACM, 2013. URL: https://doi.org/10.1145/2448496.2448510.
  6. Udi Boker, Orna Kupferman, and Michał Skrzypczak. How deterministic are good-for-games automata? arXiv, 2017. URL: http://arxiv.org/abs/1710.04115.
  7. J. Richard Büchi. Regular canonical systems. Archiv für mathematische Logik und Grundlagenforschung, 6(3):91-111, April 1964. URL: https://doi.org/10.1007/BF01969548.
  8. Arnaud Carayol and Matthew Hague. Saturation algorithms for model-checking pushdown systems. In Zoltán Ésik and Zoltán Fülöp, editors, AFL 2014, volume 151 of EPTCS, pages 1-24, 2014. URL: https://doi.org/10.4204/EPTCS.151.1.
  9. Arnaud Carayol and Christof Löding. Uniformization in automata theory, 2015. In LMPS 2015. URL: https://hal.archives-ouvertes.fr/hal-01806575.
  10. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, ICALP 2009, (Part II), volume 5556 of LNCS, pages 139-150. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_12.
  11. Olivier Finkel. Topological properties of omega context-free languages. Theor. Comput. Sci., 262(1):669-697, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00405-9.
  12. David Gale and F. M. Stewart. Infinite games with perfect information. In Harold William Kuhn and Albert William Tucker, editors, Contributions to the Theory of Games (AM-28), Volume II, chapter 13, pages 245-266. Princeton University Press, 1953. Google Scholar
  13. Jonathan Goldstine, Hing Leung, and Detlef Wotschke. Measuring nondeterminism in pushdown automata. Journal of Computer and System Sciences, 71(4):440-466, 2005. Google Scholar
  14. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct. arXiv, 2021. URL: http://arxiv.org/abs/2105.02611.
  15. Juris Hartmanis. On the succinctness of different representations of languages. SIAM J. Comput., 9(1):114-120, 1980. URL: https://doi.org/10.1137/0209010.
  16. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Zoltán Ésik, editor, CSL 2006, volume 4207 of LNCS, pages 395-410. Springer, 2006. URL: https://doi.org/10.1007/11874683_26.
  17. Christian Herzog. Pushdown automata with bounded nondeterminism and bounded ambiguity. Theor. Comput. Sci., 181(1):141-157, 1997. Google Scholar
  18. Markus Holzer and Martin Kutrib. Descriptional complexity of (un)ambiguous finite state machines and pushdown automata. In Antonín Kucera and Igor Potapov, editors, RP 2010, volume 6227 of LNCS, pages 1-23. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15349-5_1.
  19. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. Google Scholar
  20. Tao Jiang and Bala Ravikumar. Minimal NFA problems are hard. SIAM Journal on Computing, 22(6):1117-1141, 1993. Google Scholar
  21. Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan. Visibly pushdown automata for streaming XML. In Carey L. Williamson, Mary Ellen Zurko, Peter F. Patel-Schneider, and Prashant J. Shenoy, editors, WWW 2007, pages 1053-1062. ACM, 2007. URL: https://doi.org/10.1145/1242572.1242714.
  22. Denis Kuperberg and Anirban Majumdar. Computing the width of non-deterministic automata. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:10)2019.
  23. Denis Kuperberg and Michal Skrzypczak. On determinisation of good-for-games automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, ICALP 2015 (Part II), volume 9135 of LNCS, pages 299-310. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_24.
  24. Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating word and tree automata. Annals of Pure and Applied Logic, 138(1-3):126-146, 2006. Google Scholar
  25. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS 2020, pages 689-702. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394737.
  26. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. arXiv, 2020. URL: http://arxiv.org/abs/2001.04392.
  27. Christof Löding, P. Madhusudan, and Olivier Serre. Visibly pushdown games. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004, volume 3328 of LNCS, pages 408-420. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_34.
  28. Wim Martens, Frank Neven, Thomas Schwentick, and Geert Jan Bex. Expressiveness and complexity of XML schema. TODS, 31(3):770-813, 2006. Google Scholar
  29. Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Active context-free games. Theory of Computing Systems, 39(1):237-276, 2006. Google Scholar
  30. Dirk Nowotka and Jirí Srba. Height-deterministic pushdown automata. In Ludek Kucera and Antonín Kucera, editors, MFCS 2007, volume 4708 of LNCS, pages 125-134. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74456-6_13.
  31. Alexander Okhotin and Kai Salomaa. Descriptional complexity of unambiguous input-driven pushdown automata. Theor. Comput. Sci., 566:1-11, 2015. URL: https://doi.org/10.1016/j.tcs.2014.11.015.
  32. Bader Abu Radi and Orna Kupferman. Minimizing GFG Transition-Based Automata. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, ICALP 2019, volume 132 of LIPIcs, pages 100:1-100:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.100.
  33. Arto Salomaa and Matti Soittola. Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science. Springer, 1978. URL: https://doi.org/10.1007/978-1-4612-6264-0.
  34. Kai Salomaa and Sheng Yu. Limited nondeterminism for pushdown automata. Bull. EATCS, 50:186-193, 1993. Google Scholar
  35. Sven Schewe. Minimising Good-For-Games Automata Is NP-Complete. In Nitin Saxena and Sunil Simon, editors, FSTTCS 2020, volume 182 of LIPIcs, pages 56:1-56:13. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.56.
  36. Géraud Sénizergues. L(A)=L(B)? decidability results from complete formal systems. Theor. Comput. Sci., 251(1-2):1-166, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00285-1.
  37. Richard Edwin Stearns and Harry B Hunt III. On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata. SIAM Journal on Computing, 14(3):598-611, 1985. Google Scholar
  38. Leslie G. Valiant. A note on the succinctness of descriptions of deterministic languages. Inf. Control., 32(2):139-145, 1976. URL: https://doi.org/10.1016/S0019-9958(76)90173-X.
  39. Igor Walukiewicz. Pushdown processes: Games and model-checking. Inf. Comput., 164(2):234-263, 2001. URL: https://doi.org/10.1006/inco.2000.2894.