Model Checking Cellular Automata

Klaus Sutner

Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15218
sutner@cs.cmu.edu

Abstract

One-dimensional cellular automata are automatic: when viewed as structures in the sense of first order logic both the carrier set (finite or infinite words) and the next step operation have canonical descriptions in terms of finite state machines.  Thus they are amenable to certain techniques from model checking and have decidable first order theory.  In particular in the finite case the spectra of first order properties are ultimately periodic and one can effectively compute the corresponding truth sets.

Alas, as is often the case in model checking, the associated finite state machines tend to grow exponentially and considerable care is needed to deal with state explosion.  We will discuss a variant of Safra's determinization algorithm that has turned out to be helpful in this regard and compare it to various determinization avoidance methods.  We show how to apply this machinery to the study of elementary cellular automata.