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 EmersonClarke 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.
展开▼
