We present a coalgebraic framework for studying dynamic modal logics such as Propositional Dynamic Logic (PDL) and Parikh's Game Logic, which are logics for reasoning about program correctness and strategic ability in games, respectively. A characteristic feature of these logics is that their syntax is two-sorted, combining program/game constructs with modal logic syntax. Semantically, programs/games are modelled as T-coalgebras for a monad T on Set, and program/game constructs are interpreted as operations on T-coalgebras. The axiomatisation of PDL consists of extending normal modal logic K with reduction axioms that capture the interplay between program structure and propositions. Similarly, an axiomatisation based on monotonic modal logic M plus reduction axioms has been proposed for Game Logic. This modularity of axiomatisations was the starting point for developing dynamic logics in the setting of coalgebraic modal logic. The framework of coalgebraic dynamic logic is parametric in the coalgebra type functor T and a choice of modalities. In recent work, it has been extended from Boolean-valued to many-valued logics, with the underlying algebra A of truth values as an additional parameter. The main technical results include a compositionality theorem for behavioural equivalence and conditions for strong completeness (without iteration, many-valued) and weak completeness (with iteration, Boolean-valued).

This is joint work with Clemens Kupke, Raul Leal, and Wolfgang Poiger.