Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable
Logic in Computer Science
2019-02-19 v5
Abstract
We prove that the theory of Monadic Second-Order logic (MSO) of the infinite binary tree extended with qualitative path-measure quantifier is undecidable. This quantifier says that the set of infinite paths in the tree that satisfies some formula has Lebesgue-measure one. To do this we prove that the emptiness problem of qualitative universal parity tree automata is undecidable. Qualitative means that a run of a tree automaton is accepting if the set of paths in the run that satisfy the acceptance condition has Lebesgue-measure one.
Keywords
Cite
@article{arxiv.1901.04349,
title = {Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable},
author = {Raphaël Berthon and Emmanuel Filiot and Shibashis Guha and Bastien Maubert and Aniello Murano and Laureline Pinault and Jean-François Raskin and Sasha Rubin},
journal= {arXiv preprint arXiv:1901.04349},
year = {2019}
}