City Research Online

Undecidability of a weak version of MSO+U

Bojańczyk, M., Daviaud, L., Guillon, B., Penelle, V. and Sreejith, A.V. Undecidability of a weak version of MSO+U. .


We prove the undecidability of mso on ω -words extended with the second-order predicate U1 ( X ) which says that the distance between consecutive positions in a set X ⊆ N is unbounded. This is achieved by showing that adding U1 to mso gives a logic with the same expressive power as mso + U , a logic on ω -words with undecidable satisfiability. As a corollary, we prove that mso on ω -words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e. , sets X such that for some positive integer p , ultimately either both or none of positions x and x + p belong to X

Publication Type: Monograph (Working Paper)
Additional Information: This is a preprint article that has been submitted to Logic Methods in Computer Science.
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Mathematics, Computer Science & Engineering > Computer Science
Text - Submitted Version
Download (6MB) | Preview



Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login