Advertisement

Branching time temporal logic

  • E. Allen Emerson
  • Jai Srinivasan
Tutorials
Part of the Lecture Notes in Computer Science book series (LNCS, volume 354)

Abstract

Many important parallel computer programs exhibit ongoing behaviour that is characterized naturally in terms of infinite execution traces, which can be organized into “branching” trees, and which reflect the high degree of nondeterminism inherent in parallel computation. In this paper, we give a systematic account of Branching Time Temporal Logics, which provide a formal system for describing and reasoning about the correct behaviour of such programs. Several systems of branching time temporal logic that have appeared in the literature are presented, and significant related issues such as their axiomatizations, and decision procedures for their satisfiability and model checking problems are discussed. The applicability of their axiomatizations to formulate deductive systems of these temporal logics to reason about the correctness of concurrent programs is then described as is that of their decision procedures to the tasks of mechanical synthesis and verification. A comparison of the relative expressive power of these systems of branching time temporal logic is also presented, and their ability to specify important correctness properties of programs, including those that involve fairness, is discussed. Moreover, their expressiveness is related to both, the expressiveness of corresponding linear time temporal logics, as well as that of other standard formalisms such as the monadic second-order theory of many successors and finite-state tree automata. Finally, a comparison is undertaken between branching time temporal logics and linear time ones, particularly with respect to their adequacy for such applications as specifying and reasoning about the correctness of concurrent programs.

Keywords

