Expressivity of bisimulation pseudometrics over analytic state spaces
Daniel Luckhardt, Harsh Beohar, Clemens Kupke
TL;DR
This work develops a measure-theoretic, coalgebraic framework for continuous-state Markov decision processes by situating MDPs as coalgebras in the category of analytic spaces ${\textnormal{Ana}}$. It constructs bisimulation pseudometrics via a coupling-based Wasserstein lifting within a fibrational Pred/lsPred setting and introduces a quantitative modal logic ${\mathcal L}$ whose semantics yield a logical distance that matches the bisimulation distance. By leveraging Kantorovich–Rubinstein duality and Stone–Weierstrass theory, the authors prove an expressivity theorem that guarantees the logic is expressive for the bisimulation metric, and they establish adequacy under suitable topologisability conditions. The framework yields a principled bridge between measurable-space semantics and modal verification, enabling precise quantitative reasoning about continuous-state MDPs with rewards. This has potential implications for verification, specification, and learning in probabilistic systems with infinite or continuous state spaces.
Abstract
A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of measurable spaces. Note that analytic spaces were already studied in the literature on labelled Markov processes and bisimulation relations. Our results are twofold. First, we define bisimulation pseudometrics over such coalgebras using the framework of fibrations. Second, we develop a quantitative modal logic for such coalgebras and prove a quantitative form of Hennessy-Milner theorem in this new setting stating that the bisimulation pseudometric corresponds to the logical distance induced by modal formulae.