FO Logic on Cellular Automata Orbits Equals MSO Logic

Author Guillaume Theyssier



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.154.pdf
  • Filesize: 0.81 MB
  • 20 pages

Document Identifiers

Author Details

Guillaume Theyssier
  • I2M, CNRS, Université Aix-Marseille, France

Acknowledgements

We thank anonymous referees for their feedback and their suggestions to improve the presentation. We also warmly thank N. Pytheas Fogg for their hints about domino problems on regular graphs and numerous stimulating discussions that inspired this work.

Cite AsGet BibTex

Guillaume Theyssier. FO Logic on Cellular Automata Orbits Equals MSO Logic. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 154:1-154:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.154

Abstract

We introduce an extension of classical cellular automata (CA) to arbitrary labeled graphs, and show that FO logic on CA orbits is equivalent to MSO logic. We deduce various results from that equivalence, including a characterization of finitely generated groups on which FO model checking for CA orbits is undecidable, and undecidability of satisfiability of a fixed FO property for CA over finite graphs. We also show concrete examples of FO formulas for CA orbits whose model checking problem is equivalent to the domino problem, or its seeded or recurring variants respectively, on any finitely generated group. For the recurring domino problem, we use an extension of the FO signature by a relation found in the well-known Garden of Eden theorem, but we also show a concrete FO formula without the extension and with one quantifier alternation whose model checking problem does not belong to the arithmetical hierarchy on group ℤ².

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Logic
  • Theory of computation → Formal languages and automata theory
