Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra A of truth-degrees. More precisely, we work with coalgebraic modal logic via A-valued predicate liftings where A is an FLew-algebra, and interpret actions (abstracting programs and games) as F-coalgebras where the functor F represents some type of A-weighted system. We also allow combinations of crisp propositions with A-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for 2-valued iteration-free PDL with A-valued accessibility relations when A is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Łukasiewicz logic.