Semantics of looping programs in Propositional Dynamic Logic

Standard and nonstandard models of Propositional Dynamic Logic differ in their interpretation of loops. In Standard models, a loop is interpreted as the Kleene closure of the interpretation of its loop body; in nonstandard (Loop Invariant) models, a loop is interpreted as a program which preserves invariant assertions over the loop body.In this paper we show that both interpretations are adequate to represent loops in PDL. We demonstrate this in two ways: First we note that Standard and Loop Invariant models are distinct but not distinguishable within PDL. Second, we show that the class of Loop Invariant models is complete with respect to the Segerberg axiomatization of PDL. Since completeness of the class of Loop Invariant models implies completeness of the class of Standard models, Standard models are also complete with respect to this axiomatization.The research reported here was supported in part by NSF Grants MCS77-02474 and MCS80-05387. Most of the results in this paper were announced in A Completeness Technique forD-axiomatizable Semantics presented at the 11th Annual ACM Symposium on the Theory of Computing in May, 1979.