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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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
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
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
Floyd, R.W.: Nondeterministic algorithms. J. ACM14(4), 636–644 (1967)
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
Harel, D.: First Order Dynamic Logic, Lecture Notes in Computer Science 68. Berlin, Heidelberg, New York: Springer 1979
Harel, D., Kozen, D., Parikh, R.: Process Logic: expressiveness, decidability, completeness. 21-st IEEE Symposium on Foundation of Computer Science, pp. 129–142, 1980
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
Lamport, L.: “Sometime” is sometimes “not never”. Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NE, pp. 174–183, 1980
Manna, Z.: Second order mathematical theory of computation. Second ACM Symposium on Theory of Computing, pp. 158–168, 1970
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
Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci.13, 45–60 (1981)
Pratt, V.R.: A near optimal method for reasoning about action. J. Comput. Syst. Sci.20, 231–254 (1980)
Prior, A.: Past, Present and Future. Oxford University Press 1967
Rescher, N., Urquhart, A.: Temporal Logic. Berlin, Heidelberg, New York, Wien: Springer 1971
Smullyan, R.M.: First Order Logic. Berlin, Heidelberg, New York: Springer 1968
Author information
Authors and Affiliations
Additional information
Portions of this work are based on the first author's Ph.D. thesis done at the Tel Aviv University under the supervision of the second author. A Preliminary version of this paper was presented at the Eighth ACM Symposium on Principles of Programming Languages, Williamsburg, VA, 1981
This research was supported in part by: NSF under grant MCS-80-6930, Office of Naval Research under grant N000-14-76-C-0687, the United States Air Force Office of Scientific Research under Grant AFOSR-81-0014, and the Israeli Academy of Sciences and Humanities, the Basic Research Foundation
Rights and permissions
About this article
Cite this article
Ben-Ari, M., Pnueli, A. & Manna, Z. The temporal logic of branching time. Acta Informatica 20, 207–226 (1983). https://doi.org/10.1007/BF01257083
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01257083