MSO+∇ is undecidable
Mikołaj Bojańczyk, Edon Kelmendi, Michał Skrzypczak · 2019
This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying “almost surely a branch π ∈ {0,1}ωsatisfies a formula φ(π)”, This logic was introduced by Michalewski and Mio; we call it MSO+∇ following notation of Shelah and Lehmann. The logic Mso+∇ subsumes many qualitative probabilistic formalisms, including qualitative probabilistic check, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+∇ is true in the full binary tree11Independently and in parallel another proof of this result was given employing different techniques in [3]..