Propositional dynamic logic of nonregular programs (Q792083)

It was shown by \textit{M. J. Fischer} and \textit{R. E. Ladner} [J. Comput. Syst. Sci. 18, 194-211 (1979; Zbl 0408.03014)] that the validity problem for regular propositional dynamic logic (PDL) is decidable in deterministic exponential time, and, within a polynomial, this upper bound is the best possible. The authors consider similar problems for context-free PDL, showing that the borderline between decidable and undecidable PDL is extremely close to the original regular PDL, and strikingly that the transition leaps from decidability in exponential time for regular PDL to \(\Pi^ 1_ 1\)-completeness. A comprehensive characterization of the class of programs for which PDL is decidable remains an intriguing topic for future research.