Towards a Coalgebraic Interpretation of Propositional Dynamic Logic

TL;DR

This paper develops a coalgebraic framework for interpreting propositional dynamic logic (PDL), especially in stochastic settings, by using rewrite rules and irreducible trees to assign meaning to programs.

Contribution

It introduces a novel coalgebraic interpretation of PDL via rewrite rules and irreducible trees, extending the semantics to stochastic Kripke models.

Findings

Establishes a correspondence between programs and irreducible trees.

Relates probabilistic models' expressivity to PDL properties.

Connects logical and behavioral equivalences in probabilistic and non-dynamic logics.

Abstract

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.