Modal and Temporal Logic: Branching time temporal logic, linear time temporal logic, dynamic logics, expressiveness, axiomatics, decidability, decision procedures, satisfiability, model checking Logics of Programs: Reasoning about concurrent programs, program specification, program verification, specification of and reasoning about fairness Software Engineering: Specification techniques, mechanical synthesis, automated verification techniques Computational Complexity; Automata Theory: Finite-state automata on infinite objects, tree automata 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. [Ab80]
    Abrahamson, K., Decidability and Expressiveness of Logics of Processes, Ph.D. Thesis, Univ. of Washington, 1980.Google Scholar
  2. [AE89]
    Attie, P.C., E.A. Emerson, Synthesis of Concurrent Systems With Many Similar Sequential Processes, to appear in Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Austin, 1989.Google Scholar
  3. [Br86]
    Browne, M.C., An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic, Proc. Symp. on Logic in Computer Science, Cambridge, pp. 260–266, 1986.Google Scholar
  4. [Bü62]
    Büchi, J.R., On A Decision Method in Restricted Second Order Arithmetic, Logic, Methodology, and Philosophy of Science: Proc. 1960 International Congress, Stanford Univ. Press, 1962.Google Scholar
  5. [BHP81]
    Ben-Ari, M., J.Y. Halpern, A. Pnueli, Finite Models for Deterministic Propositional Dynamic Logic, Proc. 8th Annual International Colloquium on Automata, Languages and Programming, LNCS#115, Springer-Verlag, pp. 249–263, 1981; a revised version entitled Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness, appears in Journal of Computer and System Sciences, vol 25, no. 3, pp. 402–417, 1982.Google Scholar
  6. [BKP84]
    Barringer, H., R. Kuiper, A. Pnueli, Now you may Compose Temporal Logic Specifications, Proc. of the 16th Annual ACM Symp. on Theory of Computing, Washington D.C., pp. 51–63, 1984.Google Scholar
  7. [BMP81]
    Ben-Ari, M., Z. Manna, A. Pnueli, The Temporal Logic of Branching Time, Proc. 8th Annual ACM Symp. on Principles of Programming Languages, Williamsburg, pp. 164–176, 1981; also appeared in Acta Informatica, vol. 20, no. 3, pp. 207–226, 1983.Google Scholar
  8. [CE81]
    Clarke, E.M., E.A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, Proc. of the Workshop on Logics of Programs, Yorktown Heights, D. Kozen, editor, LNCS#131, Springer-Verlag, pp. 52–71, 1981.Google Scholar
  9. [CES83]
    Clarke, E.M., E.A. Emerson, A.P. Sistla, Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Proc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, pp. 117–126, 1983; also appeared in ACM Transactions on Programming Languages and Systems, vol. 8, no. 2, pp. 244–263, 1986.Google Scholar
  10. [CG87]
    Clarke, E.M., O. Grumberg, Avoiding the State Explosion Problem in Temporal Model Checking Algorithms, Proc. of the 6th Annual ACM Symp. on Principles of Distributed Computing, Vancouver, pp. 294–303, 1987.Google Scholar
  11. [CVW86]
    Courcoubetis C., M.Y. Vardi, P. Wolper, Reasoning about Fair Concurrent Programs, Proc. of the 18th Annual ACM Symp. on Theory of Computing, Berkeley, pp. 283–294, 1986.Google Scholar
  12. [deB80]
    de Bakker, J.W., Mathematical Theory of Program Correctness, Prentice-Hall, 1980.Google Scholar
  13. [deR76]
    de Roever, W.P., Recursive Program Schemes: Semantics and Proof Theory, Mathematical Centre Tracts 70, Mathematisch Centrum, Amsterdam, 1976.Google Scholar
  14. [Di76]
    Dijkstra, E.W., A Discipline of Programming, Prentice-Hall, 1976.Google Scholar
  15. [Em81]
    Emerson, E.A., Branching Time Temporal Logic and the Design of Correct Concurrent Programs, Ph.D. Thesis, Harvard University, 1981.Google Scholar
  16. [Em83]
    Emerson, E.A., Alternative Semantics for Temporal Logics, Theoretical Computer Science, vol. 26, no. 1–2, pp. 121–130, 1983.CrossRefGoogle Scholar
  17. [Em85]
    Emerson, E.A., Automata, Tableaux, and Temporal Logics, Proc. Conf. on Logics of Programs, Brooklyn, R. Parikh, editor, LNCS#193, Springer-Verlag, pp. 79–88, 1985.Google Scholar
  18. [Em88]
    Emerson, E.A., Temporal and Modal Logic, manuscript, 1988; to appear in the Handbook of Theoretical Computer Science, J. van Leeuwen, editor, North-Holland.Google Scholar
  19. [EC80]
    Emerson, E.A., E.M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proc. 7th Annual International Colloquium on Automata, Languages and Programming, LNCS#85, Springer-Verlag, pp. 169–181, 1980.Google Scholar
  20. [EC82]
    Emerson, E.A., E.M. Clarke, Using Branching Time Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, vol. 2, pp. 241–266, 1982.CrossRefGoogle Scholar
  21. [EH82]
    Emerson, E.A., J.Y. Halpern, Decision Procedures and Expressiveness in the Temporal Logic of Branching Time, Proc. of the 14th Annual ACM Symp. on Theory of Computing, San Francisco, pp. 169–180, 1982; also appeared in Journal of Computer and System Sciences, vol 30, no. 1, pp. 1–24, 1985.Google Scholar
  22. [EH83]
    Emerson, E.A., J.Y. Halpern, “Sometimes” and “Not Never” Revisited: On Branching versus Linear Time, Proc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, pp. 127–140, 1983; also appeared in Journal ACM, vol 33, no. 1, pp. 151–178, 1986.Google Scholar
  23. [EJ88]
    Emerson, E.A., C.S. Jutla, The Complexity of Tree Automata and Logics of Programs, 29th Annual Symp. on Foundations of Computer Science, White Plains, pp. 328–337, 1988.Google Scholar
  24. [EL85]
    Emerson, E.A., C.L. Lei, Modalities for Model Checking: Branching Time Logic Strikes Back, Proc. 12th Annual ACM Symp. on Principles of Programming Languages, New Orleans, pp. 84–96, 1985; also appeared in Science of Computer Programming, vol. 8, pp. 275–306, 1987.Google Scholar
  25. [EL86]
    Emerson, E.A., C.L. Lei, Temporal Reasoning under Generalized Fairness Constraints, 3rd Annual Symp. on Theoretical Aspects of Computer Science, LNCS#210, Springer-Verlag, pp. 21–36, 1986.Google Scholar
  26. [ES84]
    Emerson, E.A., A.P. Sistla, Deciding Full Branching Time Logic, Information and Control, vol. 61, no. 3, pp. 175–201, 1984; also appeared in Proc. of the 16th Annual ACM Symp. on Theory of Computing, Washington D.C., pp. 14–24, 1984.Google Scholar
  27. [ESS89]
    Emerson, E.A., T.H. Sadler, J. Srinivasan, Efficient Temporal Reasoning (Extended Abstract), to appear in Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Austin, 1989.Google Scholar
  28. [Fl67]
    Floyd, R.W., Assigning Meaning to Programs, Proceedings of Symposia in Applied Mathematics, in Mathematical Aspects of Computer Science, J.T. Schwartz, editor, (American Mathematical Society), vol. 19, pp. 19–32, 1967.Google Scholar
  29. [FL77]
    Fischer, M.J., R.E. Ladner, Propositional Modal Logic of Programs, Proc. of the 9th Annual ACM Symp. on Theory of Computing, Boulder, pp. 286–294, 1977.Google Scholar
  30. [FL79]
    Fischer, M.J., R.E. Ladner, Propositional Dynamic Logic of Regular Programs, Journal of Computer and System Sciences, vol. 18, pp. 194–211, 1979.CrossRefGoogle Scholar
  31. [Fr86]
    Francez, N., Fairness, Springer-Verlag, 1986.Google Scholar
  32. [FK84]
    Francez, N., D. Kozen, Generalized Fair Termination, Proc. 11th Annual ACM Symp. on Principles of Programming Languages, Salt Lake City, pp. 46–53, 1984.Google Scholar
  33. [GPSS80]
    Gabbay, D., A. Pnueli, S. Shelah, J. Stavi, On the Temporal Analysis of Fairness, Proc. 7th Annual ACM Symp. on Principles of Programming Languages, Las Vegas, pp. 163–173, 1980.Google Scholar
  34. [Ha80]
    Hailpern, B., Verifying Concurrent Processes Using Temporal Logic, Ph.D. Thesis, Stanford Univ. Computer Systems Lab Technical Report #195, 1980.Google Scholar
  35. [HC72]
    Hughes, G.E., M.J. Creswell, An Introduction to Modal Logic, Methuen and Co. Ltd., 1972.Google Scholar
  36. [Ho69]
    Hoare, C.A.R., An Axiomatic Basis for Computer Programming, Communications ACM, vol. 12, no. 10, pp. 576–583, 1969.CrossRefGoogle Scholar
  37. [HR72]
    Hossley, R., C. Rackoff, The Emptiness Problem For Automata On Infinite Trees, Proc. 13th IEEE Symp. on Switching and Automata Theory (now called: Symp. on Foundations of Computer Science), pp. 121–124, 1972.Google Scholar
  38. [HT87]
    Hafer, T., W. Thomas, Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree, Proc. 14th Annual International Colloquium on Automata, Languages and Programming, LNCS#267, Springer-Verlag, pp. 269–279, 1987.Google Scholar
  39. [In84]
    Inaba, Y., An Implementation of Synthesis of Concurrent Programs from Branching Time Temporal Logic Specifications, Master's Thesis, Univ. of Texas at Austin, 1984.Google Scholar
  40. [Ka68]
    Kamp, H.W., Tense Logic and the Theory of Linear Order, Ph.D. Thesis, Univ. of California at Los Angeles, 1968.Google Scholar
  41. [Ko82]
    Kozen, D., Results on the Propositional μ-Calculus, Proc. 9th Annual International Colloquium on Automata, Languages and Programming, LNCS#140, Springer-Verlag, pp. 348–359, 1982; also appeared in Theoretical Computer Science, vol. 27, no. 3, pp. 333–354, 1983.Google Scholar
  42. [Kr63]
    Kripke, S.A., A Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi, Zeitschr. f. Math. Logik Grundlagen d. Math., vol. 9, pp. 67–96, 1963.Google Scholar
  43. [La80]
    Lamport, L., “Sometime” is Sometimes “Not Never”—On the Temporal Logic of Programs, Proc. 7th Annual ACM Symp. on Principles of Programming Languages, Las Vegas, pp. 174–185, 1980.Google Scholar
  44. [La83]
    Lamport, L., What Good is Temporal Logic?, Information Processing, vol. 83, pp. 657–668, 1983.Google Scholar
  45. [Lav78]
    Laventhal, M., Synthesis of Synchronization Code for Data Abstractions, Ph.D. Thesis, MIT, 1978.Google Scholar
  46. [LS82]
    Lehmann, D., S. Shelah, Reasoning with Time and Chance, Information and Control, vol. 53, no. 3, pp. 165–198, 1982.CrossRefGoogle Scholar
  47. [LPS81]
    Lehmann, D., A. Pnueli, J. Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proc. 8th Annual International Colloquium on Automata, Languages and Programming, LNCS#115, Springer-Verlag, pp. 262–277, 1981.Google Scholar
  48. [LP85]
    Lichtenstein, O., A. Pnueli, Checking That Finite State Concurrent Programs Satisfy Their Linear Specification, Proc. 12th Annual ACM Symp. on Principles of Programming Languages, New Orleans, pp. 97–107, 1985.Google Scholar
  49. [LPZ85]
    Lichtenstein, O., A. Pnueli, L. Zuck, The Glory of The Past, Proc. Conf. on Logics of Programs, Brooklyn, R. Parikh, editor, LNCS#193, Springer-Verlag, pp. 196–218, 1985.Google Scholar
  50. [McN66]
    McNaughton, R., Testing and Generating Infinite Sequences By a Finite Automaton, Information and Control, vol. 9, pp. 521–530, 1966.Google Scholar
  51. [Me75]
    Meyer, A.R., Weak Monadic Second Order Theory of Successor Is Not Elementary-Recursive, Logic Colloquium, Symposium on Logic Held at Boston in 1972–73, Lecture Notes in Mathematics #453, R. Parikh, editor, Springer-Verlag, pp. 132–154, 1975.Google Scholar
  52. [MP79]
    Manna, Z., A. Pnueli, The Modal Logic of Programs, Proc. 6th Annual International Colloquium on Automata, Languages and Programming, LNCS#71, Springer-Verlag, pp. 385–409, 1979.Google Scholar
  53. [MP81a]
    Manna, Z., A. Pnueli, Verification of Concurrent Programs: The Temporal Framework, in The Correctness Problem in Computer Science, R.S. Boyer and J.S. Moore, editors, Academic Press, pp. 215–273, 1981.Google Scholar
  54. [MP81b]
    Manna, Z., A. Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Proc. of the Workshop on Logics of Programs, Yorktown Heights, D. Kozen, editor, LNCS#131, Springer-Verlag, pp. 200–252, 1981.Google Scholar
  55. [MP82]
    Manna, Z., A. Pnueli, Verification of Concurrent Programs: A Temporal Proof System, Proc. 4th School on Advanced Programming, Amsterdam, Holland, June 1982.Google Scholar
  56. [MP83]
    Manna, Z., A. Pnueli, How to Cook a Proof System for Your Pet Language, Proc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, pp. 141–154, 1983.Google Scholar
  57. [MW78]
    Manna, Z., R. Waldinger, Is “Sometime” Sometimes Bettar Than “Always”? Intermittent Assertions in Proving Program Correctness, Communications ACM, vol. 21, no. 2, pp. 159–172, 1978.CrossRefGoogle Scholar
  58. [MW84]
    Manna, Z., P. Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, vol. 6, no. 1, pp. 68–93, 1984.CrossRefGoogle Scholar
  59. [OL82]
    Owicki, S., L. Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems, vol. 4, no. 3, pp. 455–495, 1982.CrossRefGoogle Scholar
  60. [Pa70]
    Park, D., Fixpoint Induction and Proofs of Program Properties, in Machine Intelligence, vol. 5, D. Mitchie, editor, Edinburgh University Press, 1970.Google Scholar
  61. [Pn77]
    Pnueli, A., The Temporal Logic of Programs, 18th Annual Symp. on Foundations of Computer Science, Providence, pp. 46–57, 1977.Google Scholar
  62. [Pn83]
    Pnueli, A., On the Extremely Fair Treatment of Probabilistic Algorithms, Proc. of the 15th Annual ACM Symp. on Theory of Computing, Boston, pp. 278–290, 1983.Google Scholar
  63. [PR89]
    Pnueli, A., R. Rosner, On the Synthesis of a Reactive Module, to appear in Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Austin, 1989.Google Scholar
  64. [Pr76]
    Pratt, V., Semantical Considerations on Floyd-Hoare Logic, Proc. of the 10th Annual ACM Symp. on Theory of Computing, San Diego, pp. 326–337, 1976.Google Scholar
  65. [Pr80]
    Pratt, V., A Near-Optimal Method For Reasoning About Action, Journal of Computer and System Sciences, vol 20, no. 2, pp. 231–254, 1980.CrossRefGoogle Scholar
  66. [QS81]
    Queille, J.P., J. Sifakis, Specification and Verification of Concurrent Systems in CESAR, Proc. of the 5th International Symposium on Programming, LNCS#137, Springer-Verlag, pp. 337–350, 1981.Google Scholar
  67. [QS83]
    Queille, J.P., J. Sifakis, Fairness and Related Properties in Transition Systems—A Temporal Logic To Deal With Fairness, Acta Informatica, vol. 19, no. 3, pp. 195–220, 1983.CrossRefGoogle Scholar
  68. [Ra69]
    Rabin, M., Decidability of Second-Order Theories and Automata on Infinite Trees, Transactions of the American Mathematical Society, vol. 141, pp. 1–35, 1969.Google Scholar
  69. [RK80]
    Ramamritham, K., R. Keller, Specification and Synthesis of Synchronizers, 9th International Conf. on Parallel Processing, 1980.Google Scholar
  70. [RU71]
    Rescher, N., A. Urquhart, Temporal Logic, Springer-Verlag, 1971.Google Scholar
  71. [Sa88]
    Safra, S., On the Complexity of Ω-Automata, 29th Annual Symp. on Foundations of Computer Science, White Plains, pp. 319–327, 1988.Google Scholar
  72. [SC82]
    Sistla, A.P., E.M. Clarke, The Complexity of Propositional Linear Temporal Logics, Proc. of the 14th Annual ACM Symp. on Theory of Computing, San Francisco, pp. 159–168, 1982; also appeared in Journal ACM, vol. 32, no. 3, pp. 733–749, 1985.Google Scholar
  73. [SG87]
    Sistla, A.P., S.M. German, Reasoning With Many Processes, Proc. 2nd Annual Symp. on Logic in Computer Science, Ithaca, pp. 138–152, 1987.Google Scholar
  74. [Sm68]
    Smullyan, R.M., First-Order Logic, Springer-Verlag, 1968.Google Scholar
  75. [St81]
    Streett, R.S., Propositional Dynamic Logic of Looping and Converse, Ph.D. Thesis, MIT LCS Technical Report TR-263, 1981; alternatively, see: Propositional Dynamic Logic of Looping and Converse is Elementarily Decidable, Information and Control, vol. 54, pp. 121–141, 1982.Google Scholar
  76. [SE84]
    Streett, R.S., E.A. Emerson, The Propositional Mu-Calculus is Elementary, Proc. 11th Annual International Colloquium on Automata, Languages and Programming, LNCS#172, Springer-Verlag, pp. 465–472, 1984.Google Scholar
  77. [VS85]
    Vardi, M., L. Stockmeyer, Improved Upper and Lower Bounds for Modal Logics of Programs, Proc. of the 17th Annual ACM Symp. on Theory of Computing, Providence, pp. 240–251, 1985.Google Scholar
  78. [VW84]
    Vardi M., P. Wolper, Automata Theoretic Techniques for Modal Logics of Programs, Proc. of the 16th Annual ACM Symp. on Theory of Computing, Washington D.C., pp. 446–456, 1984; also appeared in Journal of Computer and System Sciences, vol 32, no. 2, pp. 183–221, 1984.Google Scholar
  79. [VW86]
    Vardi, M., P. Wolper, An Automata-Theoretic Approach to Automatic Program Verification, Proc. Symp. on Logic in Computer Science, Cambridge, pp. 332–345, 1986.Google Scholar
  80. [Wo81]
    Wolper, P., Temporal Logic Can Be More Expressive, 22nd Annual Symp. on Foundations of Computer Science, Nashville, pp. 340–348, 1981; also appeared in Information and Control, vol. 56, pp. 72–99, 1983.Google Scholar
  81. [Wo82]
    Wolper, P., Specification and Synthesis of Communicating Processes Using an Extended Temporal Logic, Proc. 9th Annual ACM Symp. on Principles of Programming Languages, Albuquerque, pp. 20–33, 1982; also see [MW84].Google Scholar
  82. [WVS83]
    Vardi M., P. Wolper, A.P. Sistla, Reasoning about Infinite Computation Paths, 24th Annual Symp. on Foundations of Computer Science, Tucson, pp. 185–194, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • E. Allen Emerson
    • 1
    • 2
  • Jai Srinivasan
    • 1
  1. 1.Department of Computer SciencesThe University of Texas at AustinAustinUSA
  2. 2.Mathematics and Computing Science DepartmentTechnical University of EindhovenEindhovenThe Netherlands

Personalised recommendations