Bits of History

For an excellent overview about the history of temporal logic in connection with formal methods see Schneider (2004)[250] and the overview of Manna and Pnueli (1992)[191]:Pp.268ff. Here only a few facts.

The connection of automata theory and temporal logics can be traced back (cf. Thomas 1997 [273],P.389) to original work about automata and monadic second order logic done by Büchi 1960 and Elgot 1961, later extended by Büchi 1962, McNaughton 1966, and Rabin 1969 to automata over infinite words and trees (for an overview see also Thomas 1990 [272]). Pnueli (1977)[229] seems to be the first who used temporal logic for the specification of the behavior of systems. From this time on became monadic second order logic partially replaced during the 80ies by temporal logics, which led to powerful algorithms for the verification of finite state programs by model checking (cf. Clarke and Emerson 1981 [66] as well as Quielle and Sifakis 1981 [238]).