Paper detail

Towards a Coalgebraic Interpretation of Propositional Dynamic Logic

The interpretation of propositional dynamic logic (PDL) through Kripke models requires the relations constituting the interpreting Kripke model to closely observe the syntax of the modal operators. This poses a significant challenge for an interpretation of PDL through stochastic Kripke models, because the programs' operations do not always have a natural counterpart in the set of stochastic relations. We use rewrite rules for building up an interpretation of PDL. It is shown that each program corresponds to an essentially unique irreducible tree, which in turn is assigned a predicate lifting, serving as the program's interpretation. The paper establishes and studies this interpretation. It discusses the expressivity of probabilistic models for PDL and relates properties like logical and behavioral equivalence or bisimilarity to the corresponding properties of a Kripke model for a closely related non-dynamic logic of the Hennessy-Milner type.