Weak MSO+U over infinite trees
Mikołaj Bojańczyk, Szymon Toruńczyk · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2012
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.