Towards quantitative verification of probabilistic transition systems

It has been argued that Boolean-valued logics and associated 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 reactive probabilistic transition systems yielding a quantitative notion of behavioural equivalence. The pseudometric is defined via the terminal coalgebra of a functor based on the Hutchinson metric on the space of Borel probability measures on a metric space. We also characterize the distance between systems in terms of a real-valued modal logic.