Behavioural Pseudometrics for Nondeterministic Probabilistic Systems
Wenjie Du, Yuxin Deng, and Daniel Gebler
For the model of probabilistic labelled transition systems that allow for
the co-existence of nondeterminism and probabilities, we present two notions
of bisimulation metrics: one is state-based and the other is distribution-based.
We provide a sound and complete modal characterisation for each of them,
using real-valued modal logics based on Hennessy-Milner logic. The logic for
characterising the state-based metric is much simpler than an earlier logic
by Desharnais et al. as it uses only two non-expansive operators rather than
the general class of non-expansive operators. For the kernels of the two metrics,
which correspond to two notions of bisimilarity, we give a comprehensive comparison
with some typical distribution-based bisimilarities in the literature.