The Complexity of Temporal Logic Model Checking.

Abstract

Introduction Temporal logic. Logical formalisms for reasoning about time and the timing of events appear in several elds: physics, philosophy, linguistics, etc. Not surprisingly, they also appear in computer science, a eld where logic is ubiquitous. Here temporal logics are used in automated reasoning, in planning, in semantics of programming languages, in arti cial intelligence, etc. There is one area of computer science where temporal logic has been unusually successful: the speci cation and veri cation of programs and systems, an area we shall just call \\programming" for simplicity. In today's curricula, thousands of programmers rst learn about temporal logic in a course on model checking! Temporal logic and programming. Twenty ve years ago, Pnueli identi ed temporal logic as a very convenient formal language in which to state, and reason about, the behavioral properties of parallel programs and more generally reactive systems [76, 77]. Indeed, correctness for these system