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

Speaker(s)

Mikołaj Bojańczyk

Affiliation

University of Warsaw

Language of the talk

English

Date

Jan. 21, 2026, 2:15 p.m.

Room

room 5440

Title in Polish

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

Seminar

Seminar Automata Theory

---

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.

 

---