A behavioural pseudometric for probabilistic transition systems

Discrete notions of behavioural equivalence sit uneasily with semantic models featuring quantitative data, like probabilistic transition systems. In this paper, we present a pseudometric on a class of probabilistic transition systems yielding a quantitative notion of behavioural equivalence. The pseudometric is defined via the terminal coalgebra of a functor based on a metric on the space of Borel probability measures on a metric space. States of a probabilistic transition system have distance 0 if and only if they are probabilistic bisimilar. We also characterize our distance function in terms of a real-valued modal logic.