For which unary predicates P1, …, Pm is the MSO theory of the structure ❬N; <, P1, …, Pm❭ decidable? We survey the state of the art, leading us to investigate combinatorial properties of almost-periodic, morphic, and toric words. In doing so, we show that if each Pi can be generated by a toric dynamical system of a certain kind, then the attendant MSO theory is decidable. We give various applications of toric words, including the recent result of [1] that the MSO theory of ❬N; <, {2n : n∈N}, {3n : n∈N}❭ is decidable.
Theoretical Computer Science 1025, 2024. 16 pages.
PDF
© 2024 Valérie Berthé, Toghrul Karimov, Joris
Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell.