Model Checking One-Dimensional Cellular Automata
Klaus Sutner
We show that the first order theory of a one-dimensional cellular automaton, construed as a structure with the global map and equality, is decidable. The argument employs bi-infinite versions of Büchi automata that can also be used to demonstrate that the spectra of cellular automata on finite grids are regular. For existential properties our method can be used to produce witnesses.
Keywords: Cellular automaton, first order logic, decidability, first order spectra, model checking.