Processing math: 100%

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 ω-words extended with the second-order predicate U1(X) which says that the distance between consecutive positions in a set XN 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.


    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 1768 times.
    This article's PDF has been downloaded 302 times.