Is the Interesting Part of Process Logic uninteresting?: A Translation from PL to PDL
R. W. Sherman, Amir Pnueli, David Harel · SIAM Journal on Computing · 1984
With the (necessary) condition that atomic programs in process logic (PL) be binary, we present an algorithm for the translation of a PL formula p into a program $\zeta (p)$ of propositional dynamic logic (PDL) such that a finite path satisfies p if it belongs to $\zeta (p)$. This reduction has two immediate corollaries: 1) validity in this PL can be tested by testing validity of formulas in PDL; 2) all state properties expressible in this PL are expressible in PDL. The translation, however, is of nonelementary time complexity.The significance of the result to the search for natural and powerful logics of programs is discussed.