Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Harel, D.: First-Order Dynamic Logic. LNCS, vol. 68. Springer, Berlin (1979)
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)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logics of nonregular programs. J. Comput. Sys. Sci. 25, 222–243 (1983)
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)
Harel, D., Singerman, E.: More on nonregular PDL: finite models and fibonacci-like programs. Inf. Comput. 128(2), 109–118 (1996)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)
Lange, M., Somla, R.: Propositional dynamic logic of context-free programs and fixpoint logic with chop. Inf. Process. Lett. 100(2), 72–75 (2006)
Leivant, D.: Propositional dynamic logic with program quantifiers. Electronic notes in Theoretical Computer Science (to appear, 2008)
Löding, C., Lutz, C., Serre, O.: Propositional dynamic logic with recursive programs. Journal of Logic and Algebraic Programming 73, 51–69 (2007)
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)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leivant, D. (2008). Propositional Dynamic Logic for Recursive Procedures. In: Shankar, N., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2008. Lecture Notes in Computer Science, vol 5295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87873-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-87873-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87872-8
Online ISBN: 978-3-540-87873-5
eBook Packages: Computer ScienceComputer Science (R0)