SCS Undergraduate Thesis Topics

Joseph Gershenson Klaus Sutner Model Checking Cellular Automata

Simple aspects of the evolution of one-dimensional cellular automata can be captured by the first-order theory of phasespace, which uses one-step evolution as its main predicate. Formulas in this logic can thus be used to express statements such as "there exists a 3-cycle" or properties of the global map such as surjectivity. Since this theory has been shown to be decidable by using two-way infinite Buchi automata, it is possible to evaluate these formulas by manipulating the Buchi automata. The goal of this research is to build a system which can evaluate these statements, and to report on the results as well as the tractability of larger problems.

Close this window