Undecidability of a weak version of MSO+U

Bojańczyk, Mikołaj, Daviaud, Laure, Guillon, Bruno, Penelle, Vincent and Sreejith, A. V. (2020) Undecidability of a weak version of MSO+U. Logical Methods in Computer Science, 16 (1).

[thumbnail of 1807.08506]
PDF (1807.08506) - Published Version
Available under License Creative Commons Attribution.

Download (5MB) | Preview


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.

Item Type: Article
Uncontrolled Keywords: mso logic,undecidability,theoretical computer science,computer science(all) ,/dk/atira/pure/subjectarea/asjc/2600/2614
Faculty \ School: Faculty of Science > School of Computing Sciences
Related URLs:
Depositing User: LivePure Connector
Date Deposited: 07 Jun 2023 13:30
Last Modified: 07 Jun 2023 13:30
URI: https://ueaeprints.uea.ac.uk/id/eprint/92313
DOI: 10.23638/LMCS-16(1:12)2020


Downloads per month over past year

Actions (login required)

View Item View Item