SCS Undergraduate Thesis Topics

2012-2013 | ||

Student | Advisor | Thesis Topic |

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.

Close this window