Logic of Programs 1983: Logics of Programs pp 501-512 | Cite as

Yet another process logic

Preliminary version
  • Moshe Y. Vardi
  • Pierre Wolper
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 164)


We present a process logic that differs from the one introduced by Harel, Kozen and Parikh in several ways. First, we use the extended temporal logic of Wolper for statements about paths. Second, we allow a “repeat” operator in the programs. This allows us to specify programs with infinite computations. However, we limit the interaction between programs and path statements by adopting semantics similar to the ones used by Nishimura. Also, we require atomic programs to be interpreted as binary relations. We argue that this gives us a more appropriate logic. We have obtained an elementary decision procedure for our logic. The time complexity of the decision procedure is four exponentials in the general case and two exponentials if the logic is restricted to finite paths.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

6. References

  1. [Bu62]
    J. R. Buchi, “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
  2. [Ch74]
    Y. Choueka, “Theories of Automata on θ-Tapes: A Simplified Approach”, Journal of Computer and System Sciences, 8 (1974), pp. 117–141.Google Scholar
  3. [EH82]
    E. A. Emerson, J. Y. Halpern, “Sometimes and Not Never Revisited: On Branching Versus Linear Time”, Proceedings of the 10th Symposium on Principles of Programming Languages, Austin, January 1983.Google Scholar
  4. [FL79]
    M. Fisher, R. Ladner, “Propositional Dynamic Logic of Regular Programs”, Journal of Computer and System Sciences, 18(2), 1979, pp. 194–211.Google Scholar
  5. [GPSS80]
    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
  6. [Ha79]
    D. Harel, “Two Results on Process Logic”, Information Processing Letters, 8 (1979), pp. 195–198.Google Scholar
  7. [HKP80]
    D. Harel, D. Kozen, R. Parikh, “Process Logic: Expressiveness, Decidability, Completeness”, Proceedings of the 21st Symposium on Foundations of Computer Science, Syracuse, October 1980, pp. 129–142.Google Scholar
  8. [HP82]
    D. Harel, D. Peleg, “Process logic with Regular Formulas”, Technical Report, Bar-Ilan University, Ramat-Gan, Israel, 1982.Google Scholar
  9. [Ni80]
    H. Nishimura, “Descriptively Complete Process Logic”, Acta Informatica, 14 (1980), pp. 359–369.Google Scholar
  10. [Pa78]
    R. Parikh, “A Decidability Result for a Second Order Process Logic”, Proceedings 19th IEEE Symposium on Foundations of Computer Science, Ann Arbor, October 1978.Google Scholar
  11. [Pn77]
    A. Pnueli, “The Temporal Logic of Programs”, Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, November 1977, pp. 46–57.Google Scholar
  12. [Pr76]
    V.R. Pratt, “Semantical Considerations on Floyd-Hoare Logic”, Proceedings 17th IEEE Symposium on Foundations of Computer Science, Houston, October 1976, pp. 109–121.Google Scholar
  13. [Pr78]
    V.R. Pratt, “A Practical Decision Method for Propositional Dynamic Logic”, Proceedings 10th ACM Symposium on Theory of Computing, San Diego, May 1979, pp. 326–337.Google Scholar
  14. [Pr81]
    V.R. Pratt, “Using Graphs to understand PDL”, Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, Springer-Verlag Lecture Notes in Computer Science, vol. 131, Berlin, 1982, pp. 387–396.Google Scholar
  15. [St81]
    R. Streett, “Propositional Dynamic Logic of Looping and Converse”, Proceedings of the 13th Symposium on Theory of Computing, Milwaukee, May 1981, pp. 375–383.Google Scholar
  16. [Wo81]
    P. Wolper, “Temporal Logic Can Be More Expressive”, Proceedings of the Twenty-Second Symposium on Foundations of Computer Science, Nashville, October 1981, pp. 340–348.Google Scholar
  17. [WVS83]
    P. Wolper, M. Y. Vardi, A. P. Sistla, “Reasoning about Infinite Computation Paths”, to appear in Proceedings 24th IEEE Symp. on Foundation of Computer Science, Tuscon, Nov. 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Moshe Y. Vardi
    • 1
  • Pierre Wolper
    • 2
    • 3
  1. 1.Stanford UniversityUSA
  2. 2.Bell LaboratoriesUSA
  3. 3.Bell LaboratoriesMurray Hill

Personalised recommendations