SCS Undergraduate Thesis Topics

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