The propositional dynamic logic of deterministic, well-structured programs (Q801682)

PDL is the propositional dynamic logic of regular programs. DPDL is the propositional dynamic logic of regular programs built from deterministic atomic programs. SDPDL is the propositional dynamic logic of deterministic well-structured programs, i.e., programs that are built from deterministic atomic programs by means of the while and if constructs. The main results of the paper are that SDPDL is strictly less expressive than DPDL, and that the validity problem for SDPDL is logspace complete for PSPACE (the validity problems for PDL and DPDL are logspace complete for EXPTIME). The results carry a special significance, since they indicate that the exponential lower bound by Fischer and Ladner for PDL may not be all that realistic.