Propositional Dynamic Logic with Program Quantifiers

We consider an extension QPDL of Segerberg-Pratt's Propositional Dynamic Logic PDL, with program quantification, and study its expressive power and complexity. A mild form of program quantification is obtained in the calculus μPDL, extending PDL with recursive procedures (i.e. context free programs), which is known to be -complete. The unrestricted program quantification we consider leads to complexity equivalent to that of second-order logic (and second-order arithmetic), i.e. outside the analytical hierarchy. However, the deterministic variant of QPDL has complexity .