Automata-Theoretic Approach to Automated Verification


Current Assignments: Assignment 8
Instructors: Amir Pnueli and Moshe Y. Vardi

Location: Ziskind 1

Time: Wednesday, 9:15-12, Oct. 28, 1998 - Feb. 10, 1999

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.

Topics to be covered include:

  • Nondeterministic automata on finite words: closure and algorithms
  • Nondeterministic automata on infinite words: closure and algorithms
  • Alternating automata on infinite words: closure and algorithms
  • Linear temporal logic (LTL) and automata on infinite words
  • Automata-theoretic approach to LTL model checking
  • Algorithmic approaches: enumerative vs. symbolic
  • Complementation and determinization
  • Extensions of linear temporal logic: automata vs. fixpoints
  • From model checking to program verification
  • Computation tree logic (CTL): model checking vs. validity checking
  • Tree automata and CTL
  • CTL vs. LTL
  • From verification to synthesis

  • Reading: There is no textbook that covers the material of the course. Relevant papers will be distributed to the students during the course. In addition, official lecture notes, taken by the students, will be posted on this page.
    Credit: The course carries 3 units of credit. Final grade will be based on:
  • Classroom participation
  • Note taking
  • Assignments
  • Final project

  • Students
    Lecture Notes
    Auxiliary Readings
    Special Accomodation: Any student with a disability requiring a special accomodation in this class is encouraged to contact the instructors.