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.
decidability properties one-dimensional cellular automaton omega-automatic structures cardinality quantifiers automatic graph space of configurations first order theory surjective cellular automaton reachability relation