Undecidability of a weak version of MSO+U
Logic in Computer Science
2023-06-22 v5
Abstract
We prove the undecidability of MSO on -words extended with the second-order predicate which says that the distance between consecutive positions in a set is unbounded. This is achieved by showing that adding to MSO gives a logic with the same expressive power as , 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 such that for some positive integer , ultimately either both or none of positions and belong to .
Cite
@article{arxiv.1807.08506,
title = {Undecidability of a weak version of MSO+U},
author = {Mikołaj Bojańczyk and Laure Daviaud and Bruno Guillon and Vincent Penelle and A. V. Sreejith},
journal= {arXiv preprint arXiv:1807.08506},
year = {2023}
}