Modal Characterisations of Behavioural Pseudometrics

TL;DR

This paper introduces two bisimulation pseudometrics for probabilistic labelled transition systems with nondeterminism, providing modal characterisations using simplified real-valued modal logics.

Contribution

It presents a simplified state-based modal logic for bisimulation metrics, improving upon previous more complex logics.

Findings

Sound and complete modal characterisations for both metrics

Simpler logic for state-based metric using only two non-expansive operators

Applicable to systems with nondeterminism and probabilities

Abstract

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 the 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.