Automata for MSO over infinite trees with quantification over Borel sets of branches

Prelegent(ci)

Mikołaj Bojańczyk

Afiliacja

University of Warsaw

Język referatu

angielski

Termin

21 stycznia 2026 14:15

Pokój

p. 5440

Tytuł w języku polskim

Automata for MSO over infinite trees with quantification over Borel sets of branches

Seminarium

Seminarium „Teoria automatów”

---

Joint work with Antonio Casares, Sven Manthe and Paweł Parys.

Rabin's Tree Theorem says that the MSO theory of the infinite binary tree is decidable. Shelah showed that MSO logic becomes undecidable if we allow quantification over sets of infinite branches. He also conjectured that the logic becomes decidable if we restrict the set quantification to Borel sets. We present an approach to Shelah's conjecture, by introducing an appropriate automaton model. We then show that Shelah’s conjecture would be implied by a certain finite memory determinacy property.  We are unable to prove that property, but provide some evidence in its favour.

 

---