×
Ben-Ari, Mordechai; Pnueli, Amir; Manna, Zohar

The temporal logic of branching time. (English) Zbl 0533.68036

Acta Inf. 20, 207-226 (1983).
Summary: A temporal logic is defined which contains both linear and branching operators. The underlying model is the tree of all possible computations. The following metatheoretical results are proven: 1) an exponential decision procedure for satisfiability; 2) a finite model property; 3) the completeness of an axiomatization.

Cited in 1 Review
Cited in 48 Documents

MSC:

68Q65 Abstract data types; algebraic specification
03B60 Other nonclassical logic

Keywords:

reasoning about programs; temporal logic; branching operators; tree of all possible computations; exponential decision procedure for satisfiability; finite model property; completeness of an axiomatization
PDF BibTeX XML Cite
\textit{M. Ben-Ari} et al., Acta Inf. 20, 207--226 (1983; Zbl 0533.68036)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[1] Abrahamson, K.R.: Modal logic of concurrent nondeterministic programs. Symposium on Semantics of Concurrent Computations, Lecture Notes in Computer Science 70, pp. 21-33. Berlin, Heidelberg, New York: Springer 1979 · Zbl 0402.68010
[2] Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. Eight ACM Symposium on Principles of Programming Languages, Williamsburg, VA, pp. 164-176, 1981 · Zbl 0533.68036
[3] Emerson, A.E., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. 14-th ACM Symposium on Theory of Computing, San Francisco, CA, pp. 169-180, 1982
[4] Floyd, R.W.: Nondeterministic algorithms. J. ACM14(4), 636-644 (1967) · Zbl 0153.47006
[5] Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: The temporal analysis of fairness. Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NE, pp. 163-173, 1980
[6] Harel, D.: First Order Dynamic Logic, Lecture Notes in Computer Science 68. Berlin, Heidelberg, New York: Springer 1979 · Zbl 0403.03024
[7] Harel, D., Kozen, D., Parikh, R.: Process Logic: expressiveness, decidability, completeness. 21-st IEEE Symposium on Foundation of Computer Science, pp. 129-142, 1980
[8] Kröger, A.: A uniform logical basis for the description, specification and verification of programs. IFIP Working Conference on Formal Description of Programming Concepts, St. Andrews, Canada, 1977 · Zbl 0373.68026
[9] Lamport, L.: ?Sometime? is sometimes ?not never?. Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NE, pp. 174-183, 1980
[10] Manna, Z.: Second order mathematical theory of computation. Second ACM Symposium on Theory of Computing, pp. 158-168, 1970
[11] Manna, Z., Pnueli, A.: The modal logic of programs. Automata, Languages and Programming, Lecture Notes in Computer Science 79, pp. 385-409. Berlin, Heidelberg, New York: Springer 1979 · Zbl 0404.68011
[12] Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci.13, 45-60 (1981) · Zbl 0441.68010
[13] Pratt, V.R.: A near optimal method for reasoning about action. J. Comput. Syst. Sci.20, 231-254 (1980) · Zbl 0424.03010
[14] Prior, A.: Past, Present and Future. Oxford University Press 1967 · Zbl 0169.29802
[15] Rescher, N., Urquhart, A.: Temporal Logic. Berlin, Heidelberg, New York, Wien: Springer 1971 · Zbl 0229.02027
[16] Smullyan, R.M.: First Order Logic. Berlin, Heidelberg, New York: Springer 1968 · Zbl 0172.28901
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.