A Note on the Semantics of Looping Programs in Propositional Dynamic Logic
Francine Berman · Purdue e-Pubs (Purdue University System) · 1980
We discuss the representation of Propositional Dynamic Logic (POL). looping programs in We show that PDL is not expressive enough to distinguish between models in which loops are interpreted as the set of all finite sequences of iterations and models in which loops are interpreted as a set of computations which preserve loop invariants. We note that for distinguishable models of finite domain, both interpretations of loops coincide.