Category and Measure in the Monadic Second Order Theory of Trees

The decidability of the "Satisfiability" problem is a major
open problem in the area of logics of probabilistic programs such as,
e.g., PCTL*.

We introduce an extension of "MSO with Null quantifier": MSO+N. The
system MSO+N is sufficiently expressive to encode  qualitative
fragments of probabilistic logics, such as pCTL*, ECTL* and
probabilistic mu calculus.

Due to this expressivity, MSO+N can define non-regular trees (this is
a feature shared by most probabilistic logics). In contrast to other
known extensions of MSO on the infinite tree,  however, so far there
is no reason to believe that MSO+N has an undecidable theory.

Indeed we show that a similar extension, MSO+M (Meager quantifier)
reduces to MSO. We use this result to prove that the F-SAT (Finite
Satisfiability) problem for the qualitative fragment of pCTL* and
similar logics is decidable. This extends a previous result of T.
Brazdil, V. Forejt, J. Kretınsky, and A. Kucera presented in the
article "The satisfiability problem for probabilistic CTL".