A master thesis from Aalborg University
Regular Model Checking and Verification of Cellular Automata
Author(s)
Term
2. term
Education
Publication year
2008
Submitted on
2008-06-10
Pages
99 pages
Abstract
Regular Model Checking is a method for verification of infinite-state and parametric systems via regular languages and finite-state transducers. The configurations of the system are modelled using regular languages and the transition relation of the system is modelled with a transducer. Regular model checking is used to verify questions of the type, can we reach or avoid a given configuration (safety), or does all computations from each configuration reach a given configuration (liveness).% and so verify the correctness of a model. Cellular Automata is a model for describing state systems with local communication. Cellular Automata are used e.g. to model election algorithms, artificial life and car traffic. The contribution of this thesis is divided into two main areas. First we, show the basics of regular model checking, then prove three results concerning the expressiveness of regular model checking. Secondly, we deal with Cellular Automata, the relation between different types of Cellular Automata and how we can analyse the behaviour of Cellular Automata of arbitrary size with regular model checking. We carry out a number of experiments to test our prototype implementation, that can automatically convert a Cellular Automaton into a regular model checking framework.
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.