FO logic on cellular automata orbits equals MSO logic
Guillaume Theyssier
TL;DR
This work extends cellular automata to arbitrary labeled graphs and proves a tight equivalence between FO logic on CA orbits and MSO logic, with effective translations in both directions. This unifies symbolic dynamics and MSO theory, enabling transfer of decidability/undecidability results and clarifying the status of domino problems on Cayley graphs through fixed FO formulas. The results include a complete characterization of FO model checking on Cayley graphs (decidable exactly for virtually free groups), undecidability of fixed FO properties on finite graphs, and the expression of the domino problem and its variants as FO model checking problems, including non-arithmetical cases on $\mathbb{Z}^2$. The paper thus provides a new framework for studying CA on graphs via MSO and lays out several avenues for further exploration in the analytic hierarchy and group-theoretic contexts.
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 Z^2.