Regular Model Checking and Verification of Cellular Automata
Authors
Byg, Joakim ; Jørgensen, Kenneth Yrke
Term
2. term
Education
Publication year
2008
Pages
99
Abstract
Regular Model Checking er en metode til at verificere systemer med uendeligt mange mulige tilstande eller parametre ved hjælp af regulære sprog og endelige transducere (maskiner, der omsætter strenge). I denne tilgang beskrives systemets konfigurationer som regulære sprog, og overgangsrelationen modelleres med en transducer. Metoden bruges til at besvare sikkerhedsspørgsmål (om en bestemt konfiguration kan nås eller undgås) og liveness-spørgsmål (om alle beregninger til sidst når en given konfiguration). Cellulære automater er modeller for systemer med lokal kommunikation og bruges bl.a. til at beskrive valg-algoritmer, kunstigt liv og biltrafik. Specialet har to hoveddele: (1) vi gennemgår grundlaget for Regular Model Checking og beviser tre resultater om metodens udtrykskraft (hvad den kan beskrive og verificere), og (2) vi undersøger cellulære automater, relationerne mellem forskellige typer af dem, og viser hvordan automater i vilkårlig størrelse kan analyseres med Regular Model Checking. Vi udfører desuden flere eksperimenter for at afprøve vores prototype, der automatisk oversætter en cellulær automat til et Regular Model Checking-setup.
Regular Model Checking is a technique for verifying systems with infinitely many possible states or parameters, using regular languages and finite-state transducers (machines that transform strings). In this approach, system configurations are encoded as regular languages, and the transition relation is modeled by a transducer. The method answers safety questions (whether a given configuration can be reached or avoided) and liveness questions (whether all computations eventually reach a given configuration). Cellular Automata model systems with local communication and are used, for example, to describe election algorithms, artificial life, and traffic. The thesis has two main parts: (1) we present the foundations of Regular Model Checking and prove three results about its expressiveness (what it can represent and verify), and (2) we study Cellular Automata, the relationships between different types, and how automata of arbitrary size can be analyzed using Regular Model Checking. We also report experiments that test our prototype, which automatically translates a Cellular Automaton into a Regular Model Checking framework.
[This abstract was generated with the help of AI]
Documents