Skip to main content
SpringerLink
Log in

On the relation of programs and computations to models of temporal logic

  • Collected Papers
  • Conference paper
  • First Online:
Temporal Logic in Specification

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

Abstract

In recent years there has been a proliferation of program verification methods that use temporal logic. These methods differ by the version of temporal logic they are based upon and by the way they use this logic. In this paper we attempt to give a simple, unified and coherent view of the field. For this, we first characterize the models and model generators of different versions of temporal logic using automata theory. From this characterization, we build a classification of verification and synthesis methods that use temporal logic.

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. S. Aggarwal, C. Courcoubetis, P. Wolper, “Adding Liveness Properties to Coupled Finite-State Machines”, to appear.

    Google Scholar 

  2. B. Alpern, F. Schneider, “Verifying Temporal Properties Without Using Temporal Logic”, Technical Report TR 85-723, Dept. of Computer Science, Cornell University, December 1985.

    Google Scholar 

  3. B. Alpern, F. Schneider, “Proving Boolean Combinations of Deterministic Properties”, Proc. Symp. on Logic in Computer Science, Ithaca, June 1987, pp. 131–137.

    Google Scholar 

  4. M. Ben-Ari, Z. Manna, A. Pnueli, “The Logic of Nexttime”, Eighth ACM Symposium on Principles of Programming Languages, Williamsburg, January 1981, pp. 164–176.

    Google Scholar 

  5. H. Barringer, R. Kuiper, A. Pnueli, “Now You May Compose Temporal Logic Specifications”, Proc. 16th ACM Symp. on Theory of Computing, Washington, April 1984, pp. 51–63.

    Google Scholar 

  6. H. Barringer, R. Kuiper, A. Pnueli. “A Compositional Temporal Approach to a CSP-like Language”, Proceedings of the IFIP Working Conference “The Role of Abstract Models in Information Processing”, E.J. Neuhold and G. Chroust, editors, North Holland, Vienna, 1985, pp. 207–227.

    Google Scholar 

  7. H. Barringer, R. Kuiper, A. Pnueli, “A Really Abstract Concurrent Model and its Temporal Logic”, Proceedings of the Thirteenth ACM Symposium on the Principles of Programming Languages, St. Petersberg Beach, Florida, January 1986, pp. 173–183.

    Google Scholar 

  8. J. R. Büchi, “On a Decision Method in Restricted Second Order Arithmetic”, Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, Stanford University Press, 1962, pp. 1–12.

    Google Scholar 

  9. E. M. Clarke, E. A. Emerson, “Synthesis of Synchronization Skeletons from Branching Time Temporal Logic”, Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, NY, Lecture Notes in Computer Science vol. 131, Springer-Verlag, Berlin, 1982, pp. 52–71.

    Google Scholar 

  10. E. M. Clarke, E. A. Emerson, A. P. Sistla, “Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications: A Practical Approach”, Proc. of the 10th ACM Symposium on Principles of Programming Languages, Austin, January 1984, pp. 117–126.

    Google Scholar 

  11. E. M. Clarke, E. A. Emerson, A. P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications”, ACM Transactions on Programming Languages and Systems, vol. 8, no. 2 (1986), pp. 244–263.

    Google Scholar 

  12. E.M. Clarke, O. Grumberg, M.C. Browne, “Reasoning about Networks with Many Identical Finite-State Processes”, Proc. 5th ACM Symp. on Principles of Distributed Computing, Minaki, Ontario, August 1985, pp. 240–248.

    Google Scholar 

  13. C. Courcoubetis, M. Y. Vardi, P. Wolper, “Reasoning about Fair Concurrent Programs”, Proc. 18th Symp. on Theory of Computing, Berkeley, May 1986, pp. 283–294.

    Google Scholar 

  14. E. A. Emerson, E. M. Clarke, “Using Banching Time Logic to Synthesize Synchronization Skeletons”, Science of Computer Programming, 2 (1982), pp. 241–266.

    Google Scholar 

  15. E. A. Emerson, J. Y. Halpern, “Decision Procedures and Expressiveness in the Temporal Logic of Branching Time”, Journal of Computer and System Sciences, 30 (1985), pp. 1–24.

    Google Scholar 

  16. E.A. Emerson, J.Y. Halpern, ““Sometimes” and “Not Never” Revisited: On Branching versus Linear Time Temporal Logic”, Journal of the ACM, vol. 33, no. 1 (1986), pp. 151–178.

    Google Scholar 

  17. E. A. Emerson, Ching-Laung Lei, “Temporal Model Checking under Generalized Fairness Constraints”, Proc. 18th Hawaii International Conference on System Sciences, 1985.

    Google Scholar 

  18. E. A. Emerson, Ching-Laung Lei, “Modalities for Model Checking: Branching Time Strikes Back”, Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, January 1985, pp. 84–96.

    Google Scholar 

  19. E. A. Emerson, “Automata, Tableaux and Temporal Logics”, Proc. Workshop on Logic of Programs, Brooklyn 1985, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, pp. 79–88.

    Google Scholar 

  20. E. A. Emerson, A. P. Sistla, “Deciding Branching Time Logic”, Information and Control, 61 (1984), pp. 175–201.

    Google Scholar 

  21. N. Francez, Fairness, Springer-Verlag, Berlin, 1986.

    Google Scholar 

  22. D. Gabbay, A. Pnueli, S. Shelah and J. Stavi, “The Temporal Analysis of Fairness”, Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, January 1980, pp. 163–173.

    Google Scholar 

  23. J. Halpern, Z. Manna, B. Moszkowski, “A Hardware Semantics Based on Temporal Intervals”, Proc. 10th International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science, vol. 154, Springer-Verlag, Berlin, 1983.

    Google Scholar 

  24. Y. Kornatsky, S. S. Pinter, “A Model Checker for Partial Order Temporal Logic”, EE PUB no. 597, Department of Electrical Enginering, Technion-Israel Institute of Technology, June 1986.

    Google Scholar 

  25. S. Katz, D. Peled, “Interleaving Set Temporal Logic”, Proc. 6th ACM Symp. on Principles of Distributed Computing, Vancouver, August 1987, pp. 178–190.

    Google Scholar 

  26. L. Lamport, “Sometimes is Sometimes Not Never”, Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NV, January 1980, pp. 174–185.

    Google Scholar 

  27. O. Lichtenstein, A. Pnueli, “Checking that Finite State Concurrent Programs Satisfy their Linear Specifications”, Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, January 1985, pp. 97–107.

    Google Scholar 

  28. O. Lichtenstein, A. Pnueli, L. Zuck, “The Glory of the Past”, Proc. Workshop on Logic of Programs, Brooklyn 1985, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, pp. 196–218.

    Google Scholar 

  29. R. Milner, “A Calculus of Communicating Systems”, Lecture Notes in Computer Science, vol. 92, Springer-Verlag, Berlin, 1980.

    Google Scholar 

  30. B. Moszkowski, “Reasoning about Digital Circuits”, Ph.D. Thesis, Department of Computer Science, Stanford University, July 1983.

    Google Scholar 

  31. Z. Manna, A. Pnueli, “Verification of Concurrent Programs: the Temporal Framework”, The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, eds., International Lecture Series in Computer Science, Academic Press, London, 1981, pp. 215–273.

    Google Scholar 

  32. Z. Manna, A. Pnueli, “How to Cook a Temporal Proof System for your Pet Language, Proc. of the 10th ACM Symposium on Principles of Programming Languages, Austin, January 1984, pp. 141–154.

    Google Scholar 

  33. Z. Manna, A. Pnueli, “Proving Properties: the Temporal Way”, Proc. 10th International Colloquium on Automata Languages and Programming, Lecture Notes in Computer Science, vol. 154, Springer-Verlag, Berlin, 1983, pp. 491–512.

    Google Scholar 

  34. Z. Manna, A. Pnueli, “Verification of Concurrent Programs: A Temporal Proof System”, Foundations of Computer Science IV, J. W. deBakker, J. Van Leeuwen, Eds., Mathematical Center Tracts, vol. 159, Amsterdam, 1983, pp. 163–225.

    Google Scholar 

  35. Z. Manna, A. Pnueli, “Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs”, Science of Computer Programming, 4 (1984), pp. 257–289.

    Google Scholar 

  36. Z. Manna, A. Pnueli, “Specification and Verification of Concurrent Programs by ∀-Automata”, Proc. 14th ACM Symp. on Principles of Programming Languages, Munich, January 1987, pp. 1–12.

    Google Scholar 

  37. Z. Manna, P. Wolper, “Synthesis of Communicating Processes from Temporal Logic Specifications”, ACM Transactions on Programming Languages and Systems, vol. 6, no. 1, January 1984, pp. 68–93.

    Google Scholar 

  38. V. Nguyen, D. Gries, S. Owicki, “A Model and Temporal Proof System for Networks of Processes”, Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, January 1985, pp. 121–131.

    Google Scholar 

  39. S. Owicki, L. Lamport, “Proving Liveness Properties of Concurrent Programs”, ACM Transactions on Programming Languages and Systems, vol. 4, no. 3, 1982, pp. 455–496.

    Google Scholar 

  40. A. Pnueli, “The Temporal Logic of Programs”, Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, RI, November 1977, pp. 46–57.

    Google Scholar 

  41. A. Pnueli, “The Temporal Logic of Concurrent Programs”, Theoretical Computer Science, 13(1981), pp. 45–60.

    Google Scholar 

  42. V. R. Pratt, “On the Composition of Processes”, Ninth Symposium on Principles of Programming Languages, Albuquerque, January 1982, pp. 213–223.

    Google Scholar 

  43. S.S. Pinter, P. Wolper, “A Temporal Logic for Reasoning about Partially Ordered Computations”, Proc. 3rd ACM Symposium on Principles of Distributed Computing, Vancouver, August 1984, pp. 28–37.

    Google Scholar 

  44. A. Pnueli, L. Zuck, “Probabilistic Verification by Tableaux”, Proc. Symp. on Logic in computer Science, Cambridge, June 1986, pp. 322–331.

    Google Scholar 

  45. M. O. Rabin, “Decidability of Second Order Theories and Automata on Infinite Trees”, Transactions of American Mathematical Society, vol. 141, July 1969, pp. 1–35.

    Google Scholar 

  46. M. O. Rabin, “Weakly Definable Relations and Special Automata”, Proc. Symp. on Mathematical Logic and Foundations of Set Theory, Y. Bar-Hillel, ed., North Holland, Amsterdam, 1970, pp. 1–23.

    Google Scholar 

  47. A.P. Sistla, “Theoretical Issues in the Design and Verification of Distributed Systems”, PhD thesis, Harvard University, Harvard, 1983.

    Google Scholar 

  48. A. P. Sistla, E. M. Clarke, “The Complexity of Propositional Linear Temporal Logic”, Proceedings of the 14th ACM Symposium on Theory of Computing, San Francisco, CA, May 1982, pp. 159–168.

    Google Scholar 

  49. A. P. Sistla, E. M. Clarke, “The Complexity of Propositional Linear Temporal Logics”, Journal of the ACM, vol. 32, no. 3, July 1985, pp. 733–749.

    Google Scholar 

  50. R. L. Schwartz, P. M. Melliar-Smith, F. H. Vogt, “An Interval Logic for Higher-Level Temporal Reasoning”, Proc. 2nd ACM Symposium on Principles of Distributed Computing, Montreal, Canada, August 1983, pp. 173–186.

    Google Scholar 

  51. A. P. Sistla, M. Y. Vardi, P. Wolper, “The Complementation Problem for Büchi Automata with Applications to Temporal Logic”, Theoretical Computer Science, 49 (1987), pp. 217–237.

    Google Scholar 

  52. M. Vardi, “Automatic Verification of Probabilistic Concurrent Finite-State Programs”, Proc. 26th Symp. on Foundations of Computer Science, Portland, October 1985, pp. 327–338.

    Google Scholar 

  53. M. Vardi, The Taming of Converse: Reasoning about Two-Way Computations”, Proc. Workshop on Logic of Programs, Brooklyn 1985, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, pp. 413–424.

    Google Scholar 

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

    Google Scholar 

  55. M. Y. Vardi, P. Wolper, “Automata-Theoretic Techniques for Modal Logics of Programs”, Journal of Computer and System Science, vol. 32, no. 2 (April 1986), pp. 183–21.

    Google Scholar 

  56. M. Y. Vardi, P. Wolper, “An Automata-Theoretic Approach To Automatic Program Verification”, Proc. Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 322–331.

    Google Scholar 

  57. M. Y. Vardi, P. Wolper, “Reasoning about Infinite Computation Paths”, to appear.

    Google Scholar 

  58. P. Wolper, “Synthesis of Communicating Processes from Temporal Logic Specifications”, Ph.D. Thesis, Stanford University, August 1982.

    Google Scholar 

  59. P. Wolper, “Temporal Logic Can Be More Expressive”, Information and Control, vol. 56, nos. 1–2, 1983, pp. 72–99.

    Google Scholar 

  60. P. Wolper, M. Y. Vardi, A. P. Sistla, “Reasoning about Infinite Computation Paths”, Proc. 24th IEEE Symposium on Foundations of Computer Science, Tucson, 1983, pp. 185–194.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut Montéfiore, Université de Liège, B28, Sart-Tilman, 4000, Liège, Belgium

    Pierre Wolper

Authors
  1. Pierre Wolper
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

B. Banieqbal H. Barringer A. Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wolper, P. (1989). On the relation of programs and computations to models of temporal logic. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds) Temporal Logic in Specification. Lecture Notes in Computer Science, vol 398. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51803-7_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-51803-7_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51803-7

  • Online ISBN: 978-3-540-46811-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation