The 2000 Gödel Prize is awarded to Moshe Vardi and Pierre Wolper for their paper:
Reasoning about infinite computations. Moshe Y. Vardi, Pierre Wolper. Information and Computation 115 (1994), 1-37.
This paper is a reworking and extension of a conference contribution of FOCS'83, which has become a major reference in the automata-theoretic approach to temporal logic. The starting point is an extension of propositional temporal logic (interpreted over infinite sequences), first suggested by Wolper, in which temporal operators are introduced by finite automata. An n-ary temporal operator is defined by a finite automaton whose inputs are n-tuples of truth values (of n given formulas) and which produces a truth value by acceptance or non-acceptance of the given model (an infinite sequence). The resulting "extended temporal logic" ETL turns out to have the same expressive power (allowing the definition of precisely the regular sets of infinite sequences) and are thus strictly more expressive than propositional temporal logic PTL with the operators "next", "eventually", "always", and "until".
The main result of the paper is a translation of ETL into equivalent Buchi automata of exponential size in the length of the given formulas. Such a Buchi automaton is designed to build up a "Hintikka sequence" for the given formula (over an infinite sequence model as input), i.e., it constructs a sequence of tuples of truth values, one truth value for each subformula of the given formula, checking that the semantic relations between these subformulas are respected and that the entire formula is signalled "true" at the start of the input sequence. The Buchi automaton is composed of two automata: the "local automaton" which checks semantic relations between subformulas not referring to the "future", e.g. composed by Boolean connectives from their constituents, and an "eventuality automaton", which guesses truth values of temporal (sub-) formulas and at later points of an input sequence checks that these guesses were correct. The technique was first introduced by the authors for the construction of automata over infinite trees and is transferred here to infinite sequences. As a result, the satisfiability problem for ETL is solvable in polynomial space (in fact, logspace complete for polynomial space). In the final section this result is extended to "alternating temporal logic" (where the automata representing the temporal operators may be alternating).
As mentioned in the paper's introduction, the contribution of the paper is applicable to program verification and program synthesis based on temporal logic. For example, an exponential-time model-checking algorithm may be inferred for finite transition systems with respect to ETL-specifications. The exponential bounds obtained in the paper are in contrast to the much higher (in fact, non-elementary) complexities of the corresponding problems for first-order or monadic second-order logic (which also characterizes the regular languages of infinite sequences but makes it possible to express certain properties much more succinctly).