Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 23

setting state s is related to state t by a relation R , say probabilistic simulation, written

a
−ₒ

a
−ₒ

s R t , if for each transition s ʔ from s there exists a transition t ʘ from t

such that ʘ can somehow mimic the behaviour of ʔ according to R . To formalise

† between distributions

the mimicking of ʔ by ʘ ,wehaveto lift R to be a relation R

† ʘ .
Various approaches of lifting relations have appeared in the literature; see e.g. [ 6 ,
19 , 22 - 24 ]. We will show that although those approaches appear different, they can be
reconciled. Essentially, there is only one lifting operation, which has been presented
in different forms. Moreover, we argue that the lifting operation is interesting in
itself. This is justified by its intrinsic connection with some fundamental concepts in
mathematics, notably the Kantorovich metric [ 25 ]. For example, it turns out that our
lifting of binary relations from states to distributions nicely corresponds to the lifting
of metrics from states to distributions by using the Kantorovich metric. In addition,
the lifting operation is closely related to the maximum flow problem in optimisation
theory, as observed by Baier et al. [ 26 ].
A good scientific concept is often elegant, even seen from many different per-
spectives. Among the wealth of behavioural equivalences proposed in the traditional
concurrency theory during the last three decades, bisimilarity [ 27 , 28 ] is probably the
most studied one as it admits a suitable semantics, a nice coinductive proof technique
and efficient decision algorithms. In our opinion, bisimulation is a good concept be-
cause it can be characterised in a great many ways such as fixed-point theory, modal
logics, game theory, coalgebras etc., and all the characterisations are very natural. We
believe that probabilistic bisimulation is such a concept in probabilistic concurrency
theory. As evidence, we will provide in this chapter three characterisations, from the
perspectives of modal logics, metrics and decision algorithms.

over states so that we can require ʔ R

1. Our logical characterisation of probabilistic bisimulation consists of two aspects:
adequacy and expressivity [ 29 ]. A logic

is adequate when two states are bisimilar
if and only if they satisfy exactly the same set of formulae in

L

L . The logic is

expressive when each state s has a characteristic formula ˕ s in such that t

is bisimilar to s if and only if t satisfies ˕ s . We will introduce a probabilistic-
choice modality to capture the behaviour of distributions. Intuitively, distribution

L

ʔ satisfies the formula i ∈ I p i ·

˕ i if there is a decomposition of ʔ into a convex
combination of some distributions, ʔ

= i ∈ I p i ·

ʔ i , and each ʔ i conforms to
the property specified by ˕ i . When the new modality is added to the Hennessy-
Milner logic [ 30 ] we obtain an adequate logic for probabilistic bisimilarity; when
it is added to the modal mu-calculus [ 31 ] we obtain an expressive logic.
2. By metric characterisation of probabilistic bisimulation, we mean to give a pseu-
dometric 1 such that two states are bisimilar if and only if their distance is 0 when
measured by the pseudometric. More specifically, we show that bisimulations
correspond to pseudometrics that are postfixed points of a monotone function,

1 We use a pseudometric rather than a proper metric because two distinct states can still be at
distance zero if they are bisimilar.