Determinism and non-determinism in PDL (Q1177157)

In a previous paper of the author it is proven that if we add the iteration to SPDL (strict propositional dynamic logic) then the new system has the same expressive power as PDL (propositional dynamic logic). Under review the case of nondeterminism is studied. The main theorem of the paper claims that if we add the nondeterministic choice to SPDL then the new system has less expressive power than PDL. In the last section of the paper the author defines a new system PPL (propositional program logic) by adding to SPDL the nondeterministic choice and propositional variables and it is proven that the system PPL and PDL have the same expressive power.