Document Open Access Logo

On Expansions of Monadic Second-Order Logic with Dynamical Predicates

Authors Joris Nieuwveld , Joël Ouaknine

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.80.pdf
  • Filesize: 0.83 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.MFCS.2025.80.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
  • Mathematics of computing → Discrete mathematics
Keywords
  • Monadic second-order logic
  • linear recurrence sequences
  • decidability
  • Baker’s theorem

Metrics

Abstract

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.

Cite As Get BibTex

Joris Nieuwveld and Joël Ouaknine. On Expansions of Monadic Second-Order Logic with Dynamical Predicates. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 80:1-80:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.80

Author Details

Joris Nieuwveld
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Ouaknine, Joël: Also affiliated with Keble College, Oxford as https://www.emmy.network/ Fellow, and supported by ERC grant DynAMiCs (101167561) and DFG grant 389792660 as part of https://perspicuous-computing.science.

References

  1. Rajab Aghamov, Christel Baier, Toghrul Karimov, Joël Ouaknine, and Jakob Piribauer. Linear dynamical systems with continuous weight functions. In HSCC, pages 22:1-22:11. ACM, 2024. URL: https://doi.org/10.1145/3641513.3650173.
  2. Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. The orbit problem for parametric linear dynamical systems. In CONCUR, volume 203 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.28.
  3. Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell. On the decidability of monadic second-order logic with arithmetic predicates. In LICS, pages 11:1-11:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662119.
  4. Achim Blumensath. Monadic Second-Order Model Theory. http://www.fi.muni.cz/~blumens/, 2024. [Online; accessed on 24 January 2025].
  5. Émile M. Borel. Les probabilités dénombrables et leurs applications arithmétiques. Rendiconti del Circolo Matematico di Palermo (1884-1940), 27(1):247-271, 1909. Google Scholar
  6. J. Richard Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Studies in Logic and the Foundations of Mathematics, volume 44, pages 1-11. Elsevier, 1966. Google Scholar
  7. Yann Bugeaud. Distribution modulo one and Diophantine approximation, volume 193. Cambridge University Press, 2012. Google Scholar
  8. Olivier Carton and Wolfgang Thomas. The monadic theory of morphic infinite words and generalizations. Information and Computation, 176(1):51-65, 2002. URL: https://doi.org/10.1006/INCO.2001.3139.
  9. Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, and James Worrell. The pseudo-reachability problem for diagonalisable linear dynamical systems. In MFCS, volume 241 of LIPIcs, pages 40:1-40:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.MFCS.2022.40.
  10. Artūras Dubickas and Min Sha. Positive density of integer polynomials with some prescribed properties. Journal of Number Theory, 159:27-44, 2016. Google Scholar
  11. Calvin C. Elgot and Michael O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. The Journal of Symbolic Logic, 31(2):169-181, 1966. URL: https://doi.org/10.2307/2269808.
  12. Graham Everest, Alf van der Poorten, Igor Shparlinski, and Thomas Ward. Recurrence Sequences. Mathematical Surveys and Monographs. American Mathematical Society, 2003. Google Scholar
  13. Glyn Harman. One hundred years of normal numbers. In Surveys in Number Theory, pages 57-74. AK Peters/CRC Press, 2002. Google Scholar
  14. Toghrul Karimov, Edon Kelmendi, Joris Nieuwveld, Joël Ouaknine, and James Worrell. The power of positivity. In LICS, pages 1-11. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175758.
  15. Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell. What’s decidable about discrete linear dynamical systems? In Principles of Systems Design, volume 13660 of Lecture Notes in Computer Science, pages 21-38. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-22337-2_2.
  16. Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell. What’s decidable about linear loops? Proc. ACM Program. Lang., 6(POPL):1-25, 2022. URL: https://doi.org/10.1145/3498727.
  17. Lauwerens Kuipers and Harald Niederreiter. Uniform distribution of sequences. Courier Corporation, 2012. Google Scholar
  18. Florian Luca, Joël Ouaknine, and James Worrell. Algebraic model checking for discrete linear dynamical systems. In FORMATS, volume 13465 of Lecture Notes in Computer Science, pages 3-15. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15839-1_1.
  19. Eugene M. Matveev. An explicit lower bound for a homogeneous rational linear form in the logarithms of algebraic numbers. II. Izvestiya: Mathematics, 64(6):1217, 2000. Google Scholar
  20. Joël Ouaknine and James Worrell. Positivity problems for low-order linear recurrence sequences. In SODA, pages 366-379. SIAM, 2014. URL: https://doi.org/10.1137/1.9781611973402.27.
  21. Martine Queffélec. Old and new results on normality. Lecture Notes-Monograph Series, pages 225-236, 2006. Google Scholar
  22. Alexander Rabinovich. On decidability of monadic logic of order over the naturals extended by monadic predicates. Information and Computation, 205(6):870-889, 2007. URL: https://doi.org/10.1016/J.IC.2006.12.004.
  23. Alexander Rabinovich and Wolfgang Thomas. Decidable theories of the ordering of natural numbers with unary predicates. In International Workshop on Computer Science Logic, pages 562-574. Springer, 2006. Google Scholar
  24. Aleksei Lvovich Semenov. Logical theories of one-place functions on the set of natural numbers. Mathematics of the USSR-Izvestiya, 22(3):587, 1984. Google Scholar
  25. S. Shelah. The monadic theory of order. Ann. Math., 102:379-419, 1975. Google Scholar
  26. Wolfgang Thomas. Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In Structures in Logic and Computer Science, volume 1261 of Lecture Notes in Computer Science, pages 118-143. Springer, 1997. URL: https://doi.org/10.1007/3-540-63246-8_8.
  27. Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages: Volume 3 Beyond Words, pages 389-455. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
  28. R. Tijdeman, M. Mignotte, and T. N. Shorey. The distance between terms of an algebraic recurrence sequence. J. Reine Angew. Math., 346:63-76, 1984. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact