A streamlined temporal completeness theorem

  • Ana Pasztor
  • Ildiko Sain
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)


Temporal Logic Proof System Time Structure Predicate Symbol Concurrent Program 
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. [1]
    M.Abadi, ”The power of temporal proofs”, preprint of Digital Systems Research Center (1988).Google Scholar
  2. [2]
    M.Abadi, ”Temporal logic was incomplete only temporarily”, Preprint (1989).Google Scholar
  3. [3]
    M.Abadi and Z.Manna, ”A timely resolution”, First Annual Symposium in Computer Science, (1986), 176–186.Google Scholar
  4. [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. [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. [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. [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. [8]
    D.Gabbay and F.Guenther (eds), ”Handbook of philosophical logic”, D.Reidel Publ. Co. vol II (1984).Google Scholar
  9. [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. [10]
    T.Gergely and L.Ury, ”First-order programming theories”, SZAMALK Technical Report Budapest (1989), 232pp.Google Scholar
  11. [11]
    R.Goldblatt, ”Logics of time and computation”, Center for the Study of Language and Information, Lecture Notes Number 7 (1987).Google Scholar
  12. [12]
    L.Henkin, J.D.Monk, A.Tarski, ”Cylindric Algebras Part II”, North Holland (1985).Google Scholar
  13. [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. [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. [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. [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.CrossRefGoogle Scholar
  17. [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. [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.CrossRefGoogle Scholar
  19. [19]
    R.Parikh, ”A decidability result for second order process logic”, IEEE Symposium on Foundation of Comp. Sci. (1978), 177–183.Google Scholar
  20. [20]
    A. Pasztor, ”Nonstandard Algorithmic and Dynamic Logic”, in: J. Symbolic Computation 2 (1986), pp. 59–81.Google Scholar
  21. [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. [22]
    A. Pnueli, ”The temporal semantics of concurrent programs”, Theoretical Computer Science 13, (1981), 45–60.CrossRefGoogle Scholar
  23. [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. [24]
    I. Sain, ”Structured nonstandard dynamic logic”, Zeitschrift fur Math. Logic und Grundlagen der Math. Heft 3, 1984, pp. 481–497.Google Scholar
  25. [25]
    I. Sain, ”A simple proof for completeness of Floyd method”, Theoretical Computer Science vol 35 (1985), 345–348.Google Scholar
  26. [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. [27]
    I. Sain, ”Dynamic logic with nonstandard model theory”, Dissertation, Hungarian Academy of Sciences, Budapest, 1986 (in Hungarian).Google Scholar
  28. [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. [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. [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. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Ana Pasztor
    • 1
  • Ildiko Sain
    • 2
  1. 1.School of Computer ScienceFlorida International UniversityMiami
  2. 2.Mathematical Institute of the Hungarian Academy of SciencesBudapestHungary

Personalised recommendations