The Structure of Trees in the Pushdown Hierarchy

Authors Arnaud Carayol, Lucien Charamond

Thumbnail PDF


  • Filesize: 0.75 MB
  • 18 pages

Document Identifiers

Author Details

Arnaud Carayol
  • Univ Gustave Eiffel, CNRS, LIGM, F-77454 Marne-la-Vallée, France
Lucien Charamond
  • Univ Gustave Eiffel, CNRS, LIGM, F-77454 Marne-la-Vallée, France


The authors are indebted to Didier Caucal for pointing out the notion of (𝓁,b)-tree implicit in the work [Boris Adamczewski et al., 2020] and starting this work. The authors would like to thanks the reviewers for their work.

Cite AsGet BibTex

Arnaud Carayol and Lucien Charamond. The Structure of Trees in the Pushdown Hierarchy. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 131:1-131:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


In this article, we investigate the structure of the trees in the pushdown hierarchy, a hierarchy of infinite graphs having a decidable MSO-theory. We show that a binary complete tree in the pushdown hierarchy must contain at least two different subtrees which are isomorphic. We extend this property to any tree with no leaves and with chains of unary vertices of bounded length. We provided two applications of this result. A first application in formal language theory, gives a simple argument to show that some languages are not deterministic higher-order indexed languages. A second application in number theory shows that the real numbers defined by deterministic higher-order pushdown automata are either rational or transcendental.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Verification by model checking
  • Pushdown hierarchy
  • Monadic second-order logic
  • Automatic numbers


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


  1. Luca Aceto, Arnaud Carayol, Zoltán Ésik, and Anna Ingólfsdóttir. Algebraic synchronization trees and processes. In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, volume 7392 of Lecture Notes in Computer Science, pages 30-41. Springer, 2012. URL:
  2. Boris Adamczewski and Yann Bugeaud. On the complexity of algebraic numbers I. Expansions in integer bases. Annals of Mathematics, 165(2):547-565, 2007. Google Scholar
  3. Boris Adamczewski, Julien Cassaigne, and Marion Le Gonidec. On the computational complexity of algebraic numbers : the Hartmanis-Stearns problem revisited. Transactions of the American Mathematical Society, 373:3085-3115., 2020. Google Scholar
  4. Jean-Paul Allouche and Jeffrey O. Shallit. Automatic Sequences - Theory, Applications, Generalizations. Cambridge University Press, 2003. URL:
  5. Achim Blumensath. On the structure of graphs in the Caucal hierarchy. Theor. Comput. Sci., 400(1-3):19-45, 2008. URL:
  6. Achim Blumensath. Erratum to "On the structure of graphs in the Caucal hierarchy" [Theoret. Comput. Sci 400 (2008) 19-45]. Theor. Comput. Sci., 475:126-127, 2013. URL:
  7. Laurent Braud and Arnaud Carayol. Linear orders in the pushdown hierarchy. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 88-99. Springer, 2010. URL:
  8. Arnaud Carayol and Stefan Wöhrle. The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In Paritosh K. Pandya and Jaikumar Radhakrishnan, editors, FSTTCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Mumbai, India, December 15-17, 2003, Proceedings, volume 2914 of Lecture Notes in Computer Science, pages 112-123. Springer, 2003. Google Scholar
  9. Didier Caucal. On infinite transition graphs having a decidable monadic theory. In Friedhelm Meyer auf der Heide and Burkhard Monien, editors, Automata, Languages and Programming, 23rd International Colloquium, ICALP96, Paderborn, Germany, 8-12 July 1996, Proceedings, volume 1099 of Lecture Notes in Computer Science, pages 194-205. Springer, 1996. URL:
  10. Didier Caucal. On infinite terms having a decidable monadic theory. In Krzysztof Diks and Wojciech Rytter, editors, Mathematical Foundations of Computer Science 2002, 27th International Symposium, MFCS 2002, Warsaw, Poland, August 26-30, 2002, Proceedings, volume 2420 of Lecture Notes in Computer Science, pages 165-176. Springer, 2002. URL:
  11. Didier Caucal and Marion Le Gonidec. Context-free sequences. In Gabriel Ciobanu and Dominique Méry, editors, Theoretical Aspects of Computing - ICTAC 2014 - 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, volume 8687 of Lecture Notes in Computer Science, pages 259-276. Springer, 2014. URL:
  12. Bruno Courcelle. Monadic second-order definable graph transductions: A survey. Theor. Comput. Sci., 126(1):53-75, 1994. URL:
  13. Bruno Courcelle and Igor Walukiewicz. Monadic second-order logic, graph coverings and unfoldings of transition systems. Ann. Pure Appl. Log., 92(1):35-62, 1998. URL:
  14. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. ACM Trans. Comput. Log., 18(3):25:1-25:42, 2017. URL:
  15. Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL:
  16. A. N. Maslov. Multilevel stack automata. Problems of Information Transmission, 12:38-43, 1976. Google Scholar
  17. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL:
  18. Paweł Parys. A pumping lemma for pushdown graphs of any level. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 54-65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL:
  19. Paweł Parys. On the expressive power of higher-order pushdown systems. Log. Methods Comput. Sci., 16(3), 2020. URL:
  20. Paweł Parys. The Caucal hierarchy: Interpretations in the (W)MSO+U logic. Inf. Comput., 286:104782, 2022. URL:
  21. Wolfgang Thomas. Constructing infinite graphs with a decidable mso-theory. In Branislav Rovan and Peter Vojtás, editors, Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25-29, 2003, Proceedings, volume 2747 of Lecture Notes in Computer Science, pages 113-124. Springer, 2003. URL:
  22. Igor Walukiewicz. Monadic second-order logic on tree-like structures. Theor. Comput. Sci., 275(1-2):311-346, 2002. URL: