Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility

TL;DR

This paper develops a coalgebraic framework for many-valued dynamic modal logics, enabling analysis of systems with truth degrees, and proves strong completeness results for various many-valued logics.

Contribution

It introduces a coalgebraic approach for many-valued dynamic logics, including reducibility of operations and strong completeness proofs for several logic variants.

Findings

Proves reducibility of coalgebra operations preserves bisimulation.

Establishes strong completeness for finite-chain many-valued PDL.

Extends results to many-valued game logic with Lukasiewicz logic.

Abstract

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 $\mathbf{A}$ of truth-degrees. More precisely, we work with coalgebraic modal logic via $\mathbf{A}$-valued predicate liftings where $\mathbf{A}$ is a $\mathsf{FL}_{\mathrm{ew}}$-algebra, and interpret actions (abstracting programs and games) as $\mathsf{F}$-coalgebras where the functor $\mathsf{F}$ represents some type of $\mathbf{A}$-weighted system. We also allow combinations of crisp propositions with $\mathbf{A}$-weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations that 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 $\mathbf{A}$-valued accessibility relations when $\mathbf{A}$ is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Lukasiewicz logic.