Thin MSO with a Probabilistic Path Quantifier.
This paper is about a variant of MSO on infinite trees where: - there is a quantifier zero probability of choosing a path pi in 2^{omega} which makes omega(pi) true; - the monadic quantifiers range over sets with countable topological closure. We introduce an automaton model, and show that it captures the logic.