Publications [#237078] of John H. Reif

Journal articles or Book chapters PUBLISHED

1. Halpern, JY; Reif, JH, The propositional dynamic logic of deterministic, well-structured programs, Theoretical Computer Science, vol. 27 no. 1-2 (January, 1983), pp. 127-165, Elsevier BV, ISSN 0304-3975 [doi]
   (last updated on 2026/01/15)

   Abstract:
   We consider a restricted propositional dynamic logic, Strict Deterministic Propositional Dynamic Logic (SDPDL), which is appropriate for reasoning about deterministic well-structured programs. In contrast to PDL, for which the validity problem is known to be complete in deterministic exponential time, the validity problem for SDPDL is shown to be polynomial space complete. We also show that SDPDL is less expressive than PDL, and give a complete axiomatization for it. The results rely on structure theorems for models of satisfiable SDPDL formulas, and the proofs give insight into the effects of nondeterminism on intractability and expressiveness in program logics. © 1983.