Document Open Access Logo

A Dichotomy Theorem for Ordinal Ranks in MSO

Authors Damian Niwiński , Paweł Parys , Michał Skrzypczak

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2025.69.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Tree languages
Keywords
  • dichotomy result
  • limit ordinal
  • countable ordinals
  • nondeterministic tree automata

Metrics

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

Abstract

We focus on formulae ∃X.φ(Y, X) of monadic second-order logic over the full binary tree, such that the witness X is a well-founded set. The ordinal rank rank(X) < ω₁ of such a set X measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula φ. Let η_φ be the minimal ordinal such that, whenever an instance Y satisfies the formula, there is a witness X with rank(X) ≤ η_φ. Then η_φ is either strictly smaller than ω² or it reaches the maximal possible value ω₁. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.

Cite As Get BibTex

Damian Niwiński, Paweł Parys, and Michał Skrzypczak. A Dichotomy Theorem for Ordinal Ranks in MSO. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 69:1-69:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.69

Author Details

Damian Niwiński
  • Institute of Informatics, University of Warsaw, Poland
Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland
Michał Skrzypczak
  • Institute of Informatics, University of Warsaw, Poland

Funding

All authors supported by the National Science Centre, Poland (grant no. 2021/41/B/ST6/03914).

Acknowledgements

The authors would like to thank Marek Czarnecki for preliminary discussions on related subjects.

References

  1. Bahareh Afshari, Giacomo Barlucchi, and Graham E. Leigh. The limit of recursion in state-based systems. In FICS, 2024. URL: https://www.irif.fr/_media/users/saurin/fics2024/pre-proceedings/fics-2024-afshari-etal.pdf.
  2. Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In CSL, volume 23 of LIPIcs, pages 30-44. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPICS.CSL.2013.30.
  3. Vince Bárány, Łukasz Kaiser, and Alexander M. Rabinovich. Expressing cardinality quantifiers in monadic second-order logic over trees. Fundam. Inform., 100(1-4):1-17, 2010. URL: https://doi.org/10.3233/FI-2010-260.
  4. Mikołaj Bojańczyk. Weak MSO+U with path quantifiers over infinite trees. In ICALP (2), volume 8573 of Lecture Notes in Computer Science, pages 38-49. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_4.
  5. Julian C. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. In STACS, volume 1373 of Lecture Notes in Computer Science, pages 39-49. Springer, 1998. URL: https://doi.org/10.1007/BFB0028547.
  6. Julian C. Bradfield, Jacques Duparc, and Sandra Quickert. Transfinite extension of the mu-calculus. In CSL, volume 3634 of Lecture Notes in Computer Science, pages 384-396. Springer, 2005. URL: https://doi.org/10.1007/11538363_27.
  7. Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Handbook of Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  8. Julius R. Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  9. Lorenzo Clemente and Michał Skrzypczak. Deterministic and game separability for regular languages of infinite trees. In ICALP, volume 198 of LIPIcs, pages 126:1-126:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ICALP.2021.126.
  10. Thomas Colcombet, Denis Kuperberg, Christof Löding, and Michael Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In CSL, volume 23 of LIPIcs, pages 215-230. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPICS.CSL.2013.215.
  11. Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. In ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages 398-409. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_33.
  12. Marek Czarnecki. How fast can the fixpoints in modal mu-calculus be reached? In FICS, pages 35-39. Laboratoire d'Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=36.
  13. Christian Delhommé. Automaticité des ordinaux et des graphes homogènes. Comptes Rendus de L’Académie des Sciences, Mathématiques, 339(1):5-10, 2004. Google Scholar
  14. Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theor. Comput. Sci., 412(28):3226-3241, 2011. URL: https://doi.org/10.1016/J.TCS.2011.03.020.
  15. Alessandro Facchini, Filip Murlak, and Michał Skrzypczak. Rabin-Mostowski index problem: A step beyond deterministic automata. In LICS, pages 499-508. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.56.
  16. Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra. Games on graphs. CoRR, abs/2305.10546, 2023. URL: https://doi.org/10.48550/arXiv.2305.10546.
  17. Olivier Finkel and Stevo Todorcevic. Automatic ordinals. Int. J. Unconv. Comput., 9(1-2):61-70, 2013. URL: http://www.oldcitypublishing.com/journals/ijuc-home/ijuc-issue-contents/ijuc-volume-9-number-1-2-2013/ijuc-9-1-2-p-61-70/.
  18. Gaëlle Fontaine. Continuous fragment of the mu-calculus. In CSL, volume 5213 of Lecture Notes in Computer Science, pages 139-153. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_12.
  19. Maria J. Gouveia and Luigi Santocanale. ℵ_1 and the modal μ-calculus. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:1)2019.
  20. Olivier Idir and Karoliina Lehtinen. Mostowski index via extended register games. CoRR, abs/2412.16793, 2024. URL: https://doi.org/10.48550/arXiv.2412.16793.
  21. Alexander Kechris. Classical descriptive set theory. Springer-Verlag, New York, 1995. Google Scholar
  22. Damian Niwiński. On the cardinality of sets of infinite trees recognizable by finite automata. In MFCS, volume 520 of Lecture Notes in Computer Science, pages 367-376. Springer, 1991. URL: https://doi.org/10.1007/3-540-54345-7_80.
  23. Damian Niwiński and Igor Walukiewicz. A gap property of deterministic tree languages. Theor. Comput. Sci., 1(303):215-231, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00452-8.
  24. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  25. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  26. Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. (Complexité algorithmique des beaux pré-ordres). École normale supérieure Paris-Saclay, 2017. URL: https://tel.archives-ouvertes.fr/tel-01663266.
  27. Michał Skrzypczak. Descriptive Set Theoretic Methods in Automata Theory - Decidability and Topological Complexity, volume 9802 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-52947-8.
  28. Michał Skrzypczak and Igor Walukiewicz. Deciding the topological complexity of Büchi languages. In ICALP, volume 55 of LIPIcs, pages 99:1-99:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.99.
  29. Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages (3), pages 389-455. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact