Automata-Theoretic Model Checking

TRICERATOPS

TriCollege Digital Repository

Automata-Theoretic Model Checking

View Dublin Core Metadata

Title: Automata-Theoretic Model Checking
Author: Dworkin, Lili Anne
Advisor: Lindell, Steven
Department: Haverford College. Dept. of Computer Science
Type: Thesis (B.A.)
Issue Date: 2011
Abstract: When designing hardware or software, it is important to ensure that systems behave correctly. This is particularly crucial for life- or safety-critical systems, in which errors can be fatal. One approach to the formal verification of such designs is to convert both the system and a specification of its correct behavior into mathematical objects. Typically, the system is modeled as a transition system, and the specification as a logical formula. Then we rigorously prove that the system satisfies its specification. This paper explores one of the most successful applications of formal verification, known as model checking, which is a strategy for the verification of finite-state reactive systems. In particular, we focus on the automata-theoretic approach to model checking, in which both the system model and logical specification are converted to automata over infinite words. Then we can solve the model checking problem using established automata-theoretic techniques from mathematical logic. Since this approach depends heavily on the connections between formal languages, logic, and automata, our explanation is guided by a discussion of the relevant theory.
Subject: Finite model theory
Subject: Computer simulation
Subject: Machine theory
Terms of Use: http://creativecommons.org/licenses/by-nc/3.0/us/
Permanent URL: http://hdl.handle.net/10066/7512

Files in this item

Files Description Size Format
2011DworkinL_thesis.pdf Thesis 621.2Kb PDF
2011DworkinL_release.pdf **Archive Staff Only** 73.08Kb PDF

Citation

Dworkin, Lili Anne. "Automata-Theoretic Model Checking". 2011. Available electronically from http://hdl.handle.net/10066/7512.

This item appears in the following Collection(s)

View Dublin Core Metadata

http://creativecommons.org/licenses/by-nc/3.0/us/ Except where otherwise noted, this item's license is described as http://creativecommons.org/licenses/by-nc/3.0/us/