Document Open Access Logo

Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches

Authors Mikołaj Bojańczyk , Antonio Casares , Sven Manthe , Paweł Parys

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.21.pdf
  • Filesize: 0.82 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • MSO logic
  • automata over infinite trees
  • games on graphs

Metrics

Abstract

Rabin’s Tree Theorem says that the {mso} theory of the infinite binary tree 2^* is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to 2^{≤ω}, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in 2^{≤ω} by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin’s Theorem can be extended to the new framework. The only missing part is a conjecture about finite-memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games.

Cite As Get BibTex

Mikołaj Bojańczyk, Antonio Casares, Sven Manthe, and Paweł Parys. Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.21

Author Details

Mikołaj Bojańczyk
  • Institute of Informatics, University of Warsaw, Poland
Antonio Casares
  • University of Kaiserslautern-Landau, Germany
Sven Manthe
  • University of Bonn, Germany
Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland

Funding

  • Bojańczyk, Mikołaj: Author supported by the Polish National Science Centre (NCN) grant "Polynomial finite state computation" (2022/46/A/ST6/00072).
  • Casares, Antonio: Partially supported by Deutsche Forschungsgemeinschaft (grant number 522843867) and European Research Council (grant number 101089343). Part of this work was done while Casares was at the University of Warsaw, Poland, supported by the Polish National Science Centre (NCN) grant "Polynomial finite state computation" (2022/46/A/ST6/00072).
  • Manthe, Sven: Author supported by Hausdorff Center for Mathematics at the University of Bonn (DFG EXC 2047).
  • Parys, Paweł: Author supported by the Polish National Science Centre (NCN) grant "Frontiers of automatic analysis of concurrent systems" (2021/41/B/ST6/00535).

References

  1. J. P. Aguilera. Long Borel games. Israel J. Math., 243(1):273-314, 2021. URL: https://doi.org/10.1007/s11856-021-2160-y.
  2. Mikołaj Bojańczyk, Damian Niwiński, Alexander Rabinovich, Adam Radziwończyk-Syta, and Michał Skrzypczak. On the Borel complexity of MSO definable sets of branches. Fund. Inform., 98(4):337-349, 2010. URL: https://doi.org/10.3233/fi-2010-231.
  3. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: https://doi.org/10.2307/1994916.
  4. J. Richard Büchi and Charles Zaiontz. Deterministic automata and the monadic theory of ordinals < ω_2. Z. Math. Logik Grundlag. Math., 29(4):313-336, 1983. URL: https://doi.org/10.1002/malq.19830290503.
  5. Mirna Džamonja. MSO logic of the real order with the set quantifiers ranging over the Borel sets. CoRR, 2025. URL: https://arxiv.org/abs/2512.23003.
  6. Nathanaël Fijalkow, C. Aiswarya, Guy Avni, Nathalie Bertrand, Patricia Bouyer, Romain Brenguier, Arnaud Carayol, Antonio Casares, John Fearnley, Paul Gastin, Hugo Gimbert, Thomas A. Henzinger, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Pierre Ohlmann, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, Mateusz Skomra, Nathalie Sznajder, and Pierre Vandenhove. Games on graphs: From logic and automata to algorithms, 2026. Cambridge University Press. URL: https://arxiv.org/abs/2305.10546.
  7. Yuri Gurevich. Monadic second-order theories. In J. Barwise and S. Feferman, editors, Model-theoretic logics, Perspectives in Mathematical Logic, pages 479-506. Springer-Verlag, New York, 1985. Google Scholar
  8. Yuri Gurevich and Leo Harrington. Trees, automata and games. In Proc. ACM Symp. on Theory of Computing, pages 60-65. Assoc. Comput. Mach., 1982. URL: https://doi.org/10.1145/800070.802177.
  9. Yuri Gurevich and Saharon Shelah. Monadic theory of order and topology in ZFC. Ann. Math. Logic, 23(2-3):179-198, 1982. URL: https://doi.org/10.1016/0003-4843(82)90004-3.
  10. Lawrence H. Landweber. Decision problems for omega-automata. Math. Syst. Theory, 3(4):376-384, 1969. URL: https://doi.org/10.1007/BF01691063.
  11. Sven Manthe. The Borel monadic theory of order is decidable. CoRR, 2024. URL: https://arxiv.org/abs/2410.00887.
  12. Sven Manthe. Decidability in Borel Monadic Logic. PhD thesis, Rheinische Friedrich-Wilhelms-Universität Bonn, 2026. Google Scholar
  13. Donald A. Martin. Borel determinacy. Ann. of Math. (2), 102(2):363-371, 1975. URL: https://doi.org/10.2307/1971035.
  14. Jan Mycielski. On the axiom of determinateness. Fund. Math., 53:205-224, 1963/64. URL: https://doi.org/10.4064/fm-53-2-205-224.
  15. Itay Neeman. Finite state automata and monadic definability of singular cardinals. J. Symbolic Logic, 73(2):412-438, 2008. URL: https://doi.org/10.2178/jsl/1208359052.
  16. Itay Neeman. Monadic definability of ordinals. In Computational prospects of infinity. Part II. Presented talks, volume 15 of Lect. Notes Ser. Inst. Math. Sci. Natl. Univ. Singap., pages 193-205. World Sci. Publ., Hackensack, NJ, 2008. URL: https://doi.org/10.1142/9789812796554_0010.
  17. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1-35, 1969. URL: https://doi.org/10.2307/1995086.
  18. Saharon Shelah. The monadic theory of order. Ann. of Math. (2), 102(3):379-419, 1975. URL: https://doi.org/10.2307/1971037.
  19. Saharon Shelah. On what I do not understand (and have something to say), model theory. Math. Japon., 51(2):329-377, 2000. Google Scholar
  20. Wolfgang Thomas. On the synthesis of strategies in infinite games. In Ernst W. Mayr and Claude Puech, editors, STACS 95, 12th Annual Symposium on Theoretical Aspects of Computer Science, Munich, Germany, March 2-4, 1995, Proceedings, volume 900 of Lecture Notes in Computer Science, pages 1-13. Springer, 1995. URL: https://doi.org/10.1007/3-540-59042-0_57.
  21. Wolfgang Thomas. Languages, automata, and logic. In Handbook of formal languages, Vol. 3, pages 389-455. Springer, Berlin, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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