2019/01/14 by Berthon, Raphaël, Filiot, Emmanuel, Guha, Shibashis +5
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1901.04349
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.