Keywords
  • MSO logic
  • FO logic
  • cellular automata
  • domino problem
  • Cayley graphs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. S. Amoroso and Y.N. Patt. Decision procedures for surjectivity and injectivity of parallel maps for tessellation structures. Journal of Computer and System Sciences, 6(5):448-464, October 1972. URL: https://doi.org/10.1016/s0022-0000(72)80013-8.
  2. Pablo Arrighi and Gilles Dowek. Causal graph dynamics. Information and Computation, 223:78-93, February 2013. URL: https://doi.org/10.1016/j.ic.2012.10.019.
  3. Pablo Arrighi, Simon Martiel, and Vincent Nesme. Cellular automata over generalized cayley graphs. Mathematical Structures in Computer Science, 28(3):340-383, May 2017. URL: https://doi.org/10.1017/s0960129517000044.
  4. Nathalie Aubrun, Sebastián Barbieri, and Emmanuel Jeandel. About the Domino Problem for Subshifts on Groups, pages 331-389. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-69152-7_9.
  5. Nathalie Aubrun, Sebastián Barbieri, and Etienne Moutot. The Domino Problem is Undecidable on Surface Groups. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 46:1-46:14, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.46.
  6. Alexis Ballier and Maya Stein. The domino problem on groups of polynomial growth. Groups, Geometry, and Dynamics, 12(1):93-105, March 2018. URL: https://doi.org/10.4171/ggd/439.
  7. Laurent Bartholdi. The domino problem for hyperbolic groups, 2023. URL: https://arxiv.org/abs/2305.06952.
  8. Laurent Bartholdi and Ville Salo. Simulations and the lamplighter group. Groups, Geometry, and Dynamics, 16(4):1461-1514, November 2022. URL: https://doi.org/10.4171/ggd/692.
  9. R. Berger. The undecidability of the domino problem. Mem. Amer. Math Soc., 66, 1966. Google Scholar
  10. Elwyn R. Berlekamp, John H. Conway, and Richard K. Guy. Winning Ways for your Mathematical Plays, volume 2. Academic Press, 1982. chapter 25. Google Scholar
  11. Florian Bridoux, Amélia Durbec, Kevin Perrot, and Adrien Richard. Complexity of fixed point counting problems in boolean networks. Journal of Computer and System Sciences, 126:138-164, June 2022. URL: https://doi.org/10.1016/j.jcss.2022.01.004.
  12. T. Ceccherini-Silberstein and M. Coornaert. Cellular automata and groups. Springer Monographs in Mathematics. Springer-Verlag, Berlin, 2010. URL: https://doi.org/10.1007/978-3-642-14034-1.
  13. Bastien Chopard and Michel Droz. Cellular Automata Modeling of Physical Systems. Cambridge University Press, December 1998. URL: https://doi.org/10.1017/cbo9780511549755.
  14. Bruno Courcelle. The monadic second-order logic of graphs, ii: Infinite graphs of bounded width. Mathematical Systems Theory, 21(1):187-221, December 1988. URL: https://doi.org/10.1007/bf02088013.
  15. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation, 85(1):12-75, March 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-h.
  16. Bruno Courcelle. The monadic second order logic of graphs vi: on several representations of graphs by relational structures. Discrete Applied Mathematics, 54(2-3):117-149, October 1994. URL: https://doi.org/10.1016/0166-218x(94)90019-1.
  17. Bruno Courcelle and Joost Engelfriet. Graph structure and monadic second-order logic. A language-theoretic approach. Encyclopedia of Mathematics and its applications, Vol. 138. Cambridge University Press, June 2012. Collection Encyclopedia of Mathematics and Applications, Vol. 138. Google Scholar
  18. Alberto Dennunzio, Enrico Formenti, and Julien Provillard. Non-uniform cellular automata: Classes, dynamics, and decidability. Information and Computation, 215:32-46, June 2012. URL: https://doi.org/10.1016/j.ic.2012.02.008.
  19. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer Berlin Heidelberg, 1995. URL: https://doi.org/10.1007/978-3-662-03182-7.
  20. Louis Esperet, Ugo Giocanti, and Clément Legrand-Duchesne. The structure of quasi-transitive graphs avoiding a minor with applications to the domino problem, 2023. URL: https://doi.org/10.48550/arXiv.2304.01823.
  21. Guilhem Gamard, Pierre Guillon, Kevin Perrot, and Guillaume Theyssier. Rice-Like Theorems for Automata Networks. In Markus Bläser and Benjamin Monmege, editors, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021), volume 187 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1-32:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.32.
  22. Martin Gardner. Mathematical games. Scientific American, 223(4):120-123, October 1970. URL: https://doi.org/10.1038/scientificamerican1070-120.
  23. Walter Gottschalk. Some general dynamical notions, pages 120-125. Springer Berlin Heidelberg, 1973. URL: https://doi.org/10.1007/bfb0061728.
  24. R. Halin. Über unendliche wege in graphen. Mathematische Annalen, 157(2):125-137, April 1964. URL: https://doi.org/10.1007/bf01362670.
  25. David Harel. Recurring Dominoes: Making the Highly Undecidable Highly Understandable, pages 51-71. Elsevier, 1985. URL: https://doi.org/10.1016/s0304-0208(08)73075-5.
  26. G. A. Hedlund. Endomorphisms and Automorphisms of the Shift Dynamical Systems. Mathematical Systems Theory, 3(4):320-375, 1969. Google Scholar
  27. Benjamin Hellouin de Menibus, Victor H. Lutfalla, and Camille Noûs. The Domino Problem Is Undecidable on Every Rhombus Subshift, pages 100-112. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-33264-7_9.
  28. Michael Hochman and Tom Meyerovitch. A characterization of the entropies of multidimensional shifts of finite type. Annals of Mathematics, 171(3):2011-2038, 2010. URL: https://doi.org/10.4007/annals.2010.171.2011.
  29. Jarkko Kari. Reversibility and surjectivity problems of cellular automata. Journal of Computer and System Sciences, 48(1):149-182, February 1994. URL: https://doi.org/10.1016/s0022-0000(05)80025-x.
  30. Jarkko Kari. Rice’s theorem for the limit sets of cellular automata. Theoretical Computer Science, 127(2):229-254, May 1994. URL: https://doi.org/10.1016/0304-3975(94)90041-8.
  31. S.A. Kauffman. Metabolic stability and epigenesis in randomly constructed genetic nets. Journal of Theoretical Biology, 22(3):437-467, March 1969. URL: https://doi.org/10.1016/0022-5193(69)90015-0.
  32. Stephan Kreutzer and Siamak Tazari. On brambles, grid-like minors, and parameterized intractability of monadic second-order logic. In Proceedings of the Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2010, Austin, Texas, USA, January 17-19, 2010, pages 354-364. SIAM, 2010. URL: https://doi.org/10.1137/1.9781611973075.30.
  33. Dietrich Kuske and Markus Lohrey. Logical aspects of cayley-graphs: the group case. Annals of Pure and Applied Logic, 131(1-3):263-286, January 2005. URL: https://doi.org/10.1016/j.apal.2004.06.002.
  34. Douglas Lind and Brian Marcus. An Introduction to Symbolic Dynamics and Coding. Cambridge University Press, December 2020. URL: https://doi.org/10.1017/9781108899727.
  35. Marston Morse and G. A. Hedlund. Symbolic dynamics. Amer. J. Math., 3:286-303, 1936. Google Scholar
  36. David E. Muller and Paul E. Schupp. The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science, 37:51-75, 1985. URL: https://doi.org/10.1016/0304-3975(85)90087-8.
  37. Fabian Reiter. Distributed graph automata. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, July 2015. URL: https://doi.org/10.1109/lics.2015.27.
  38. Adrien Richard. Fixed points and connections between positive and negative cycles in boolean networks. Discrete Applied Mathematics, 243:1-10, July 2018. URL: https://doi.org/10.1016/j.dam.2017.12.037.
  39. Neil Robertson and P.D Seymour. Graph minors. ii. algorithmic aspects of tree-width. Journal of Algorithms, 7(3):309-322, September 1986. URL: https://doi.org/10.1016/0196-6774(86)90023-4.
  40. Neil Robertson and P.D Seymour. Graph minors. v. excluding a planar graph. Journal of Combinatorial Theory, Series B, 41(1):92-114, August 1986. URL: https://doi.org/10.1016/0095-8956(86)90030-4.
  41. H. Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, 1987. Google Scholar
  42. Thomas Schwentick and Klaus Barthelmann. Local normal forms for first-order logic with applications to games and automata, pages 444-454. Springer Berlin Heidelberg, 1998. URL: https://doi.org/10.1007/bfb0028580.
  43. René Thomas. Boolean formalization of genetic control circuits. Journal of Theoretical Biology, 42(3):563-585, December 1973. URL: https://doi.org/10.1016/0022-5193(73)90247-6.
  44. Wolfgang Thomas. On logics, tilings, and automata, pages 441-454. Springer Berlin Heidelberg, 1991. URL: https://doi.org/10.1007/3-540-54233-7_154.