MSO+∇ is undecidable


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 tree.

In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019