"Sometimes" and "not never" revisited: on branching versus linear time (preliminary report)

ABSTRACT

Temporal logic ([PR57], [PR67]) provides a formalism for describing the occurrence of events in time which is suitable for reasoning about concurrent programs (cf. [PN77]). In defining temporal logic, there are two possible views regarding the underlying nature of time. One is that time is linear: at each moment there is only one possible future. The other is that time has a branching, tree-like nature: at each moment, time may split into alternate courses representing different possible futures. Depending upon which view is chosen, we classify (cf. [RU71]) a system of temporal logic as either a linear time logic in which the semantics of the time structure is linear, or a system of branching time logic based on the semantics corresponding to a branching time structure. The modalities of a temporal logic system usually reflect the semantics regarding the nature of time. Thus,in a logic of linear time, temporal operators are provided for describing events along a single time path (cf. [GPSS80]). In contract, in a logic of branching time the operators reflect the branching nature of time by allowing quantification over possible futures cf. [AB80],[EC80]).

Some controversy has arisen in the computer science community regarding the differences between and appropriateness of branching versus linear time temporal logic. In a landmark paper [LA80] intended to "clarify the logical foundations of the application of temporal logic to concurrent programs," Lamport addresses these issues. He defines a single language based on the temporal operators "always" and "sometimes". Two distinct interpretations for the language are given. In the first interpretation formulae make assertions about paths, whereas in the second interpretation they make assertions about states. Lamport associates the former with linear time and the latter with branching time (although it should be noted that in both cases the underlying time structures are branching). He then compares the expressive power of linear time and branching time logic. Based on his comparison and other arguments, he concludes that, while branching time logic is suitable for reasoning about nondeterministic programs, linear time logic is preferable for reasoning about concurrent programs.

In this paper, we re-examine Lamport's arguments and reach somewhat different conclusions. We first point out some technical difficulties with the formalism of [LA80]. For instance, the definition of expressive equivalence leads to paradoxical situations where satisfiable formulae are classified as equivalent to false. Moreover, the proofs of the results comparing expressive power do not apply in the case of structures generated by a binary relation like those used in the logics of [FL79] and [BMP81]. We give a more refined basis for comparing expressive power that avoids these technical difficulties. It does turn out that expressibility results corresponding to Lamport's still hold. However, it should be emphasized that these results apply only to the two particular systems that he defines. Sweeping conclusions regarding branching versus linear time logic in general are not justified on this basis.

We will argue that there are several different aspects to the problem of designing and reasoning about concurrent programs. While the specific modalities needed in a logic depend on the precise nature of the purpose for which it is intended, we can make some general observations regarding the choice between a system of branching or linear time. We believe that linear time logics are generally adequate for verifying the correctness of pre-existing concurrent programs. For verification purposes, we are typically interested in properties that hold of all computation paths. It is thus satisfactory to pick an arbitrary path and reason about it. However, there are applications where we need the ability to assert the existence of alternative computation paths as provided by a branching time logic. This arises from the nondeterminism - beyond that used to model concurrency - present in many concurrent programs. In order to give a complete specification of such a program, we must ensure that there are viable computation path a corresponding to the nondeterministic choices the program might make. (An example is given in section 6.) Neither of Lamport's systems is entirely adequate for such applications.

In order to examine these issues more carefully, we define a language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion. CTL* is an extension of the Computation Tree Logic, CTL, defined in [CE81] and studied in [EH82]. This language subsumes both of Lamport's interpretations and allows us to compare branching with linear time. Moreover, the syntax of CTL* makes it clear which interpretation is intended.

The paper is organized as follows: In section 2 we summarize Lamport's approach and discuss its limitation. In section 3 we present the syntax and semantics of CTL*. We also define some natural sublanguages of CTL* and compare their expressive power in Section 4. In particular, we show that (cf. Theorem 4.1) a language substantially less expressive than CTL* still subsumes both of Lamport's interpretations. Section 5 then shows how CTL* can be embedded in MPL [AB80] and PL [HKP80]. Finally, section 6 concludes with a comparison of the utility of branching and linear time logic.

REFERENCES

• 1: Karl Raymond Abrahamson, Decidability and expressiveness of logics of processes, 1980
• 2: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 3: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 4: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 5: E. Allen Emerson , Edmund M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.169-181, July 14-18, 1980
• 6: E. A Emerson, Using Branching Time Logic to Synthesize Synchronization Skeletons, University of Texas at Austin, Austin, TX, 1982
• 7: E. Allen Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.169-180, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802190]
• 8: E. A Emerson, Alternative Semantics for Temporal Logics, University of Texas at Austin, Austin, TX, 1981
• 9: {FL79} Fischer, M. J., and Ladner, R. E, propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194-211, 1979.
• 10: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 11: {HA82} Halpern, J. Y., Deterministic Process Logic is Elementary, to appear in FOCS, 1982.
• 12: Brent T. Hailpern , Susan S. Owicki, Verifying network protocols using temporal logic, Stanford University, Stanford, CA, 1980
• 13: {HKP80} Harel, D., Kozen, D., and Parikh, R., Process Logic: Expressiveness, Decidability, and Completeness, 12th Annual ACM Symp. on Theory of Computing, 1980.
• 14: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 15: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, Logic of Programs, Workshop, p.253-281, May 01, 1981
• 16: {0L80}1 Owicki, S., and Lamport, L., Proving Liveness Properties of Concurrent Programs, Computer Systems Laboratory, Stanford Univ., 1980.
• 17: {PN77} Pnueli, A., The Temporal Logic of Programs, 19th Annual Symp. on Foundations of Computer Science, 1977.
• 18: {PN81} Pnueli, A., The Temporal Logic of Concurrent Programs, Theoretical Computer Science, V13, pp. 45-60, 1981.
• 19: {PR57} Prior, A., Time and Modality, Oxford Univ. Press, London, 1957.
• 20: {PR67} Prior, A., Past, Present, and Future, Oxford Univ. Press, London, 1967.
• 21: {RU71} Rescher, N., and Urquhart, A., Temporal Logic, Springer-Verlag, Berlin, 1971.
• 22: {WO81} Wolper, P., Temporal Logic can be more Expressive, 22nd Annual Symp. on Foundations of Computer Science, 1981.
• 23: Pierre Wolper, Specification and synthesis of communicating processes using an extended temporal logic: (preliminary version), Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.20-33, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582156]