Undecidability of a weak version of MSO+U

Tools

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).

Preview

PDF (1807.08506) - Published Version
Available under License Creative Commons Attribution.
Download (5MB) | Preview

Abstract

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:	http://www.scopus.com/inward/record.url?... https://arxiv.org/abs/1807.08506v5
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

Downloads per month over past year

Actions (login required)

View Item