Mikołaj Bojańczyk ; Laure Daviaud ; Bruno Guillon ; Vincent Penelle ; A. V. Sreejith - Undecidability of a weak version of MSO+U

lmcs:5059 - Logical Methods in Computer Science, February 11, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:12)2020
Undecidability of a weak version of MSO+UArticle

Authors: Mikołaj Bojańczyk ; Laure Daviaud ; Bruno Guillon ; Vincent Penelle ; A. V. Sreejith

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


    Volume: Volume 16, Issue 1
    Published on: February 11, 2020
    Accepted on: December 16, 2019
    Submitted on: January 2, 2019
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1590 times.
    This article's PDF has been downloaded 296 times.