Skip to main content
SpringerLink
Log in

Automated temporal reasoning about reactive systems

  • Chapter
  • First Online:
Logics for Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1043))

Abstract

There is a growing need for reliable methods of designing correct reactive systems such as computer operating systems and air traffic control systems. It is widely agreed that certain formalisms such as temporal logic, when coupled with automated reasoning support, provide the most effective and reliable means of specifying and ensuring correct behavior of such systems. This paper discusses known complexity and expressiveness results for a number of such logics in common use and describes key technical tools for obtaining essentially optimal mechanical reasoning algorithms. However, the emphasis is on underlying intuitions and broad themes rather than technical intricacies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Anderson, H. R., Verification of Temporal Properties of Concurrent Systems, Ph. D. Dissertation, Computer Science Department, Aarhus Univ., Denmark, June 1993.

    Google Scholar 

  2. Aggarwal S., Kurshan R. P., Sabnani K. K., “A Calculus for Protocol Specification and Validation”, in Protocol Specification, Testing and Verification III, H. Ruden, C. West (ed.'s), North-Holland 1983, 19–34.

    Google Scholar 

  3. Apt, K. and Kozen, D., Limits for Automatic Verification of Finite State Systems, IPL vol. 22, no. 6., pp. 307–309, 1986.

    Google Scholar 

  4. Barringer, H., Fisher, M., Gabbay, D., Gough, G., and Owens, R., Metatem: A Framework for Programming in Temporal Logic. In Proc. of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, Mook, The Netherlands, Springer LNCS, no. 430, June 1989.

    Google Scholar 

  5. Barringer, H., Kuiper, R., and Pnueli, A., Now You May Compose Temporal Logic Specifications, STOC84.

    Google Scholar 

  6. Barringer, H., Kuiper, R., and Pnueli, A., A Really Abstract Concurrent Model and its Temporal Logic, pp. 173–183, POPL86.

    Google Scholar 

  7. Ben-Ari, M., Pnueli, A. and Manna, Z. The Temporal Logic of Branching Time. Acta Informatica vol. 20, pp. 207–226, 1983.

    Article  Google Scholar 

  8. Bernholtz, O., and Grumberg G., Branching Time Temporal Logic and Amorphous Automata, Proc. 4th Conf. on Concurrency Theory, Hildesheim, Springer LNCS no. 715, pp. 262–277, August 1993.

    Google Scholar 

  9. Bradfield, J., and Stirling, C., “Local Model Checking for Infinite State Spaces”, Theor. Comp. Sci., vol. 96, pp. 157–174, 1992.

    Article  Google Scholar 

  10. Browne, M., Clarke, E. M., and Dill, D. Checking the Correctness of sequential Circuits, Proc. 1985 IEEE Int. Conf. Comput. Design, Port Chester, NY pp. 545–548

    Google Scholar 

  11. Browne, M., Clarke, E. M., and Dill, D., and Mishra, B., Automatic verification of sequential circuits using Temporal Logic, IEEE Trans. Comp. C-35(12), pp. 1035–1044, 1986

    Google Scholar 

  12. Bryant, R., Graph-based algorithms for boolean function manipulation, IEEE Trans. on Computers, C-35(8), 1986.

    Google Scholar 

  13. Buchi, J. R., On a Decision Method in restricted Second Order Arithmetic, Proc. 1960 Inter. Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11.

    Google Scholar 

  14. Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic, Logics of Programs Workshop, IBM Yorktown Heights, New York, Springer LNCS no. 131., pp. 52–71, May 1981.

    Google Scholar 

  15. Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent System Using Temporal Logic, 10th ACM Symp. on Principles of Prog. Lang., Jan. 83; journal version appears in ACM Trans. on Prog. Lang. and Sys., vol. 8, no. 2, pp. 244–263, April 1986.

    Article  Google Scholar 

  16. Clarke, E. M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993.

    Google Scholar 

  17. Clarke, E. M., Grumberg, O., and Brown, M., Characterizing Kripke Structures in Temporal Logic, Theor. Comp. Sci., 1988

    Google Scholar 

  18. Clarke, E. M., Grumberg, O. and Browne, M.C., Reasoning about Networks with Many Identical Finite State Processes, Proc. 5th ACM PODC, pp. 240–248, 1986.

    Google Scholar 

  19. Clarke, E. M. and Grumberg, O., Avoiding the State Explosion Problem In Temporal Model Checking, PODC87.

    Google Scholar 

  20. Clarke, E. M. and Grumberg, O. Research on Automatic Verification of Finite State Concurrent Systems, Annual Reviews in Computer Science, 2, pp. 269–290, 1987

    Article  Google Scholar 

  21. Clarke, E. M., Mishra, B., Automatic Verification of Asynchronous Circuits, CMU Logics of Programs Workshop, Springer LNCS #164, pp. 101–115, May 1983.

    Google Scholar 

  22. Clarke, E. M., Grumberg, O., and Brown, M., Reasoning about Many Identical Processes, Inform. and Comp., 1989

    Google Scholar 

  23. Cleaveland, R. and Steffan, B., A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-calculus, Formal Methods in System Design, vol. 2, no. 2, pp. 121–148, April 1993.

    Article  Google Scholar 

  24. Cleaveland, R., Analyzing Concurrent Systems using the Concurrency Workbench, Functional Programming, Concurrency, Simulation, and Automated Reasoning Springer LNCS no. 693, pp. 129–144, 1993.

    Google Scholar 

  25. Courcoubetis, C., Vardi, M. Y., and Wolper, P. L., Reasoning about Fair Concurrent Programs, Proc. 18th STOC, Berkeley, Cal., pp. 283–294, May 86.

    Google Scholar 

  26. Coudert, O., and Madre, J. C., Verifying Temporal Properties of Sequential Machines without building their State Diagrams, Computer Aided Verification '90, E. M. Clarke and R. P. Kurshan, eds., DIMACS, Series, pp. 75–84, June 1990.

    Google Scholar 

  27. Dams, D., Grumberg, O., and Gerth, R., Generation of Reduced Models for checking fragments of CTL, CAV93, Springer LNCS no. 697, 1993.

    Google Scholar 

  28. Dijkstra, E. W., A Discipline of Programming, Prentice-Hall, 1976.

    Google Scholar 

  29. Dill, D. and Clarke, E.M., Automatic Verification of Asynchronous Circuits using Temporal Logic, IEEE Proc. 133, Pt. E 5, pp. 276–282, 1986.

    Google Scholar 

  30. Emerson, E. A., Branching Time Temporal Logics and the Design of Correct Concurrent Programs, Ph. D. Dissertation, Division of Applied Sciences, Harvard University, August 1981.

    Google Scholar 

  31. Emerson, E. A., Alternative Semantics for Temporal Logics, Theor. Comp. Sci., v. 26, pp. 121–130, 1983.

    Article  Google Scholar 

  32. E.A. Emerson, “Automata, Tableaux, and Temporal Logics”, Proc. Workshop on Logics of Programs, Brooklyn College, pp. 79–87, Springer LNCS no. 193, June 1985.

    Google Scholar 

  33. Emerson, E. A., and Clarke, E. M., Characterizing Correctness Properties of Parallel Programs as Fixpoints. Proc. 7th Int. Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science #85, Springer-Verlag, 1981.

    Google Scholar 

  34. Emerson, E. A., and Clarke, E. M., Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, vol. 2, pp. 241–266, Dec. 1982.

    Article  Google Scholar 

  35. Emerson, E. A., Evangelist, M., and Srinivasan, J., On the Limits of Efficient Temporal Satisfiability, Proc. of the 5th Annual IEEE Symp. on Logic in Computer Science, Philadelphia, pp. 464–477, June 1990.

    Google Scholar 

  36. Emerson, E. A., and Halpern, J. Y., Decision Procedures and Expressiveness in the Temporal Logic of Branching Time, Journal of Computer and System Sciences, vol. 30, no. 1, pp. 1–24, Feb. 85.

    Google Scholar 

  37. Emerson, E. A., and Halpern, J. Y., 'sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time Temporal Logic, JACM, vol. 33, no. 1, pp. 151–178, Jan. 86.

    Google Scholar 

  38. Emerson, E. A. and Jutla, C. S., “Complexity of Tree Automata and Modal Logics of Programs”, Proc. 29th IEEE Foundations of Computer Sci., 1988

    Google Scholar 

  39. Emerson, E. A., and Jutla, C. S., On Simultaneously Determinizing and Complementing ω-automata, Proceedings of the 4th IEEE Symp. on Logic in Computer Science (LICS), pp. 333–342, 1989.

    Google Scholar 

  40. Emerson, E. A., and Jutla, C. S. “Tree Automata, Mu-Calculus, and Determinacy”, Proc. 33rd IEEE Symp. on Found. of Comp Sci., 1991

    Google Scholar 

  41. Emerson, E. A., Jutla, C. S., and Sistla, A. P., On Model Checking for Fragments of the Mu-calculus, Proc. of 5th Inter. Conf. on Computer Aided Verification, Elounda, Greece, Springer LNCS no. 697, pp. 385–396, 1993.

    Google Scholar 

  42. Emerson, E. A., and Lei, C.-L., Efficient Model Checking in Fragments of the Mu-calculus, IEEE Symp. on Logic in Computer Science (LICS), Cambridge, Mass., June, 1986.

    Google Scholar 

  43. Emerson, E. A., and Lei, C.-L.m Modalities for Model Checking: Branching Time Strikes Back, pp. 84–96, ACM POPL85; journal version appears in Sci. Comp. Prog. vol. 8, pp 275–306, 1987.

    Google Scholar 

  44. Emerson, E. A., and Sistla, A. P., Symmetry and Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993full version to appear in Formal Methods in System Design.

    Google Scholar 

  45. Emerson, E. A., and Sistla, A. P., Deciding Full Branching Time Logic, Proc. of the Workshop on Logics of Programs, Carnegie-Mellon University, Springer LNCS no. 164, pp. 176–192, June 6–8, 1983; journal version appears in Information & Control, vol. 61, no. 3, pp. 175–201, June 1984.

    Google Scholar 

  46. Emerson, E. A., Sadler, T. H., and Srinivasan, J. Efficient Temporal Reasoning, pp 166–178, 16th ACM POPL, 1989.

    Google Scholar 

  47. Emerson, E. A., Uniform Inevitability is Finite Automaton Ineffable, Information Processing Letters, v. 24, pp. 77–79, 30 January 1987.

    Article  Google Scholar 

  48. Emerson, E. A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, vol. B, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.

    Google Scholar 

  49. Fischer, M. J., and Ladner, R. E., Propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194–211, 1979.

    Google Scholar 

  50. Francez, N., Fairness, Springer-Verlag, New York, 1986

    Google Scholar 

  51. Gabbay, D., Pnueli A., Shelah, S., Stavi, J., On The Temporal Analysis of Fairness, 7th Annual ACM Symp. on Principles of Programming Languages, 1980, pp. 163–173.

    Google Scholar 

  52. German, S. M. and Sistla, A. P. Reasoning about Systems with many Processes, Journal of the ACM, July 1992, Vol 39, No 3, pp 675–735.

    Google Scholar 

  53. Gurevich, Y., and Harrington, L., “Trees, Automata, and Games”, 14th ACM STOC, 1982.

    Google Scholar 

  54. Hafer, T., and Thomas, W., Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree, ICALP87. Knowledge and Common Knowledge in a Distributed Environment, Proc. 3rd ACM Symp. PODC, pp. 50–61.

    Google Scholar 

  55. Halpern, J. Y. and Shoham, Y., A Propositional Modal Logic of Time Intervals, IEEE LICS, pp. 279–292, 1986.

    Google Scholar 

  56. Harel, D., Dynamic Logic: Axiomatics and Expressive Power, PhD Thesis, MIT, 1979; also available in Springer LNCS Series no. 68, 1979.

    Google Scholar 

  57. Harel, D., Dynamic Logic, in Handbook of Philosophical Logic vol. II: Extensions of Classical Logic, ed. D. Gabbay and F. Guenthner, D. Reidel Press, Boston, 1984, pp. 497–604. Applications, 16th STOC, pp. 418–427, May 84.

    Google Scholar 

  58. Hart, S., and Sharir, M., Probabilistic Temporal Logics for Finite and Bounded Models, 16th STOC, pp. 1–13, 1984.

    Google Scholar 

  59. Hart, S. and Sharir, M. Probabilistic Temporal Logics for Finite and Bounded Models, 16th ACM STOC, pp. 1–13, 1984.

    Google Scholar 

  60. Hoare, C. A. R., Communicating Sequential Processes, CACM, vol. 21, no. 8, pp. 666–676, 1978.

    Google Scholar 

  61. Hailpern, B., Verifying Concurrent Processes Using Temporal Logic, Springer-Verlag LNCS no. 129, 1982.

    Google Scholar 

  62. Hailpern, B. T., and Owicki, S. S., Verifying Network Protocols Using Temporal Logic, In Proceedings Trends and Applications 1980: Computer Network Protocols, IEEE Computer Society, 1980, pp. 18–28.

    Google Scholar 

  63. Hossley, R., and Rackoff, C., The Emptiness Problem For Automata on Infinite Trees, Proc. 13th IEEE Symp. Switching and Automata Theory, pp. 121–124, 1972.

    Google Scholar 

  64. Ip, C-W. N., Dill, D. L., Better Verification through Symmetry, CHDL, April 1993.

    Google Scholar 

  65. Jensen, K., Colored Petri Nets: Basic Concepts, Analysis Methods, and Practical Use, vol. 2: Analysis Methods, EATCS Monographs, Springer-Verlag, 1994.

    Google Scholar 

  66. Jensen, K., and Rozenberg, G. (eds.), High-level Petri Nets: Theory and Application, Springer-Verlag, 1991.

    Google Scholar 

  67. Kamp, Hans, Tense Logic and the Theory of Linear Order, PhD Dissertation, UCLA 1968.

    Google Scholar 

  68. Koymans, R., Specifying Message Buffers Requires Extending Temporal Logic, PODC87.

    Google Scholar 

  69. Kozen, D., Results on the Propositionnai Mu-Calculus, Theor. Comp. Sci., pp. 333–354, Dec. 83

    Google Scholar 

  70. Kozen, D. and Parikh, R. An Elementary Proof of Completeness for PDL, Theor. Comp. Sci., v. 14, pp. 113–118, 1981

    Article  Google Scholar 

  71. Kozen, D., and Parikh, R. A Decision Procedure for the Propositional Mu-calculus, Proc. of the Workshop on Logics of Programs, CarnegieMellon University, Springer LNCS no. 164, pp. 176–192, June 6–8, 1983.

    Google Scholar 

  72. Kozen, D. and Tiuryn, J., Logics of Programs, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.

    Google Scholar 

  73. Kurshan, R. P., ”Testing Containment of omega-regular Languages”, Bell Labs Tech. Report 1121-861010-33 (1986); conference version in R. P. Kurshan, ”Reducibility in Analysis of Coordination”, LNCIS 103 (1987) Springer-Verlag 19–39.

    Google Scholar 

  74. Kurshan, R. P., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach Princeton University Press, Princeton, New Jersey 1994.

    Google Scholar 

  75. Ladner, R. and Reif, J. The Logic of Distributed Protocols, in Proc. of Conf. On Theor. Aspects of reasoning about Knowledge, ed. J Halpern, pp. 207–222, Los Altos, Cal., Morgan Kaufmann

    Google Scholar 

  76. Lamport, L., Sometimes is Sometimes “Not Never” — on the Temporal Logic of programs, 7th Annual ACM Symp. on Principles of Programming Languages, 1980, pp. 174–185.

    Google Scholar 

  77. Lamport, L., What Good is Temporal Logic?, Proc. IFIP, pp. 657–668, 1983.

    Google Scholar 

  78. Lehmann. D., Pnueli, A., and Stavi, J., Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, ICALP 1981, LNCS Vol. 115, pp 264–277.

    Google Scholar 

  79. Lehmann, D., and Shelah, S. Reasoning about Time and Chance, Inf. and Control, vol. 53, no. 3, pp. 165–198, 1982.

    Article  Google Scholar 

  80. Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85, pp. 97–107, Jan. 85.

    Google Scholar 

  81. Lichtenstein, O, Pnueli, A.,and Zuck, L. The Glory of the Past, Brooklyn College Conference on Logics of Programs, Springer-Verlag LNCS, June 1985.

    Google Scholar 

  82. Long, D., Browne, A., Clarke, E., Jha, S., Marrero, W., An Improved Algorithm for the Evaluation of Fixpoint Expressions, Proc. of 6th Inter. Conf. on Computer Aided Verification, Stanford, Springer LNCS no. 818, June 1994.

    Google Scholar 

  83. Manna, Z., and Pnueli, A., Verification of Concurrent Programs: The Temporal Framework, in The Correctness Problem in Computer Science, Boyer & Moore (eds.), Academic Press, pp. 215–273, 1982.

    Google Scholar 

  84. Manna, Z. and Pnueli, A., Verification of Concurrent Programs: Temporal Proof Principles, in Proc. of Workshop on Logics of Programs, D. Kozen (ed.), Springer LNCS #131, pp. 200–252, 1981.

    Google Scholar 

  85. Manna, Z. and Pnueli, A., Verification of Concurrent Programs: A Temporal Proof System, Proc. 4th School on Advanced Programming, Amsterdam, The Netherlands, June 82.

    Google Scholar 

  86. Manna, Z. and Pnueli, A., How to Cook a Proof System for your Pet Language, ACM Symp. on Princ. of Prog. Languages, pp. 141–154, 1983.

    Google Scholar 

  87. Manna, Z. and Pnueli, A., Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, Science of Computer Programming, vol. 4, no. 3, pp. 257–290, 1984.

    Article  Google Scholar 

  88. Manna, Z. and Pnueli, A. Specification and Verification of Concurrent Programs by ∀-automata, Proc. 14th ACM POPL, 1987

    Google Scholar 

  89. Manna, Z. and Pnueli, A. A Hierarchy of Temporal Properties, PODC7.

    Google Scholar 

  90. Manna, Z., and Waldinger, R., Is “sometimes” sometimes better than “always”?: Intermittent assertions in proving program correctness, CACM, vol. 21, no. 2, pp. 159–172, Feb. 78

    Google Scholar 

  91. Manna, Z. and Wolper, P. L., Synthesis of Communicating Processes from Temporal Logic Specifications, vol. 6, no. 1, pp. 68–93, Jan. 84.

    Google Scholar 

  92. Manna, Z. and Pnueli, A., Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992

    Google Scholar 

  93. McMillan, K., Symbolic Model Checking: An Approach to the State Explosion Problem, Ph. D. Thesis, Carnegie-Mellon University, 1992.

    Google Scholar 

  94. McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, Vol. 9, 1966.

    Google Scholar 

  95. McNaughton, R. and Pappert, S. Counter-Free automata, MIT Press, 1971.

    Google Scholar 

  96. Mead, C. and Conway, L., Introduction to VLSI Systems, Addison-Wesley, Reading, Mass., 1980.

    Google Scholar 

  97. Meyer, A. R., Weak Monadic Second Order Theory of One Successor is Not Elementarily Recursive, Boston Logic Colloquium, Springer-Verlag Lecture Notes in Math. no. 453, Berlin/New York, 1974.

    Google Scholar 

  98. Mostowski, A. W., Regular Expressions for Infinite Trees and a Standard Form of Automata, Proc. 5th. Symp on Computation Theory, Zaborow, Poland, pp. 157–168, Springer LNCS no. 208, 1984.

    Google Scholar 

  99. Muchnik, A. A., Games on Infinite Trees and Automata with Dead-ends: a New Proof of the Decidability of the Monadic Theory of Two Successors, Semiotics and Information, 24, pp. 17–40, 1984 (in Russian).

    Google Scholar 

  100. Moszkowski, B., Reasoning about Digital Circuits, PhD Thesis, Stanford Univ, 1983.

    Google Scholar 

  101. Muller, D. E., Infinite Sequences and Finite Machines, 4th Ann. IEEE Symp. of Switching Theory and Logical Design, pp. 3–16, 1963.

    Google Scholar 

  102. Nguyen, V., Demers, A., Owicki, S., and Gries, D., A Model and Temporal Proof System for Networks of Processes, Distr. Computing, vol. 1, no. 1, pp 7–25, 1986

    Article  Google Scholar 

  103. Niwinski, D., unpublished manuscript.

    Google Scholar 

  104. Niwinski, D., Fixed Points versus Infinite Generation, Proc. 3rd IEEE Symp. on Logic in Computer Science, pp. 402–409, 1988.

    Google Scholar 

  105. Owicki, S. S., and Lamport, L., Proving Liveness Properties of Concurrent Programs, ACM Trans. on Programming Languages and Syst., Vol. 4, No. 3, July 1982, pp. 455–495.

    Article  Google Scholar 

  106. Pinter, S., and Wolper, P. L., A Temporal Logic for Reasoning about Partially Ordered Computations, Proc. 3rd ACM PODC, pp. 28–37, Vancouver, Aug. 84

    Google Scholar 

  107. Pixley, C., A Computational Theory and Implementation of Sequential Hardware Equivalence, CAV'90 DIMACS series, vol.3 (also DIMACS Tech. Report 90-3 1), eds. R. Kurshan and E. Clarke, June 1990.

    Google Scholar 

  108. Pixley, C., A Theory and Implementation of Sequential Hardware Equivalence, IEEE Transactions on Computer-Aided Design, pp. 1469–1478, vol. 11, no. 12, 1992.

    Article  Google Scholar 

  109. Peterson, G. L., Myths about the Mutual Exclusion Problem, Inform. Process. Letters, vol. 12, no. 3, pp. 115–116, 1981.

    Article  Google Scholar 

  110. Pnueli, A., The Temporal Logic of Programs, 18th annual IEEE-CS Symp. on Foundations of Computer Science, pp. 46–57, 1977.

    Google Scholar 

  111. Pnueli, A., The Temporal Semantics of Concurrent Programs, Theor. Comp. Sci., vol. 13, pp 45–60, 1981.

    Google Scholar 

  112. Pnueli, A., On The Extremely Fair Termination of Probabilistic Algorithms, 15 Annual ACM Symp. on Theory of Computing, 1983, 278–290.

    Google Scholar 

  113. Pnueli, A., In Transition from Global to Modular Reasoning about Concurrent Programs, in Logics and Models of Concurrent Systems, ed. K. R. Apt, Springer, 1984.

    Google Scholar 

  114. Pnueli, A., Linear and Branching Structures in the Semantics and Logics of Reactive Systems, Proceedings of the 12th ICALP, pp. 15–32, 1985.

    Google Scholar 

  115. Pnueli, A., Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends, in Current Trends in Concurrency: Overviews and Tutorials, ed. J. W. de Bakker, W.P. de Roever, and G. Rozenberg, Springer LNCS no. 224, 1986.

    Google Scholar 

  116. A. Pnueli and R. Rosner, On the Synthesis of a Reactive Module, 16th Annual ACM Symp. on Principles of Programing Languages, pp. 179–190, Jan. 1989.

    Google Scholar 

  117. A. Pnueli and R. Rosner, On the Synthesis of an Asynchronous Reactive Module, Proc. 16th Int'l Colloq. on Automata, Languages, and Programming, Stresa, Italy, July, 1989, pp. 652–671, Springer-Verlag LNCS no. 372.

    Google Scholar 

  118. Pratt, V., A Decidable Mu-Calculus, 22nd FOCS, pp. 421–427, 1981.

    Google Scholar 

  119. Prior, A., Past, Present, and Future, Oxford Press, 1967.

    Google Scholar 

  120. Rescher, N., and Urquhart, A., Temporal Logic, Springer-Verlag, 1971.

    Google Scholar 

  121. Queille, J. P., and Sifakis, J., Specification and verification of concurrent programs in CESAR, Proc. 5th Int. Symp. Prog., Springer LNCS no. 137, pp. 195–220, 1982.

    Google Scholar 

  122. Queille, J. P., and Sifakis, J., Fairness and Related Properties in Transition Systems, Acta Informatica, vol. 19, pp. 195–220, 1983.

    Google Scholar 

  123. Rabin, M. O., “Decidability of Second Order Theories and Automata on Infinite Trees”, Trans. AMS, 141(1969), pp. 1–35.

    Google Scholar 

  124. Rabin, M. O., Automata on Infinite Objects and Church's Problem, Conf. Board. of Math. Sciences, Regional Series in Math. no. 13, Amer. Math. Soc., Providence, Rhode Island, 1972.

    Google Scholar 

  125. Rackoff, C., The Emptiness and Complementation Problems for Automata on Infinite Trees, Master's Thesis, EECS Dept, MIT, 1971.

    Google Scholar 

  126. Rescher, N. and Urquhart, A., Temporal Logic, Springer-Verlag, New York, 1971.

    Google Scholar 

  127. de Roever, W. P., Recursive Program Schemes: Semantics and Proof Theory, Math. Centre Tracts no. 70, Amsterdam, 1976.

    Google Scholar 

  128. Safra, S., On the complexity of omega-automata, Proc. 29th IEEE FOCS, pp. 319–327, 1988.

    Google Scholar 

  129. Safra, S., Exponential Determinization for ω-Automata with Strong Fairness Acceptance Condition, Proceedings of the 24th Annual ACM Symposium on the Theory of Computing, pp. 275–282, Victoria, May 1992.

    Google Scholar 

  130. Sistla, A. P., Theoretical Issues in the Design of Distributed and Concurrent Systems, PhD Thesis, Harvard Univ., 1983.

    Google Scholar 

  131. Sistla, A. P., and Clarke, E. M., The Complexity of Propositional Linear Temporal Logic, J. ACM, Vol. 32, No. 3, pp.733–749.

    Google Scholar 

  132. Sistla, A. P., Clarke, E. M., Francez, N., and Meyer, A. R., Can Message Buffers be Axiomatized in Temporal Logic?, Information & Control, vol. 63., nos. 1/2, Oct./Nov. 84, pp. 88–112.

    Google Scholar 

  133. Sistla, A. P., Characterization of Safety and Liveness Properties in Temporal Logic, PODC85.

    Google Scholar 

  134. Sistla, A. P., Vardi, M. Y., and Wolper, P. L., The Complementation Problem for Buchi Automata with Applications to Temporal Logic, Theor. Comp. Sci., v. 49, pp 217–237, 1987.

    Google Scholar 

  135. Schwartz, R., and Melliar-Smith, P. From State Machines to Temporal Logic: Specification Methods for Protocol Standards, IEEE Trans. on Communication, COM-30, 12, pp. 2486–2496, 1982.

    Google Scholar 

  136. Schwartz, R., Melliar-Smith, P. and Vogt, F. An Interval Logic for Higher-Level Temporal Reasoning, Proc. 2nd ACM PODC, Montreal, pp. 173–186, Aug. 83.

    Google Scholar 

  137. Streett, R., Propositional Dynamic Logic of Looping and Converse, PhD Thesis, MIT, 1981; journal version appears in Information and Control 54, 121–141, 1982.

    Google Scholar 

  138. Streett, R., and Emerson, E. A., The Propositional Mu-Calculus is Elementary, ICALP84, pp 465–472, July 84; journal version appears as An Automata Theoretic Decision Procedure for the Propositional Mucalculus, Information and Computation v. 81, no. 3, June 1989.

    Google Scholar 

  139. Stirling, C., and Walker, D., Local Model Checking in the Mu-calculus, pp. 369–383, Springer LNCS no. 351, 1989.

    Google Scholar 

  140. Stirling, C., Modal and Temporal Logics, in Handbook of Logic in Computer Science, (D. Gabbay, ed.) Oxford, 1993

    Google Scholar 

  141. Tarksi, A., A Lattice-Theoretical Fixpoint Theorem and its Applications, Pacific. J. Math., 55, pp. 285–309, 1955.

    Google Scholar 

  142. Thomas, W., Star-free regular sets of omega-sequences, Information and Control, v. 42, pp. 148–156, 1979

    Google Scholar 

  143. Thomas, W., Automata on Infinite objects, in Handbook of Theoretical Computer Science, vol. B, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.

    Google Scholar 

  144. Vardi, M., The Taming of Converse: Reasoning about Two-Way Computations, Proc. Workshop on Logics of Programs, Brooklyn, NY, LNCS no. 193, Springer-Verlag, pp. 413–424, 1985.

    Google Scholar 

  145. Vardi, M., Verification of Concurrent Programs: The Automata-theoretic Framework, Proc. IEEE LICS, pp. 167–176, June 87

    Google Scholar 

  146. Vardi, M. A Temporal Fixpoint Calculus, PC-PL, 1988.

    Google Scholar 

  147. Vardi, M, An Automata-theoretic Approach to Linear Temporal Temporal Logic, this volume.

    Google Scholar 

  148. Vardi, M. and Stockmeyer, L., Improved Upper and Lower Bounds for Modal Logics of Programs, Proc. 17th ACM Symp. on Theory of Computing, pp. 240–251, 1985.

    Google Scholar 

  149. Vardi, M. and Wolper, P., Yet Another Process Logic, in Proc. CMU Workshop on Logics of Programs, Springer LNCS no. 164, pp. 501–512, 1983.

    Google Scholar 

  150. Vardi, M. and Wolper, P., Automata Theoretic Techniques for Modal Logics of Programs, STOC 84; journal version in JCSS, vol. 32, pp. 183–221, 1986.

    Google Scholar 

  151. Vardi, M., and Wolper, P., An Automata-theoretic Approach to Automatic Program Verification, Proc. IEEE LICS, pp. 332–344, 1986.

    Google Scholar 

  152. Wolper, P., Temporal Logic can be More Expressive, FOCS 81; journal version in Information and Control, vol. 56, nos. 1–2, pp. 72–93, 1983.

    Article  Google Scholar 

  153. Wolper, P., Synthesis of Communicating Processes from Temporal Logic Specifications, Ph.D. Thesis, Stanford Univ., 1982.

    Google Scholar 

  154. Wolper, P., The Tableau Method for Temporal Logic: An Overview, Logique et Analyse, v. 28, June-Sept. 85, pp. 119–136, 1985.

    Google Scholar 

  155. Wolper, P., Expressing Interesting Properties of Programs in Propositional Temporal Logic, ACM Symp. on Princ. of Prog. Lang., pp. 184–193, 1986.

    Google Scholar 

  156. Wolper, P., On the Relation of Programs and Computations to Models of Temporal Logic, in Temporal Logic and Specification, Springer-Verlag LNCS no. 398, April 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Texas at Austin, 78712, Austin, Tx, USA

    E. Allen Emerson

Authors
  1. E. Allen Emerson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Faron Moller Graham Birtwistle

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Emerson, E.A. (1996). Automated temporal reasoning about reactive systems. In: Moller, F., Birtwistle, G. (eds) Logics for Concurrency. Lecture Notes in Computer Science, vol 1043. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60915-6_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-60915-6_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60915-5

  • Online ISBN: 978-3-540-49675-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation