An Automata-Theoretic Approach to Linear Temporal Logic

The automata-theoretic approach to linear temporal logic uses the theory of automata as a unifying paradigm for program specification, verification, and synthesis. Both programs and specifications are in essence descriptions of computations. These computations can be viewed as words over some alphabet. Thus,programs andspecificationscanbe viewedas descriptionsof languagesover some alphabet. The automata-theoretic perspective considers the relationships betweenprograms and their specificationsas relationships between languages.By translating programs and specifications to automata, questionsabout programs and their specificationscanbe reducedto questionsabout automata. More specifically, questions such as satisfiability of specifications and correctness of programs with respect to their specifications can be reduced to questions such as nonemptiness and containment of automata. Unlike classical automata theory, which focused on automata on finite words, the applications to p...

• Type: Conference
• Year: 1995
• Where: BANFF
• Authors: Moshe Y. Vardi
• Keywords: BANFF 1995, Classical Automata Theory, Distributed And Parallel Computing, Program Specification, Reducedto Questionsabout Automata