Propositional Dynamic Logic for Recursive Procedures
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.
KeywordsPropositional dynamic logic recursive procedures fixpoints μ-Calculus
Unable to display preview. Download preview PDF.
- 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
- 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
- 10.Leivant, D.: Propositional dynamic logic with program quantifiers. Electronic notes in Theoretical Computer Science (to appear, 2008)Google Scholar
- 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