MSO+nabla is undecidable

2019/01/21 by Mikołaj Bojańczyk, Bojańczyk, Mikołaj, Edon Kelmendi +3
Computer Science · #Formal Methods in Verification #semigroups and automata theory #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1901.06900

Abstract

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^w satisfies a formula ϕ(π)''. This logic was introduced by Michalewski and Mio; we call it MSO+nabla following notation of Shelah and Lehmann. The logic MSO+nabla subsumes many qualitative probabilistic formalisms, including qualitative probabilistic CTL, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+nabla is true in the full binary tree.

Related

• Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable
• Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
• Computing measures of weak-MSO definable sets of trees
• Monadic second order logic as the model companion of temporal logic
• Weak MSO+U with Path Quantifiers over Infinite Trees