Moshe Y. Vardi
Rice University
Lecture 1
Lecture 2
Lecture 3
Lecture 4
Lecture 5
The automata-theoretic approach to design verification uses the theory of automata as a unifying paradigm for design specification, verification, and synthesis. Both designs and specifications are in essence descriptions of computations. These computations can be viewed as words or trees over some alphabet. Thus, designs and specifications can be viewed as descriptions of languages over some alphabet. The automata-theoretic perspective considers the relationships between designs and their specifications as relationships between languages. By translating design and logical specifications to automata, questions about programs and their specifications can be reduced to questions about automata. More specifically, questions such as satisfiability of specifications and correctness of designs with respect to their specifications can be reduced to questions such as non-emptiness and containment of automata.
Unlike classical automata theory, which focused on automata on finite objects, the applications to design specification, verification, and synthesis, use automata on infinite objects, since the computations in which we are interested are typically infinite. The course will provide an introduction to the theory of automata on infinite objects and demonstrates its applications to design specification, verification, and synthesis.