Automata-Theoretic Model Checking

TriCollege Digital Repository

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:
Permanent URL:

Files in this item

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


Dworkin, Lili Anne. "Automata-Theoretic Model Checking". 2011. Available electronically from

This item appears in the following Collection(s) Except where otherwise noted, this item's license is described as


Advanced Search


My Account