Weak MSO+U with Path Quantifiers over Infinite Trees

TL;DR

This paper proves that satisfiability for a specific extension of weak monadic second-order logic over infinite trees is decidable, using automaton-based methods and profinite trees.

Contribution

It establishes decidability of satisfiability for weak MSO+U with path quantifiers over infinite trees, a previously unresolved problem.

Findings

Decidability of satisfiability for weak MSO+U with path quantifiers over infinite trees.

Reduction to automaton emptiness problem using profinite trees.

Automaton emptiness is decidable via profinite tree techniques.

Abstract

This paper shows that over infinite trees, satisfiability is decidable for weak monadic second-order logic extended by the unbounding quantifier U and quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees.