Weak monadic second-order logic (WMSO) over the infinite binary tree has the same syntax as MSO, but second-order quantification is interpreted only over finite sets. It captures a strict subclass of the regular languages of infinite trees, but is expressive enough to subsume temporal logics like CTL.

In this talk, I will sketch the proofs showing the equivalence of WMSO and a form of automata called weak alternating automata. I will also prove Rabin’s characterization of WMSO: a language is weakly definable iff the language and its complement are recognizable by nondeterministic Büchi automata.

I will conclude by describing connections with recent work (joint with Thomas Colcombet, Denis Kuperberg, and Christof Löding) showing that given a Büchi automaton as input, it is decidable whether the language is definable in WMSO.