DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.21

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

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

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.LICS.2026.21,
  author =	{Boja\'{n}czyk, Miko{\l}aj and Casares, Antonio and Manthe, Sven and Parys, Pawe{\l}},
  title =	{{Automata for MSO over Infinite Trees with Quantification over Borel Sets of Branches}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{21:1--21:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.21},
  URN =		{urn:nbn:de:0030-drops-268080},
  doi =		{10.4230/LIPIcs.LICS.2026.21},
  annote =	{Keywords: MSO logic, automata over infinite trees, games on graphs}
}

Search Results

Documents authored by Manthe, Sven

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

Abstract

Cite as

Thanks for your feedback!

Could not send message