Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 119

Fig. 5.7 Two simulation equivalent processes

FS are called (forward) simulation
equivalence and failure simulation equivalence , denoted

The equivalences generated by S and

S and FS , respe ct ively.

If P ∈ sCSP , that is if P is a state in the pLTS of pCSP and so [[ P ]] = P , then

to establish P S Q it is sufficient to exhibit a simul a tion between the state P and the

distribution [[ Q ]], because trivially s s ) † ʔ .

Example 5.13 Consider the two processes P i i n Fig. 5.7 . To show P 1 S P 2 it is
sufficient to exhibit a simulation

s ʔ implies s (

R such that s 0 R t 0 . Let R ↆ sCSP × D ( sCSP )be

defined by

s 0 R t 0 s 1 R ʔ t s 2 R t 3 s 3 R t 3 0 R 0

1

where ʔ t is the two-point distribution mapping both t 1 and t 2 to the probability

2 .
Then it is straightforward to check that it satisfies the requirements of a simulation:
the only nontrivial requirement is that ʔ 1 R

† ʔ 2 . But this follows from the fact that

1
2 ·

1
4 ·

1
4 ·

ʔ 1 = s 1 + s 2 + s 3

1 1 1

ʔ 2 =

2 ·

ʔ t +

4 ·

t 3 +

4 ·

t 3 .

As another example reconsider R 1 = a.c from Fig. 5.5 ,

where for convenience we use process terms to denote their semantic interpretations.
It is easy to see that R 1 S R 2 because of the simulation

a. ( b 2 ↕ c ) and R 2 = a.b 2 ↕

R 1 R

R R 0 R 0

[[ R 2 ]] b b c c

a
−ₒ

a
−ₒ

The transition R 1 ( b 2 ↕ c ) is matched by the transition R 2 ( b 2 ↕ c ) with

( b 2 ↕

R

( b 2 ↕

c ) c ).

Similarly, ( a 2 ↕ c ) ( b 2 ↕ c ) S ( a b ) 2 ↕ c because it is possible to find a

simulation between the state ( a 2 ↕ c ) ( b 2 ↕ c ) and the distribution ( a b ) 2 ↕ c .