An Automata-Theoretic Approach to Linear Temporal Logic

12 years 3 months ago
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...
Moshe Y. Vardi
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 1995
Authors Moshe Y. Vardi
Comments (0)