Expansions of the monadic second-order (MSO) theory of the structure ❬N; <❭ have been a fertile and active topic of research ever since the publication of the seminal papers of Büchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of ❬N; <, P❭, where P ranges over a large class of unary "dynamical" predicates, i.e., sets of non-negative values assumed by certain integer linear recurrence sequences. Such predicates are so named in view of their close kinship with discrete-time linear dynamical systems. In turn, our results enable decision procedures for a range of new properties over a wide class of linear dynamical systems.
Submitted, 2025. 11 pages.
PDF
© 2025 Joris Nieuwveld and Joël Ouaknine.