arXiv:2611.10136 · v1

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

首次提交 2026-11-07 03:02

版本更新 2026-11-07 03:02

雷达观测 2026-11-10 10:11

摘要

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^{\le ω}$, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in $2^{\le ω}$ 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.

期刊信息：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)