Yuxin Deng (ECNU)

Title: Modal Characterisations of Behavioural Pseudometrics 

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.