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

= s ∈ ʔ ʔ ( s ) with X ʔ : · X s .

Theorem 3.9 Suppose E is a characteristic equation system. Then s ∼ t if and

only if t ∈ ˁ E ( X s ) .

Proof ( ⃐ ) Let R ={ ( s , t ) | t ∈ ˁ E ( X s ) } . We first show that

† ʘ.

ʘ ∈ [[ X ʔ ]] ˁ E implies ʔ R (3.20)

= i ∈ I p i · s i , then X ʔ = i ∈ I p i · Let ʔ X s i . Suppose ʘ ∈ [[ X ʔ ]] ˁ E .Wehave

= i ∈ I p i · I and t ∈ , that t ∈ t . that ʘ ʘ i and, for all i ∈ ʘ i [[ X s i ]] ˁ E , i.e. s i R

† ʘ i and thus ʔ

It follows that s i R

R

† ʘ .

Now we show that R is a bisimulation.

a
−ₒ ʔ . Then t ∈ ˁ E ( X s )

1. Suppose s R t and s = [ | ˕ s | ] ˁ E . It follows from ( 3.19 )

a
−ₒ ʘ and ʘ ∈

that t ∈ [ | a X ʔ | ] ˁ E . So there exists some ʘ such that t [ | X ʔ | ] ˁ E .

Now we apply ( 3.20 ).
2. Suppose s

a
−ₒ R t and t ʘ . Then t ∈ ˁ E ( X s ) = [ | ˕ s | ] ˁ E . It follows from ( 3.19 )

[ a ] s

that t ∈ [ |

−ₒ ʔ X ʔ |

]. Notice that it must be the case that s can enable action

a

a , otherwise, t ∈ [ | [ a ] ↥| ] ˁ E and thus t cannot enable a either, in contradiction

| s

a
−ₒ

with the assumption t ʘ . Therefore, ʘ ∈ [

−ₒ ʔ X ʔ |

] ˁ E , which implies

a

a
−ₒ

ʘ ∈ [ | X ʔ | ] ˁ E for some ʔ with s ʔ . Now we apply ( 3.20 ).

( ⃒ ) We define the environment ˁ ∼ by

ˁ ∼ ( X s ): ={ t | s ∼ t } .

It suffices to show that ˁ ∼ is a postfixed point of E , i.e.

ˁ ∼ ≤ E ( ˁ ∼ ) (3.21)

because in that case we have ˁ ∼ ≤ ˁ E , thus s ∼ t implies t ∈ ˁ ∼ ( X s ) that in turn

implies t ˁ E ( X s ).

We first show that

∈

† ʘ implies ʘ

ʔ ∼ ∈ [[ X ʔ ]] ˁ ∼ . (3.22)

= i ∈ I p i ·

† ʘ . Using Proposition 3.1 we have that (i) ʔ

Suppose that ʔ ∼ s i , (ii)

= i ∈ I p i · ʘ t i , (iii) s i ∼ t i for all i ∈ I . We know from (iii) that t i ∈ [[ X s i ]] ˁ ∼ .

[[ i ∈ I p i ·

Using (ii) we have that ʘ ∈ X s i ]] ˁ ∼ . Using (i) we obtain ʘ ∈ [[ X ʔ ]] ˁ ∼ .

Now we are in a position to show ( 3.21 ). Suppose t ∈ ˁ ∼ ( X s ). We must prove

that t ∈ [[ ˕ s ]] ˁ ∼ , i.e.

(
s

(
a

[[ [ a ]
s

t ∈ [[ a X ʔ ]] ˁ ∼ ) ∩ X ʔ ]] ˁ ∼ )

a
−ₒ

∈ L

a
−ₒ ʔ ʔ

by ( 3.19 ). This can be done by showing that t belongs to each of the two parts of this
intersection.