Weak MSO+U over infinite trees

Mikolaj Bojanczyk & Szymon Torunczyk
We prove that, over infinite trees, satisfiability is decidable for Weak Monadic Second-Order Logic extended by the unbounding quantifier U. We develop an automaton model, prove that it is effectively equivalent to the logic, and that the automaton model has decidable emptiness.