Dynamic process logic (Q1092892)

\textit{M. K. Valiev} [Lect. Notes Comput. Sci. 148, 304-313 (1983; Zbl 0528.03014)] has shown that each formula of Pratt's dynamic process logic (DPL) is transformable into a formula of Pratt's propositional dynamic logic (PDL) in exponential time. The author shows that for any DPL formula, we can construct in quadratic time and linear space a PDL formula which is satisfiable if and only if the original DPL formula is satisfiable, which implies that DPL is decidable with exponential upper bound on its complexity.