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

The above property will be used in Sect. 3.7 to give a metric characterisation of
probabilistic bisimulation (cf. Theorem 3.11 ).
In the remainder of this subsection we do a sanity check and show that ( 3.7 ) and
( 3.8 ) do entail the same metric on ( S ). Given a metric m on S , we write m for the

lifted metric by using the linear programming problem in ( 3.8 ).

D

Proposition 3.5 Let m be a metric over S. Then m is a metric over ˆ D ( S ) .

Proof We verify that ( D ( S ), m ) satisfies the definition of pseudometric space. ˆ

1. It is clear that m ( ʔ , ʔ ) ˆ = 0.

2. We observe that
s ∈ S ( ʔ ( s ) s ∈ S ( ʔ ( s ) s ∈ S ʔ ( s ) s ∈ S ʔ ( s )

ʔ ( s )) x s = − − ʔ ( s ))(1 − x s ) + −

s ∈ S ( ʔ ( s )

= − ʔ ( s ))(1 − x s ) .

Now x s =

−

1 x s also satisfy the constraints on x s in ( 3.7 ), hence the symmetry

ˆ

m can be shown.
3. Let ʔ 1 , ʔ 2 , ʔ 3 ∈ D

of

( S ), we have

( ʔ 1 ( s ) − ʔ 3 ( s )) x s = ( ʔ 1 ( s ) − ʔ 2 ( s )) x s + ( ʔ 2 ( s ) − ʔ 3 ( s )) x s .

s ∈ S s ∈ S s ∈ S

By taking the maximum over the x s for the left hand side, we obtain

m ( ʔ 1 , ʔ 3 ) ≤ m ( ʔ 1 , ʔ 2 ) + m ( ʔ 2 , ʔ 3 ) .

Let m be a metric over S. Then m Proposition 3.6 is a metric over D ( S ) .

( S ), m ) satisfies the definition of pseudometric space.
1. It is easy to see that m ( ʔ , ʔ )

Proof We verify that ( D

= 0, by letting y s , s = ʔ ( s ) and y s , t = 0 for all

t in ( 3.8 ).
2. Suppose m ( ʔ , ʔ ) is obtained by using some real numbers y s , t in ( 3.8 ). Let
y s , t =

s =

y t , s for all s , t ∈ S . We have that

y t , s = y t , s .

m ( s , t ) · y s , t = m ( s , t ) · m ( t , s ) ·

s , t ∈ S s , t ∈ S t , s ∈ S

Observe that s ∈ S y t , s = s ∈ S y s , t =

ʔ ( t ) for all t

S , and similarly we have
the dual t ∈ S y t , s = ʔ ( s ) for all s ∈ S . It follows that m ( ʔ , ʔ )

∈

= m ( ʔ , ʔ ).
3. Suppose m ( ʔ 1 , ʔ 2 ) is obtained by using some real numbers x s , t in ( 3.8 ), and

m ( ʔ 2 , ʔ 3 ) is obtained by using y s , t . Let z s , t = r ∈ ʔ 2 x s , r ·

y r , t
ʔ 2 ( r ) . Note that

if ʔ 2 ( r ) = 0 for some r ∈ S , then we must have that x s , r = y r , t = 0 for any