2026-07-21T20:01:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24187 2025-11-12T13:34:19Z ddc:004 open_access

On Expansions of Monadic Second-Order Logic with Dynamical Predicates Nieuwveld, Joris Ouaknine, Joël Monadic second-order logic linear recurrence sequences decidability Baker’s theorem Expansions of the monadic second-order (MSO) theory of the structure ⟨ℕ;<⟩ have been a fertile and active area 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 ⟨ℕ;<,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. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Joris Nieuwveld and Joël Ouaknine 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.80 urn:nbn:de:0030-drops-241879 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.80 eng https://creativecommons.org/licenses/by/4.0/legalcode