10.23638/LMCS-16(1:12)2020
https://lmcs.episciences.org/5059
Bojańczyk, Mikołaj
Mikołaj
Bojańczyk
Daviaud, Laure
Laure
Daviaud
Guillon, Bruno
Bruno
Guillon
Penelle, Vincent
Vincent
Penelle
Sreejith, A. V.
A. V.
Sreejith
Undecidability of a weak version of MSO+U
We prove the undecidability of MSO on $\omega$-words extended with the
second-order predicate $U_1(X)$ which says that the distance between
consecutive positions in a set $X \subseteq \mathbb{N}$ is unbounded. This is
achieved by showing that adding $U_1$ to MSO gives a logic with the same
expressive power as $MSO+U$, a logic on $\omega$-words with undecidable
satisfiability. As a corollary, we prove that MSO on $\omega$-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$.
episciences.org
Computer Science - Logic in Computer Science
Attribution 4.0 International (CC BY 4.0)
2020-02-11
2020-02-11
2020-02-11
eng
journal article
arXiv:1807.08506
10.48550/arXiv.1807.08506
1860-5974
10.48550/arxiv.1807.08506
https://lmcs.episciences.org/5059/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 16, Issue 1
Researchers
Students