|
 ABSTRACT
Pnueli [15] has recently introduced the idea of using temporal logic [18] as the logical basis for proving correctness properties of concurrent programs. This has permitted an elegant unifying formulation of previous proof methods. In this paper, we attempt to clarify the logical foundations of the application of temporal logic to concurrent programs. In doing so, we will also clarify the relation between concurrency and nondeterminism, and identify some problems for further research.In this paper, we consider logics containing the temporal operators "henceforth" (or "always") and "eventually" (or "sometime"). We define the semantics of such a temporal logic in terms of an underlying model that abstracts the fundamental concepts common to almost all the models of computation which have been used. We are concerned mainly with the semantics of temporal logic, and will not discuss in any detail the actual rules for deducing theorems.We will describe two different temporal logics for reasoning about a computational model. The same formulas appear in both logics, but they are interpreted differently. The two interpretations correspond to two different ways of viewing time: as a continually branching set of possibilities, or as a single linear sequence of actual events. The temporal concepts of "sometime" and "not never" ("not always not") are equivalent in the theory of linear time, but not in the theory of branching time -- hence, our title. We will argue that the logic of linear time is better for reasoning about concurrent programs, and the logic of branching time is better for reasoning about nondeterministic programs.The logic of linear time was used by Pnueli in [15], while the logic of branching time seems to be the one used by most computer scientists for reasoning about temporal concepts. We have found this to cause some confusion among our colleagues, so one of our goals has been to clarify the formal foundations of Pnueli's work.The following section gives an intuitive discussion of temporal logic, and Section 3 formally defines the semantics of the two temporal logics. In Section 4, we prove that the two temporal logics are not equivalent, and discuss their differences. Section 5 discusses the problems of validity and completeness for the temporal logics. In Section 6, we show that there are some important properties of the computational model that cannot be expressed with the temporal operators "henceforth" and "eventually", and define more general operators.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
Krzystof R. Apt. Recursive Assertions and Parallel Progams, 2 October 1979.
|
| |
2
|
Stephen A. Cook. Soundness and Completeness of an Axiom System for Program Verification. SIAM J. Comput. 7, 1 (February 1978), 70-90.
|
| |
3
|
L. Flon and N. Suzuki. Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs. Proceedings of 19th Annual Symp. on Found. of Comp. Sci., IEEE, October, 1978.
|
| |
4
|
R. W. Floyd. Assigning Meanings to Programs. Proc. Symposium on Applied Math., Vol. 19, Amer. Math. Soc., 1967, pp. 19-32.
|
| |
5
|
N. Francez and A. Pnueli. A Proof Method for Cyclic Programs. Proceedings of the 1976 International Conference on Parallel Processing, IEEE, 1976, pp. 235-245.
|
| |
6
|
D. Gabbay, A. Pnueli, S. Shelah and Y. Stavi. Completeness Results for the Future Fragment of Temporal Logic.
|
 |
7
|
|
| |
8
|
David Harel. On the Total Correctness of Nondeterministic Programs. RC 7691, IBM T.J. Watson Research Center, 1979. To appear in Theoretical Computer Science.
|
| |
9
|
L. Lamport. Proving the Correctness of Multiprocess Programs. IEEE Trans. on Software Engineering SE-3, 2 (March 1977), 125-143.
|
| |
10
|
L. Lamport. The 'Hoare Logic' of Concurrent Programs. CSL-79, SRI International, October, 1978.
|
| |
11
|
|
| |
12
|
|
| |
13
|
|
| |
14
|
S. Owicki and D. Gries. An Axiomatic Proof Technique for Parallel Programs. Acta Informatica 6, 4 (1976), 319-340.
|
| |
15
|
A. Pnueli. The Temporal Logic of Programs. 18th Annual Symposium on the Foundations of Computer Science, IEEE, November, 1977.
|
| |
16
|
V. R. Pratt. Semantical Considerations on Floyd-Hoare Logic. 17th Symposium on Foundations of Computer Science, IEEE, October, 1976.
|
| |
17
|
|
| |
18
|
N. Rescher and A. Urquhart. Temporal Logic. Springer-Verlag, New York, 1971.
|
CITED BY 54
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
C Courcoubetis , M Y Vardi , P Wolper, Reasoning about fair concurrent programs, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.283-294, May 28-30, 1986, Berkeley, California, United States
|
|
|
|
|
|
|
|
|
Jean-Michael Helary , Claude Jard , Noël Plouzeau , Michel Raynal, Detection of stable properties in distributed applications, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.125-136, August 10-12, 1987, Vancouver, British Columbia, Canada
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Foto Afrati , Theodore Andronikos , Vassia Pavlaki , Eugenie Foustoucos , Irène Guessarian, From CTL to datalog, Proceedings of the Paris C. Kanellakis memorial workshop on Principles of computing & knowledge: Paris C. Kanellakis memorial workshop on the occasion of his 50th birthday, p.72-85, June 08-08, 2003, San Diego, California, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Van Nguyen , David Gries , Susan Owicki, A model and temporal proof system for networks of processes, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.121-131, January 14-16, 1985, New Orleans, Louisiana, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf