Institutional Scholarship

Automata-Theoretic Model Checking

Show simple item record

dc.contributor.advisor Lindell, Steven
dc.contributor.author Dworkin, Lili Anne
dc.date.accessioned 2011-09-29T13:33:27Z
dc.date.available 2011-09-29T13:33:27Z
dc.date.issued 2011
dc.identifier.uri http://hdl.handle.net/10066/7512
dc.description.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.
dc.description.sponsorship Haverford College. Department of Computer Science
dc.language.iso eng
dc.rights.uri http://creativecommons.org/licenses/by-nc/3.0/us/
dc.subject.lcsh Finite model theory
dc.subject.lcsh Computer simulation
dc.subject.lcsh Machine theory
dc.title Automata-Theoretic Model Checking
dc.type Thesis
dc.rights.access Open Access


Files in this item

This item appears in the following Collection(s)

Show simple item record

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/

Search


Browse

My Account