Reasoning about concurrent programs with simplified temporal logics
J. Srinivasan · 1992
Temporal logic is a formalism that is well suited to describing the behaviour of ongoing concurrent programs. There has been much interest in automating reasoning about the correctness of such programs using the satisfiability and validity problems of temporal logic. However, the complexity of these problems is exponential time or worse for all extant temporal logics. In this thesis, we consider temporal logics with a restricted syntax and show that useful mechanical reasoning can be done efficiently. We exhibit a temporal logic, SCTL (Simplified Computation Tree Logic), whose satisfiability problem is efficiently decidable, in quadratic time, and which is useful for reasoning about an interesting class of programs, the history-free ones. It follows from our results that the method proposed by Emerson & Clarke to mechanically synthesize concurrent programs from temporal specifications is decidable in polynomial time for history-free programs. We go on to present a quadratic time algorithm for the validity of inference problem for SCTL and show how it can be used to automate the verification of program correctness properties. We also study the limits of efficient temporal reasoning for arbitrary programs. We consider temporal logics which permit conjunctions of such important kinds of program assertions as initiality, safety, liveness, succession, and precedence. By suppressing the role the boolean connectives play in determining lower bounds on the complexity of decision procedures for temporal logics, we show that some of these classes of programs properties are efficiently decidable in general. However, a finite line separates such tractable classes from intractable ones, and there are certain combinations of temporal operators which cannot be efficiently decided. Finally, we extend SCTL to an indexed temporal logic, Indexed SCTL, which permits quantifications over the constituent processes of a program. Thus, we can specify programs with arbitrarily many similar processes. With a view to automating the synthesis of such programs, we pose two new decision problems for indexed temporal logics: almost always satisfiability and almost always unsatisfiability. We show that both these problems can be decided in exponential time for Indexed SCTL, and, in fact, every Indexed SCTL specification is either almost always satisfiable, i.e., it can be realized by a concurrent program with arbitrarily many processes, or is almost always unsatisfiable, i.e., no program with more than a certain number (which is determined by our decision procedure) of processes can realize the specification. We also show how these results could be used to automate the synthesis of a program that meets a desired Indexed SCTL specification which is almost always satisfiable.