Computer Science Department
School of Computer Science, Carnegie Mellon University


Model Checking Omega Cellular Automata

Joseph A. Gershenson

May 2010

Masters Thesis


Keywords: Automata theory, cellular automata, model checking, ω-automata

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.

48 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by