A gap property for Buchi languages of infinite trees

In this talk I will speak about classes of languages of infinite trees
definable in monadic second-order (MSO) logic. My main interest will
be in two such classes: languages that are definable in the weak
variant of MSO (or equivalently recognisable by weak alternating
automata); and languages definable in the existential fragment of MSO
(or equivalently recognisable by Buchi automata). The former languages
are always Borel while the latter are always analytic (i.e.
\Sigma^1_1). One of the natural questions about these classes asks,
whether the topological complexity corresponds to the logical
complexity of a given language. It was formulated by Skurczyński in
1993 as the following conjecture: if a regular language of infinite
trees is Borel then it is weak MSO-definable.

During my talk I will present a joint work with Igor Walukiewicz
proving that the conjecture holds for languages recognisable by Buchi
automata. More precisely, I will prove that the language recognisable
by a Buchi automaton is either weak MSO-definable and Borel; or not
weak MSO-definable and \Sigma^1_1-complete. Moreover, it is decidable
which of the cases holds. Although, an effective characterisation of
weak MSO-definable languages among Buchi automata was already given by
Colcombet et al.; this is the first result proving the conjecture of
Skurczyński for automata that admit unrestricted non-determinism.