Expressivity of bisimulation pseudometrics over analytic state spaces

Tools

Luckhardt, Daniel and Beohar, Harsh and Kupke, Clemens; Cîrstea, Corina and Knapp, Alexander, eds. (2025) Expressivity of bisimulation pseudometrics over analytic state spaces. In: 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, GBR. ISBN 9783959773836 (https://doi.org/10.4230/LIPIcs.CALCO.2025.13)

[thumbnail of Luckhardt-etal-CALCO-2025-Expressivity-of-bisimulation-pseudometrics-over-analytic-state-spaces]
Preview
 Text. Filename: Luckhardt-etal-CALCO-2025-Expressivity-of-bisimulation-pseudometrics-over-analytic-state-spaces.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (818kB)| Preview

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.

ORCID iDs

Luckhardt, Daniel, Beohar, Harsh and Kupke, Clemens ORCID logoORCID: https://orcid.org/0000-0002-0502-391X; Cîrstea, Corina and Knapp, Alexander
CORE (COnnecting REpositories)