Expressivity of bisimulation pseudometrics over analytic state spaces

TL;DR

This paper introduces a new framework for analyzing Markov decision processes as coalgebras in analytic spaces, defining bisimulation pseudometrics and a quantitative modal logic that characterizes behavioral similarity.

Contribution

It develops a novel approach to bisimulation pseudometrics and modal logic for MDPs in analytic spaces, extending existing theories to a more general setting.

Findings

Defined bisimulation pseudometrics using fibrations

Developed a quantitative modal logic for coalgebras

Proved a quantitative Hennessy-Milner theorem

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.