City Research Online

Undecidability of a weak version of MSO+U

Bojanczyk, M., Daviaud, L. ORCID: 0000-0002-9220-7118, Guillon, B. , Penelle, V. & Sreejith, A. V. (2020). Undecidability of a weak version of MSO+U. Logical Methods in Computer Science, 16(1), 12:1-12:15. doi: 10.23638/LMCS-16(1:12)2020


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: Article
Publisher Keywords: MSO logic, undecidability
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Science & Technology > Computer Science
Text - Published Version
Available under License Creative Commons: Attribution International Public License 4.0.

Download (5MB) | Preview



Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login