There has been much interest in decision procedures for testing satisfiability in various systems of temporal logic. This is due to the potential applications of these decision procedures to reasoning about the correctness of concurrent programs. In this paper, we exhibit a temporal logic that is both useful in applications to program reasoning and is efficiently decidable in quadratic time. A surprising corollary of our results is that the fragment of CTL (Computation Tree Logic) used by Emerson & Clarke [11] to synthesize concurrent programs from temporal specifications is actually decidable in polynomial time. Our results demonstrate that many useful correctness properties can be expressed with a rather restricted syntax, and provide insight into the relation between the syntactic complexity of temporal logics and the complexity of testing satisfiability.

An analysis is made of the contribution of the temporal operators alone to the complexity of deciding temporal logics by suppressing the role the usual Boolean connectives play in determining lower bounds on the complexity of their decision procedures. Several temporal logics are exhibited which can state many properties useful in describing temporal systems and which restrict combinations of temporal and Boolean operators so as to be decidable in low deterministic polynomial time. It is also shown that relaxing any of the constraints placed on the syntax of these logics results in intractability, thereby demonstrating that there is a fine line separating tractably decidable sets of temporal formulas from intractable ones.>

There has been much interest in decision procedures for testing satisfiability (or validity) of formulae in various systems of Temporal Logic. This is due to the potential applications of such decision procedures to mechanical reasoning about correctness of concurrent programs. We show that there exist Temporal Logics that are (i) decidable in polynomial time, and (ii) still useful in applications. One surprising corollary of our results is that the fragment of CTL (Computation Tree Logic) actually used by Emerson & Clarke [EC82] to synthesize concurrent programs from temporal specifications is decidable in polynomial time. Another is that the verification of many correctness properties of concurrent programs (such as in Owicki & Lamport [OL82]) can be efficiently automated. This demonstrates that many useful correctness properties can be expressed with a rather restricted syntax. Finally, our results provide insight into the relation between the structural (i.e., syntactic) complexity of temporal logics and the complexity of their decision problems.