In Transition From Global to Modular Temporal Reasoning about Programs

  • Amir Pnueli
Part of the NATO ASI Series book series (volume 13)


The role of Temporal Logic as a feasible approach to the specification and verification of concurrent systems is now widely accepted. A companion paper in this volume ([HP]) defines more precisely the area of applicability of Temporal Logic as that of reactive systems.


Temporal Logic Mutual Exclusion Safety Property Concurrent Program Atomic Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BK]
    Barringer, H., Kuiper, R. — A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester (November 1983).Google Scholar
  2. [BKP1]
    Barringer, H., Kuiper, R., Pnueli, A. — Now You May Compose Temporal Logic Specifications, Proc. of the 16th ACM Symposium on Theory of Computing (1984) 51–63.Google Scholar
  3. [BKP2]
    Barringer, H., Kuiper, R., Pnueli, A. — A Compositional Temporal Approach to a CSP-like Language, Proc. of IFIP Conference, The Role of Abstract Models in Information Processing.Google Scholar
  4. [FP]
    Frances, N., Pnueli, A. — A Proof Method for Cyclic Programs, Acta Informatica 9 (1978) 133–157.CrossRefGoogle Scholar
  5. [GPSS]
    Gabbay, D., Pnueli, A., Shelah, S., Stavi, J. — On the Temporal Analysis of Fairness, Proc. of the 7th ACM Symposium on Principles of Programming Languages (1980) 163–173.Google Scholar
  6. [G]
    Gerth, R. — Transition Logic, Proc. of the 16th ACM Symposium on Theory of Computing (1984) 39–50.Google Scholar
  7. [HO]
    Hailpern, B., Owicki, S. — Modular Verification of Computer Communication Protocols, IEEE Trans. on Communications, COM-31, 1 (Jan. 1983) 56–68.CrossRefGoogle Scholar
  8. [HP]
    Harel, D., Pnueli, A. — On the Development of Reactive Systems, Thisissue.Google Scholar
  9. [KVR]
    Koymans, R., Vytopil, J., De Roever, W.P. — Real Time Programming and Asynchronous Message Passing, 2nd ACM Symposium on Principles of Distributed Computing, Montreal (1983) 187–197.Google Scholar
  10. [L1]
    Lamport, L. — What Good is Temporal Logic?, Proceedings IFIP (1983) 657–668.Google Scholar
  11. [L2]
    Lamport, L. — Specifying Concurrent Program Modules, ACM TOPLAS, 5, 2 (1983) 190–222.CrossRefMATHGoogle Scholar
  12. [LS]
    Lamport, L., Schneider, P. — The “Hoare Logic” of CSP and All That,ACM TOPLAS, 6, 2 (April 1984) 281–296.CrossRefMATHGoogle Scholar
  13. [MC]
    Misra, J., Chandy, K.M. — Proofs of Networks of Processes, IEEE Transactions on Software Engin. SE-7, 4 (July 1981).Google Scholar
  14. [MP1]
    Manna, Z., Pnueli, A.–Verification of Concurrent Programs: The Temporal Framework, in Correctness Problem in Computer Science, R.S. Boyer, J.S. Moare (eds.) Academic Press (1982) 215–273.Google Scholar
  15. [MP2]
    Manna, Z., Pnueli, A. — Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs, Science of Computer Programming, 4,3 (1984) 257–290.Google Scholar
  16. [MP3]
    Manna, Z., Pnueli, A. — Verification of Concurrent Programs. A Temporal Proof System, Proc. 4th School on Advanced Programming, Amsterdam (June 1982) 163–255.Google Scholar
  17. [MP4]
    Manna, Z., Pnueli, A. — How to Cook a Temporal Proof System for Your Pet Language, Proceeding of the Symposium of Principles of Programming Languages (1983).Google Scholar
  18. [N]
    Naur, P. (Ed.) — Revised Report on the Algorithmic Language Algol 60, CACM, 6, 1 (1963) 1–17.Google Scholar
  19. [OG]
    Owicki, S., Gries, D. — An Axiomatic Proof Technique for Parallel Programs, Acta Informatica 6 (1976) 319–340.CrossRefMATHMathSciNetGoogle Scholar
  20. [OL]
    Owicki, S., Lamport, L. — Proving Liveness Properties of Concurrent Programs, ACM TOPLAS 4, 3 (July 1982) 455–495.CrossRefMATHGoogle Scholar
  21. [Pe]
    Peterson, G.L. — Myths about the Mutual Exclusion Problem, Information Processing Letters 12, 3 (1981) 115–116.CrossRefMATHGoogle Scholar
  22. [RZ]
    De Roever, W.P., Zwiers, J. — manuscript.Google Scholar

Copyright information

© Springer-Verlag Heidelberg 1985

Authors and Affiliations

  • Amir Pnueli
    • 1
  1. 1.Department of Applied MathematicsThe Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations