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

perfect, but impractical processes and other practical processes are considered safe
if they only differ from the specification with a negligible probability.
To find a more flexible way to differentiate processes, we borrow from pure
mathematics the notion of metric 2 and measure the difference between two processes
that are not quite bisimilar. Since different processes may behave the same, they
will be given distance zero in our metric semantics. So we are more interested in
pseudometrics than metrics.
In the rest of this section, we fix a finite-state pLTS ( S , L ,

−ₒ ) and provide the

set of pseudometrics on S with the following partial order.

Definition 3.10 The relation for the set M of 1-bounded pseudometrics on S is

defined by

m 1 m 2 if ∀ s , t : m 1 ( s , t ) ≥ m 2 ( s , t ) .

Here we reverse the ordering with the purpose of characterising bisimilarity by a
greatest fixed point (cf. Corollary 3.2 ).

Lemma 3.5 ( M , ) is a complete lattice.

Proof The top element is given by ∀ s , t : ( s , t ) = 0; the bottom element is given

by ↥ ( s , t ) = 1if s = t , 0 otherwise. Greatest lower bounds are given by

X ( s , t )

= { | ∈ }

sup m ( s , t ) m X

ↆ M

for any X . Finally, least upper bounds are given by

X

m ∈ X : m

= { m ∈ M |∀ m } .

In order to define the notion of state-metrics (that will correspond to bisimulations)
and the monotone transformation on metrics, we need to lift metrics from S to ( S ).

Here we use the lifting operation based on the Kantorovich metric [ 25 ] on probability
measures (cf. Sect. 3.4.1 ), which has been used by van Breugel and Worrell for
defining metrics on fully probabilistic systems [ 40 ] and reactive probabilistic systems
[ 55 ]; and by Desharnais et al. for labelled Markov chains [ 56 ] and labelled concurrent
Markov chains [ 57 ], respectively.

D

Definition 3.11 m ∈ M is a state-metric if, for all ʵ ∈ [0, 1), m ( s , t ) ≤ ʵ implies:

a
−ₒ

a
−ₒ

ʔ then there exists some ʔ such that t ʔ and m ( ʔ , ʔ )

ˆ ≤

• f s ʵ .

Note that if m is a state-metric then it is also a metric. By m ( s , t ) ≤ ʵ we have

m ( t , s ) ≤ ʵ , which implies

a
−ₒ

a
−ₒ ʔ then there exists some ʔ such that s m ( ʔ , ʔ )

• f t ʔ and ˆ ≤ ʵ .

2 For simplicity, in this section we use the term metric to denote both metric and pseudometric. All
the results are based on pseudometrics.