joint work with Alexander Rabinovich and Adam Radziwonczyk-Syta

What sets of infinite words can be defined by means of MSO formulas interpreted in a binary tree, if we additionally allow some monadic predicates over the nodes ? We show that topologically these languages are no more complex than ordinary omega-regular languages. The proof goes via a characterization of this class by Buchi automata with advice, which can be determinized by a suitable adaptation of the classical Safra construction.