2026-07-22T04:42:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23572 2025-10-27T10:40:13Z ddc:004 open_access

Expressivity of Bisimulation Pseudometrics over Analytic State Spaces Luckhardt, Daniel Beohar, Harsh Kupke, Clemens Markov decision process quantitative Hennessy-Milner theorem 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Daniel Luckhardt and Harsh Beohar and Clemens Kupke 2025 Is Part Of LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CALCO.2025.13 urn:nbn:de:0030-drops-235727 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.13 eng https://creativecommons.org/licenses/by/4.0/legalcode