Extensions of the Caucal Hierarchy?

  • Paweł ParysEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11417)


The Caucal hierarchy contains graphs that can be obtained from finite graphs by alternately applying the unfolding operation and inverse rational mappings. The goal of this work is to check whether the hierarchy is closed under interpretations in logics extending the monadic second-order logic by the unbounding quantifier \(\mathsf U\). We prove that by applying interpretations described in the MSO+\(\mathsf {U^{fin}}\) logic (hence also in its fragment WMSO+\(\mathsf U\)) to graphs of the Caucal hierarchy we can only obtain graphs on the same level of the hierarchy. Conversely, interpretations described in the more powerful MSO+\(\mathsf U\) logic can give us graphs with undecidable MSO theory, hence outside of the Caucal hierarchy.


Caucal hierarchy Boundedness WMSO+U logic 



We thank Mikołaj Bojańczyk, Szymon Toruńczyk, and Arnaud Carayol for discussions preceding the process of creating this paper.


  1. 1.
    Bojańczyk, M.: A bounding quantifier. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 41–55. Springer, Heidelberg (2004). Scholar
  2. 2.
    Bojańczyk, M.: Weak MSO with the unbounding quantifier. Theory Comput. Syst. 48(3), 554–576 (2011). Scholar
  3. 3.
    Bojańczyk, M., Parys, P., Toruńczyk, S.: The MSO+U theory of (N, \(<\)) is undecidable. In: STACS, pp. 21:1–21:8 (2016).
  4. 4.
    Bojańczyk, M., Toruńczyk, S.: Weak MSO+U over infinite trees. In: STACS, pp. 648–660 (2012).
  5. 5.
    Cachat, T.: Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 556–569. Springer, Heidelberg (2003). Scholar
  6. 6.
    Carayol, A.: Automates infinis, logiques et langages. Ph.D. thesis. Université de Rennes 1 (2006)Google Scholar
  7. 7.
    Carayol, A., Wöhrle, S.: The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 112–123. Springer, Heidelberg (2003). Scholar
  8. 8.
    Caucal, D.: On infinite transition graphs having a decidable monadic theory. In: Meyer, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 194–205. Springer, Heidelberg (1996). Scholar
  9. 9.
    Caucal, D.: On infinite terms having a decidable monadic theory. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 165–176. Springer, Heidelberg (2002). Scholar
  10. 10.
    Colcombet, T.: A combinatorial theorem for trees. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 901–912. Springer, Heidelberg (2007). Scholar
  11. 11.
    Colcombet, T.: Composition with algebra at the background - on a question by Gurevich and Rabinovich on the monadic theory of linear orderings. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 391–404. Springer, Heidelberg (2013). Scholar
  12. 12.
    Colcombet, T., Löding, C.: Transforming structures by set interpretations. Log. Methods Comput. Sci. 3(2) (2007).
  13. 13.
    Courcelle, B.: Monadic second-order definable graph transductions: a survey. Theoret. Comput. Sci. 126(1), 53–75 (1994). Scholar
  14. 14.
    Courcelle, B., Walukiewicz, I.: Monadic second-order logic, graph coverings and unfoldings of transition systems. Ann. Pure Appl. Logic 92(1), 35–62 (1998). Scholar
  15. 15.
    Engelfriet, J.: Iterated stack automata and complexity classes. Inf. Comput. 95(1), 21–75 (1991). Scholar
  16. 16.
    Haddad, A.: IO vs OI in higher-order recursion schemes. In: FICS, pp. 23–30 (2012). Scholar
  17. 17.
    Hague, M., Murawski, A.S., Ong, C.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: LICS, pp. 452–461 (2008).
  18. 18.
    Hummel, S., Skrzypczak, M.: The topological complexity of MSO+U and related automata models. Fundam. Inform. 119(1), 87–111 (2012). Scholar
  19. 19.
    Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002). Scholar
  20. 20.
    Ong, C.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90 (2006).
  21. 21.
    Parys, P.: Variants of collapsible pushdown systems. In: CSL, pp. 500–515 (2012).
  22. 22.
    Parys, P.: Recursion schemes, the MSO logic, and the U quantifier (submitted).
  23. 23.
    Parys, P.: A type system describing unboundedness (submitted).
  24. 24.
    Parys, P.: On the significance of the collapse operation. In: LICS, pp. 521–530 (2012).
  25. 25.
    Penelle, V.: Rewriting higher-order stack trees. Theory Comput. Syst. 61(2), 536–580 (2017). Scholar
  26. 26.
    Walukiewicz, I.: Monadic second-order logic on tree-like structures. Theoret. Comput. Sci. 275(1–2), 311–346 (2002). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Institute of InformaticsUniversity of WarsawWarsawPoland

Personalised recommendations