  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.
