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 [email protected]