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

and F 0 ( where is the top metric in M ) = .

Lemma 3.9 For image-finite pLTSs, the closure ordinal of F is ˉ.

a
−ₒ

F i (

Proof Let m max ( s , t ) ≤ ʵ and s ʔ . For each m i = ) there is a ʘ i such

a
−ₒ

that t ʵ . Since the pLTSs are image-finite, there is a ʘ

such that for all but finitely many i , t

ʘ i and m i ( ʔ , ʘ i ) ˆ ≤

a
−ₒ

We now show the correspondence between our state-metrics and bisimulations.

ʘ and m i ( ʔ , ʘ ) ˆ ≤ ʵ .

Theorem 3.11 Given a binary relation R and a pseudometric m ∈ M on a finite-

state pLTS such that

⊧
⊨

0 if s R t

m ( s , t ) = (3.23)

⊩

1 otherwise.

Then R is a probabilistic bisimulation if and only if m is a state-metric.

Proof The result can be proved by using Theorem 3.3 , which in turn relies on
Theorem 3.1 (1). Below we give an alternative proof that uses Theorem 3.1 (2) instead.
Given two distributions ʔ , ʔ over S , let us consider how to compute m ( ʔ , ʔ )if ˆ

R is an equivalence relation. Since S is finite, we may assume that V 1 , ... , V n ∈ S/ R

are all the equivalence classes of S under R .If s , t ∈ V i for some i ∈ 1, ... , n ,

then m ( s , t ) = 0, which implies x s = x t by the first constraint of ( 3.7 ). So for

each i V i . Thus,

some summands of ( 3.7 ) can be grouped together and we have the following linear
program:

∈ 1, ... , n there exists some x i such that x i = x s for all s ∈

ʔ ( V i )) x i

−

( ʔ ( V i ) (3.24)

i ∈ 1, ... , n

with the constraint x i − x j ≤ 1 for any i , j ∈ 1, ... , n with i = j . Briefly speaking,

m ( ʔ , ʔ ) is obtained by maximising the linear

if R is an equivalence relation then ˆ

program in ( 3.24 ).
( ⃒ ) Suppose R is a bisimulation and m ( s , t ) = 0. From the assumption in ( 3.23 )

we know that R is an equivalence relation. By the definition of m we have s R t .If

a
−ₒ

a
−ₒ

† ʔ . To show that m is a state-

ʔ for some ʔ such that ʔ

R

s ʔ then t

† ʔ and Theorem 3.1

m ( ʔ , ʔ )

ˆ = R

metric it suffices to prove 0. We know from ʔ

(2) that ʔ ( V i ) = ʔ ( V i ), for each i ∈ 1, ... , n . It follows that ( 3.24 ) is maximised

m ( ʔ , ʔ )

to be 0, thus = 0.

is an
equivalence relation. We show that it is a bisimulation. Suppose s R t , which means
m ( s , t )

( ⃐ ) Suppose m is a state-metric and has the relation in ( 3.23 ). Notice that R

a
−ₒ

a
−ₒ ʔ for some ʔ such that m ( ʔ , ʔ ) = 0. If s ʔ then t ˆ = 0. To

m ( ʔ , ʔ )

ensure that ˆ = 0, in ( 3.24 ) the following two conditions must be satisfied.

ʔ ( V i ) > 0 then ( 3.24 ) would 1. No coefficient is positive. Otherwise, if ʔ ( V i ) −

ʔ ( V i )), which is greater than 0.

be maximised to a value not less than ( ʔ ( V i ) −