Skip to main content
SpringerLink
Log in

Completing the temporal picture

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1989)

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

Included in the following conference series:

Abstract

The paper presents a relatively complete proof system for proving the validity of temporal properties of reactive programs. The presented proof system improves on previous temporal systems, such as [MP83a] and [MP83b], in that it reduces the validity of program properties into pure assertional reasoning, not involving additional temporal reasoning. The proof system is based on the classification of temporal properties according to the Borel hierarchy, providing an appropriate proof rule for each of the main classes, such as safety, response, and progress properties.

This research was supported in part by the National Science Foundation under grants DCR-8413230 and CCR-8812595, by the Defense Advanced Research Projects Agency under contract N00039-84-C-0211, and by the United States Air Force Office of Scientific Research under contracts AFOSR 87-0149 and 88-0281.

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. K.R. Apt, Ten years of Hoare's logic: A survey — part I, ACM Trans. Prog. Lang. Sys. 3, 1981, pp. 431–483.

    Article  Google Scholar 

  2. B. Alpern and F.B. Schneider, Verifying temporal properties without temporal logic, ACM Trans. Prog. Lang. Sys. 11, 1989, pp. 147–167.

    Article  Google Scholar 

  3. S.A. Cook, Soundness and completeness of an axiom system for program verification, SIAM J. Comp. 7, 1978, pp. 70–90.

    Google Scholar 

  4. N. Francez, Fairness, Springer, 1986.

    Google Scholar 

  5. O. Grumberg, N. Francez, J.A. Makowski, and W.P. de Roever, A proof rule for fair termination, Inf. and Comp. 66, 1985, pp. 83–101.

    Google Scholar 

  6. D. Harel, First-Order Dynamic Logic, Lec. Notes in Comp. Sci. 68, Springer, 1979.

    Google Scholar 

  7. F. Kröger, Temporal Logic of Programs, Volume 8 of EATCS Monographs on Theoretical Computer Science, Springer, 1987.

    Google Scholar 

  8. D. Lehmann, A. Pnueli, and J. Stavi, Impartiality, justice and fairness: The ethics of concurrent termination, Proc. 8th Int. Colloq. Aut. Lang. Prog., Lec. Notes in Comp. Sci. 115, Springer, 1981, pp. 264–277.

    Google Scholar 

  9. O. Lichtenstein, A. Pnueli, and L. Zuck, The glory of the past, Proc. Conf. Logics of Programs, Lec. Notes in Comp. Sci. 193, Springer, 1985, pp. 196–218.

    Google Scholar 

  10. Z. Manna and A. Pnueli, How to cook a temporal proof system for your pet language, Proc. 10th ACM Symp. Princ. of Prog. Lang., 1983, pp. 141–154.

    Google Scholar 

  11. Z. Manna and A. Pnueli, Verification of concurrent programs: A temporal proof system, Foundations of Computer Science IV, Distributed Systems: Part 2 (J.W. DeBakker and J. Van Leuwen, eds.), Mathematical Centre Tracts 159, Center for Mathematics and Computer Science (CWI), Amsterdam, 1983, pp. 163–255.

    Google Scholar 

  12. Z. Manna and A. Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Sci. Comp. Prog. 32, 1984, pp. 257–289.

    Article  Google Scholar 

  13. Z. Manna and A. Pnueli, Specification and verification of concurrent programs by ∀-automata, Proc. 14th ACM Symp. Princ. of Prog. Lang., 1987, pp. 1–12.

    Google Scholar 

  14. Z. Manna and A. Pnueli, The anchored version of the tempoal framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency (J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, eds.), Lec. Notes in Comp. Sci. 354, Springer-Verlag, 1989, pp. 201–284.

    Google Scholar 

  15. Z. Manna and A. Pnueli, Proof Principles for Classes of Properties, Technical Report, Dept. of Comp. Sci., Weizmann Institute, 1989.

    Google Scholar 

  16. S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM Trans. Prog. Lang. Sys. 4, 1982, pp. 455–495.

    Article  Google Scholar 

  17. A. Pnueli, Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends, Current Trends in Concurrency (J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, eds.), Lec. Notes in Comp. Sci. 224, Springer, 1986, pp. 510–584.

    Google Scholar 

  18. W. Thomas, A combinatorial approach to the theory of ω-automata, Inf. and Cont. 48, 1981, pp. 261–283.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, 94305, Stanford, CA

    Zohar Manna

  2. Department of Applied Mathematics, Weizmann Institute, Rehovot, Israel

    Zohar Manna & Amir Pnueli

Authors
  1. Zohar Manna
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Giorgio Ausiello Mariangiola Dezani-Ciancaglini Simonetta Ronchi Della Rocca

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Manna, Z., Pnueli, A. (1989). Completing the temporal picture. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds) Automata, Languages and Programming. ICALP 1989. Lecture Notes in Computer Science, vol 372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035782

Download citation

  • DOI: https://doi.org/10.1007/BFb0035782

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51371-1

  • Online ISBN: 978-3-540-46201-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation