Computer Science Department
School of Computer Science, Carnegie Mellon University
Model Checking Omega Cellular Automata
Joseph A. Gershenson
The evolution of one-way infinite cellular automata can be described by the firstorder theory of phase-space, which uses one-step evolution as its main predicate. Formulas in this logic can be used to express properties of the global map such as surjectivity. A complete implementation of the decision algorithm is provided, as well as methods for manipulating the Büchi automata on which the decision algorithm relies. Experimental results and a discussion of the tractability of larger problems are presented.