Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 1989: CSL '89 pp 322–336Cite as

A streamlined temporal completeness theorem

  • Conference paper
  • First Online:

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M.Abadi, ”The power of temporal proofs”, preprint of Digital Systems Research Center (1988).

    Google Scholar 

  2. M.Abadi, ”Temporal logic was incomplete only temporarily”, Preprint (1989).

    Google Scholar 

  3. M.Abadi and Z.Manna, ”A timely resolution”, First Annual Symposium in Computer Science, (1986), 176–186.

    Google Scholar 

  4. H. Andreka, ”Sharpening the characterization of the power of Floyd's method”, in: Logic of Programs and their Applications, ed.: A. Salwicki (Proc. Conf. Poznan 1980), Lecture Notes in Computer Science 148, Springer-Verlag 2983, pp. 1–26.

    Google Scholar 

  5. H. Andreka, I. Nemeti and I. Sain, “A complete logic for reasoning about programs via nonstandard model theory”, Parts I–II, Theoretical Computer Science 17 (1982), pp. 193–212 and pp. 259–278.

    Google Scholar 

  6. H.Andreka, I.Nemeti, I.Sain, ”On the strength of temporal proofs”, Proc. Conf. MFCS'89 (Mathem. Foundations of Comp. Sci.), in press (1989).

    Google Scholar 

  7. B.Biro and I.Sain, ”Peano Arithmetic for the time scale of nonstandard models for logics of programs”, Annals of Pure and Applied Logic, to appear.

    Google Scholar 

  8. D.Gabbay and F.Guenther (eds), ”Handbook of philosophical logic”, D.Reidel Publ. Co. vol II (1984).

    Google Scholar 

  9. D.Gabbay, A.Pnueli, S.Shelah, J.Stavi, ”On the temporal analysis of fairness”, Preprint Weizman Institute of Science, Dept. of Applied Math. (1981).

    Google Scholar 

  10. T.Gergely and L.Ury, ”First-order programming theories”, SZAMALK Technical Report Budapest (1989), 232pp.

    Google Scholar 

  11. R.Goldblatt, ”Logics of time and computation”, Center for the Study of Language and Information, Lecture Notes Number 7 (1987).

    Google Scholar 

  12. L.Henkin, J.D.Monk, A.Tarski, ”Cylindric Algebras Part II”, North Holland (1985).

    Google Scholar 

  13. J.A. Makowsky and I. Sain, ”Weak second order characterizations of various program verification systems”, Technical Report #457, Technion-Israel Institute of Technology, Comp. Sci. Dept., June 1987. Submitted to Theoretical Computer Science.

    Google Scholar 

  14. Z.Manna and A.Pnueli, ”How to cook a temporal proof system for your pet language”, Tenth ACM Symposium on Principles of Programming languages, (1983), 141–154.

    Google Scholar 

  15. Z.Manna and A.Pnueli, ”Verification of concurrent programs: A temporal proof system”, Report No. STAN-CS-83-967, Comp. Sci. Dept., Stanford University, (1983).

    Google Scholar 

  16. Z. Manna and A. Pnueli, ”Adequate proof principles for invariance and liveliness properties of concurrent programs”, Science of Computer Programming, vol. 4, No. 3, (1984), 257–289.

    Article  Google Scholar 

  17. I. Nemeti, ”Nonstandard dynamic logic”, in: Logics of Programs, ed.: D. Kozen, (Proc. Conf. New York 1981) Lecture Notes in Computer Science 131, Springer-Verlag, 1982, pp. 311–348.

    Google Scholar 

  18. S. Owicki and L. Lamport, ”Proving liveness properties of concurrent programs”, ACM Transactions on Programming Languages and Systems, vol. 4, No. 3, (1982), 455–495.

    Article  Google Scholar 

  19. R.Parikh, ”A decidability result for second order process logic”, IEEE Symposium on Foundation of Comp. Sci. (1978), 177–183.

    Google Scholar 

  20. A. Pasztor, ”Nonstandard Algorithmic and Dynamic Logic”, in: J. Symbolic Computation 2 (1986), pp. 59–81.

    Google Scholar 

  21. A.Pasztor, “Pnueli's temporal method is complete for nondeterministic programs”, Florida International University School of Computer Science Research Report 89-09, University Park, Miami, FL 33199, (1989).

    Google Scholar 

  22. A. Pnueli, ”The temporal semantics of concurrent programs”, Theoretical Computer Science 13, (1981), 45–60.

    Article  Google Scholar 

  23. M.M. Richter and M.E. Szabo, ”Nonstandard computation theory”, In: Algebra, combinatorics, and logic in computer science, Proc. Conf. Gyoer Hungary 1983 (eds: J.Demetrovics, G.Katona, A.Salomaa), Colloq. Math. Soc. J.Bolyai vol 42, North-Holland (1986), 667–693.

    Google Scholar 

  24. I. Sain, ”Structured nonstandard dynamic logic”, Zeitschrift fur Math. Logic und Grundlagen der Math. Heft 3, 1984, pp. 481–497.

    Google Scholar 

  25. I. Sain, ”A simple proof for completeness of Floyd method”, Theoretical Computer Science vol 35 (1985), 345–348.

    Google Scholar 

  26. I. Sain, ”The reasoning powers of Burstall's (modal logic) and Pnueli's (temporal logic) program verification methods”, in: Logics of Programs, ed.: R. Parikh (Proc. Conf. Brooklyn USA 1985) Lecture Notes in Computer Science 193, Springer-Verlag, pp. 302–319.

    Google Scholar 

  27. I. Sain, ”Dynamic logic with nonstandard model theory”, Dissertation, Hungarian Academy of Sciences, Budapest, 1986 (in Hungarian).

    Google Scholar 

  28. I. Sain, ”Is “SOME OTHER TIME” sometimes better than “SOMETIME” in proving partial correctness of programs?”, to appear in a special vol. of Studia Logica on nonstandard methods edited by M.M. Richter and M.E. Szabo.

    Google Scholar 

  29. I.Sain, ”Elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic”, Notre Dame Journal of Formal Logic, to appear (1989).

    Google Scholar 

  30. I. Sain, ”Relative program verifying powers of the various temporal logics”, Information and Control, to appear. An extended abstract of this is [26].

    Google Scholar 

  31. I.Sain, ”Comparing and characterizing the power of established program verification methods”, In: Many Sorted Logic and its applications (ed: J. Tucker), Proc. Conf. Leeds, Great Britain 1988, to appear.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Florida International University, University Park, 33199, Miami, FL

    Ana Pasztor

  2. Mathematical Institute of the Hungarian Academy of Sciences, P.O. Box 127, H-1364, Budapest, Hungary

    Ildiko Sain

Authors
  1. Ana Pasztor
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ildiko Sain
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Egon Börger Hans Kleine Büning Michael M. Richter

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pasztor, A., Sain, I. (1990). A streamlined temporal completeness theorem. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '89. CSL 1989. Lecture Notes in Computer Science, vol 440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52753-2_48

Download citation

  • DOI: https://doi.org/10.1007/3-540-52753-2_48

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52753-4

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation