Undecidability of MSO with Path-Measure Quantifier via Probabilistic Automata

We consider monadic second-order logic extended with the qualitative path-measure quantifier that is interpreted over the infinite binary tree. This quantifier says that the set of infinite paths in the tree satisfying a formula has Lebesgue-measure one. We prove that this logic is undecidable. Towards this we first show that the emptiness problem of qualitative universal parity tree automata is undecidable, where qualitative means that a run of a tree automaton is accepting if the set of paths in the run that satisfies the acceptance condition has Lebesgue-measure equal to one. This result also implies the undecidability of the emptiness problem of a recently introduced model of alternating probabilistic tree automata. This is a joint work with Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, Aniello Murano, Jean-François Raskin, Sasha Rubin and Olivier Serre. It has been written but not published.

Authors

• Laureline Pinault.

Keywords

No keywords are indexed for this paper.