2026-07-23T19:13:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20297 2024-07-02T07:52:56Z ddc:004 open_access

FO Logic on Cellular Automata Orbits Equals MSO Logic Theyssier, Guillaume MSO logic FO logic cellular automata domino problem Cayley graphs 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 ℤ². Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guillaume Theyssier 2024 Is Part Of LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2024.154 urn:nbn:de:0030-drops-202972 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.154 eng https://creativecommons.org/licenses/by/4.0/legalcode