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

Therefore,

ʔ ( A ) ≤ inf

n ≥ 0 ʘ (

∼ n ( A )) = ʘ (( ∩ n ≥ 0 ∼ n )( A )) = ʘ ( ∼ ˉ ( A )) .

Using Theorem 3.5 (1) again, we obtain ( 3.12 ).
By symmetry we also have that if t

a
−ₒ

a
−ₒ

ʘ then there is some ʔ with s ʔ

∼ ˉ ) † ʘ .

and ʔ (

Let ≺ be the largest probabilistic simulation, called probabilistic similarity, and

≺∩≺ − 1 , called simulation equivalence .
In general, simulation equivalence is coarser than bisimilarity. However, for reactive
pLTSs, the two relations do coincide. Recall that in a reactive pLTS, for each state s
and action a there is at most one distribution ʔ with s

be the kernel of probabilistic similarity, i.e.

a
−ₒ ʔ . To prove that result,

we need a technical lemma.

†

Lemma 3.3 Let R be a preorder on a set S and ʔ , ʘ ∈ D ( S ) .Ifʔ R ʘ and

† ʔ then ʔ ( C )

ʘ R = ʘ ( C ) for all equivalence classes C with respect to the kernel

R ∩ R − 1 of R .

R ∩ R − 1 . For any s Proof Let us write ≡ for ∈ S , let [ s ] ≡ be the equivalence class

{ ∈ | R ∧ R }

that contains s . Let A s be the set t S s t t s . It is easy to see that

R ( s ) ={ t ∈ S | s R t }

={ t ∈ S | s R t ∧ t R s }{ t ∈ S | s R t ∧ t R s }

= [ s ] ≡ A s

where stands for a disjoint union. Therefore, we have

ʔ ( R ( s )) = ʔ ([ s ] ≡ ) + ʔ ( A s ) and ʘ ( R ( s )) = ʘ ([ s ] ≡ ) + ʘ ( A s ) . (3.13)

We now check that both R ( s ) and A s are R -closed sets, that is R ( R ( s )) ↆ R ( s )

and R ( A s ) ↆ A s . Suppose u ∈ R ( R ( s )). Then there exists some t ∈ R ( s ) such that

t R u , which means that s R t and t R u . As a preorder R is a transitive relation. So we

have s R u that implies u ∈ R ( s ). Therefore we can conclude that R ( R ( s )) ↆ R ( s ).

Suppose u ∈ R ( A s ). Then there exists some t ∈ A s such that t R u , which means

that s R t , t R s and t R u . As a preorder R is a transitive relation. So we have

s R u . Note that we also have u R s . Otherwise we would have u R s , which

means, together with t R u and the transitivity of R , that t R s , a contradiction to the

hypothesis t R s . It then follows that u ∈ A s and then we conclude that R ( A s ) ↆ A s .

† ʘ and ʘ † ʔ ,

We have verified that R ( s ) and A s are R -closed sets. Since ʔ R R

R ≤ R R ≤

we apply Theorem 3.5 (2) and obtain that ʔ ( ( s )) ʘ ( ( s )) and ʘ ( ( s ))

R

ʔ ( ( s )), that is

ʔ ( R ( s )) = ʘ ( R ( s )) . (3.14)

Similarly, using the fact that A s is R -closed we obtain that

ʔ ( A s ) = ʘ ( A s ) (3.15)