On Decidability Properties of One-Dimensional Cellular Automata
In a recent paper Sutner proved that the first-order theory of the phase-space SA = (QZ,−→ ) of a one-dimensional cellular automaton A whose configurations are elements of QZ, for a finite set of states Q, and where−→is the “next configuration relation”, is decidable . He asked whether this result could be extended to a more expressive logic. We prove in this paper that this is actually the case. We first show that, for each one-dimensional cellular automaton A, the phase-space SA is an ω-automatic structure. Then, applying recent results of Kuske and Lohrey on ω-automatic structures, it follows that the first-order theory, extended with some counting and cardinality quantifiers, of the structure SA, is decidable. We give some examples of new decidable properties for one-dimensional cellular automata. In the case of surjective cellular automata, some more efficient algorithms can be deduced from results of  on structures of bounded degree. On the other hand we show that the case of cellular automata give new results on automatic graphs.
Keywords: One-dimensional cellular automaton; space of configurations; ω- automatic structures; first order theory; cardinality quantifiers; decidability properties; surjective cellular automaton; automatic graph; reachability relation.