The temporal logic of branching time

ABSTRACT

A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either along one path or along all paths. Consequently it is possible to express in this system all the properties that were previously expressible in linear time or branching time systems. We present an exponential decision procedure for satisfiability in the language based on tableaux methods, and a complete deduction system. As associated temporal semantics is illustrated for both structured and graph representation of programs.

REFERENCES

• 1: Karl R. Abrahamson, Modal Logic of Concurrent Nondeterministic Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.21-33, July 02-04, 1979
• 2: Karl Raymond Abrahamson, Decidability and expressiveness of logics of processes, 1980
• 3: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 4: {EC} E. A. Emerson and E. M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, TR-04-80, Aiken Computation Laboratory, Harvard.
• 5: Robert W. Floyd, Nondeterministic Algorithms, Journal of the ACM (JACM), v.14 n.4, p.636-644, Oct. 1967 [doi>10.1145/321420.321422]
• 6: {FL} M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences 18(2), 1979, 194-211.
• 7: 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]
• 8: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 9: {HKP} D. Harel, D. Kozen and R. Parikh, Process logic: expressiveness, decidability, completeness, 21th Symposium on Foundations of Computer Science, 1980.
• 10: {HC} G. E. Hughes and M. J. Cresswell, An Introduction to Modal Logic, Methuen, London, 1968.
• 11: 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]
• 12: {M1} Z. Manna, Mathematical theory of partial correctness, Symposium on Semantics of Algorithmic Languages, Lecture Notes in Mathematics 188, Springer Verlag, Berlin, 1971, 252-269.
• 13: Zohar Manna, Second-order mathematical theory of computation, Proceedings of the second annual ACM symposium on Theory of computing, p.158-168, May 04-06, 1970, Northampton, Massachusetts, United States [doi>10.1145/800161.805161]
• 14: Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
• 15: Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
• 16: V. R. Pratt, A practical decision method for propositional dynamic logic (Preliminary Report), Proceedings of the tenth annual ACM symposium on Theory of computing, p.326-337, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804362]
• 17: {RU} N. Rescher and A. Urquhart, Temporal Logic, Springer-Verlag, Vienna, 1971.
• 18: {S} R. M. Smullyan, First-Order Logic, Springer-Verlag, Berlin, 1968.