SCS Undergraduate Thesis Topics
|Adrien Trejo||Klaus Sutner||Classification and Automaticity of Discrete Dynamical Systems|
Model checking is a method of building a model of a system and then exhaustively and automatically checking whether that model meets a given specification. In particular, the system could require infinitary descriptions (e.g., runs of a reactive system).
Elementary cellular automata (ECA) form simple dynamical systems that exhibit a wide array of behaviors, ranging from trivial to computationally complete.
I've built the automata-theoretic support structure to perform model checking on first-order logic formulae on one-way infinite cellular automata. Using these formulae, I separate the 256 different ECAs into distinct behavioral classes.