On Decidability Properties of One-Dimensional Cellular Automata

In a recent paper Sutner proved that the first-order theory of the phase-space S-A = (Q(Z),->) of a one-dimensional cellular automaton A whose configurations are elements of Q(Z), 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 actuallly the case. We first show that, for each one-dimensional cellular automaton A, the phase-space S-A is an omega-automatic structure. Then, applying recent results of Kuske and Lohrey on omega-autoniatic structures, it follows that the first-order theory, extended with some counting and cardinality quantifiers, of the structure S-A, 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.