×

Behavioural pseudometrics for nondeterministic probabilistic systems. (English) Zbl 07897383

Summary: 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 M. Hennessy and R. Milner [J. Assoc. Comput. Mach. 32, 137–161 (1985; Zbl 0629.68021)]. The logic for characterising the state-based metric is much simpler than an earlier logic proposed by J. Desharnais et al. [Theor. Comput. Sci. 318, No. 3, 323–354 (2004; Zbl 1068.68093)] 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.

MSC:

68Qxx Theory of computing
Full Text: DOI