Automata-Theoretic Model Checking

Date
2011
Journal Title
Journal ISSN
Volume Title
Publisher
Producer
Director
Performer
Choreographer
Costume Designer
Music
Videographer
Lighting Designer
Set Designer
Crew Member
Funder
Rehearsal Director
Concert Coordinator
Moderator
Panelist
Alternative Title
Department
Haverford College. Department of Computer Science
Type
Thesis
Original Format
Running Time
File Format
Place of Publication
Date Span
Copyright Date
Award
Language
eng
Note
Table of Contents
Terms of Use
Rights Holder
Access Restrictions
Open Access
Tripod URL
Identifier
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.
Description
Citation
Collections