Propositional Dynamic Logic for Recursive Procedures

  • Daniel Leivant
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


We present a simple and natural deductive formalism μPDL for propositional dynamic logic for recursive procedures, including simultaneous recursion. Though PDL with recursive programs is known to be highly undecidable, natural deductive formalisms for it are of substantial interest, because they distill the essential logical components of recursive procedures. We also show that Pratt-Kozen’s μ-Calculus, in which fixpoints are taken over formulas rather than programs, is interpretable in μ PDL.


Propositional dynamic logic recursive procedures fixpoints μ-Calculus 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and nonrecursive programs. Technical Report TR-75, Deptment of Computer Science, University of Toronto (1975)Google Scholar
  2. 2.
    Harel, D.: First-Order Dynamic Logic. LNCS, vol. 68. Springer, Berlin (1979)zbMATHGoogle Scholar
  3. 3.
    Harel, D.: Recursion in logics of programs. In: POPL 1979: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 81–92. ACM, New York (1979)CrossRefGoogle Scholar
  4. 4.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  5. 5.
    Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logics of nonregular programs. J. Comput. Sys. Sci. 25, 222–243 (1983)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Harel, D., Puneli, A., Stavi, J.: A complete axiomatic system for proving deductions about recursive programs. In: Proceedings of the ninth annual ACM symposium on Theory of computing, pp. 249–260 (1977)Google Scholar
  7. 7.
    Harel, D., Singerman, E.: More on nonregular PDL: finite models and fibonacci-like programs. Inf. Comput. 128(2), 109–118 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Lange, M., Somla, R.: Propositional dynamic logic of context-free programs and fixpoint logic with chop. Inf. Process. Lett. 100(2), 72–75 (2006)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Leivant, D.: Propositional dynamic logic with program quantifiers. Electronic notes in Theoretical Computer Science (to appear, 2008)Google Scholar
  11. 11.
    Löding, C., Lutz, C., Serre, O.: Propositional dynamic logic with recursive programs. Journal of Logic and Algebraic Programming 73, 51–69 (2007)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471. pp. 103–119. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. 13.
    Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Pratt, V.: A decidable mu-calculus (preliminary report). In: Proceedings of the twenty-second IEEE Symposium on Foundations of Computer Science, pp. 421–427. Computer Society press, Los Angles (1981)Google Scholar
  15. 15.
    von Oheimb, D.: Hoare logic for mutual recursion and local variables. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738. pp. 168–180. Springer, Heidelberg (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Daniel Leivant
    • 1
  1. 1.Computer Science DepartmentIndiana UniversityBloomingtonUSA

Personalised recommendations