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

In the above definition, we prohibit ʵ from being 1 because we use 1 to represent
the distance between any two incomparable states including the case where one state
may perform a transition and the other may not.
The greatest state-metric is defined as

m max = { m ∈ M | m is a state-metric } .

It turns out that state-metrics correspond to bisimulations and the greatest state-
metric corresponds to bisimilarity. To make the analogy closer, in what follows we
will characterise m max as a fixed point of a suitable monotone function on M . First

we recall the definition of Hausdorff distance.

Definition 3.12 Given a 1-bounded metric d on Z , the Hausdorff distance between
two subsets X , Y of Z is defined as follows:

H d ( X , Y ) = max { sup x ∈ X inf y ∈ Y d ( x , y ), sup y ∈ Y inf x ∈ X d ( y , x ) }

where inf 0.

Next we define a function F on

∅= 1 and sup ∅=

M by using the Hausdorff distance.

a
−ₒ

Definition 3.13 Let der ( s , a ) ={ ʔ | s ʔ } . For any m ∈ M , F ( m )isa

pseudometric given by

F ( m )( s , t ) = max a ∈ L { H m ( der ( s , a ), der ( t , a )) } .

Thus we have the following property.

Lemma 3.6 For all ʵ ∈ [0, 1) , F ( m )( s , t ) ≤ ʵ if and only if:

a
−ₒ

a
−ₒ ʔ then there exists some ʔ such that t ʔ and m ( ʔ , ʔ ) • fs ˆ ≤ ʵ.

a
−ₒ

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

• ft ʔ and ˆ ≤ ʵ.

The above lemma can be proved by directly checking the definition of F , as can the
next lemma.
Lemma 3.7 m is a state-metric iff m F ( m ) .

Consequently we have the following characterisation:

m max =

{ ∈ M | }

m m F ( m ) .

Lemma 3.8 F is monotone on

Because of Lemmas 3.5 and 3.8 , we can apply Theorem 2.1, which tells us that
m max is the greatest fixed point of F . Furthermore, by Lemma 3.7 we know that m max
is indeed a state-metric, and it is the greatest state-metric.
In addition, if our pLTS is image-finite , i.e. for all a

M .

S the set der ( s , a )
is finite, the closure ordinal of F is ˉ . Therefore one can proceed in a standard way
to show that

∈ L , s ∈

{ F i (

m max = ) | i ∈ N}