On Decidability Properties of One-Dimensional Cellular Automata
Olivier Finkel
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 [15]. 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 [7] 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.