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

˄
⃒

a
−ₒ

˄
⃒ ʔ i ʔ i ʔ

i

for some ʔ i , ʔ i , ʔ s ) † ʔ

ʔ i with ʘ i ( .By

i i

˄
−ₒ

˄
−ₒ

˄
⃒ ʔ 1 | A ʔ 2 ʔ 1 | A ʔ 2 ʔ

1

| A ʔ

Lemma 5.8 we have ʔ 1 | A ʔ 2

2

†

( ʔ
1

| A ʔ 2 ). and ( ʘ 1 | A ʘ 2 ) R

So we have checked that is a simulation.

Since P i S Q i , there must be a ʔ i such that [[ Q i ]]

R

˄
⃒

s ) † ʔ i .By ʔ i and [[ P i ]] (

†

Lemma 5.8 we have [[ P 1 | A P 2 ]] = ([[ P 1 ]] | A [[ P 2 ]] ) R ( ʔ 1 | A ʔ 2 ). Therefore, we

s ) † ( ʔ 1 | A ʔ 2 ). By Lemma 5.8 we also obtain

have [[ P 1 | A P 2 ]] (

˄
⃒

˄
⃒

[[ Q 1 | A Q 2 ]] = [[ Q 1 ]] | A [[ Q 2 ]] ʔ 1 | A [[ Q 2 ]] ʔ 1 | A ʔ 2 ,

which had to be established.

FS is pre-
served under parallel composition. The key step is to show that the binary relation
R ↆ

The case for FS is analogous. As an example, we show that

sCSP × D ( sCSP ) defined by

R ={

( s 1 | A s 2 , ʔ 1 | A ʔ 2 )

|

s 1 FS ʔ 1 ∧ s 2 FS ʔ 2 } : .

is a failure simulation.
Suppose s i FS ʔ i for i

X
−ₒ

= 1, 2 and s 1 | A s 2 for some X ↆ Act . For each

a ∈ X there are two possibilities:

a a a

∈

, since otherwise we would have s 1 | A s 2 • f a A , then s 1 and s 2 .

a a ˄

• f a .

Hence, we can partition the set X into three subsets: X 0 , X 1 and X 2 such that X 0 =
X

∈ A , then either s 1 or s 2 , since otherwise we would have s 1 | A s 2

X 1
ₒ

X 2
ₒ

a
ₒ

\ A and X 1 ∪ X 2 ↆ A with s 1 and s 2 , but allowing s 1 for some a ∈ X 2 and

X 0 ∪ X i
−ₒ

a
ₒ

s 2 for some a ∈ X 1 . We then have that s i for i = 1, 2. By the assumption that

˄
⃒

X 0 ∪ X i
−ₒ

X
ₒ 1, 2, there is a ʔ i ʔ i . Therefore, ʔ 1 | A ʔ 2

s i FS ʔ i for i = with ʔ i as

˄
⃒ ʔ 1 | A ʔ 2 . Hence ʔ 1 | A ʔ 2 can match well. By Lemma 5.8 (i) we have ʔ 1 | A ʔ 2

the failures of s 1 | A s 2 .
The matching of transitions and the using of R to prove the preservation property

of FS under parallel composition are similar to those in the above corresponding

proof for simulations, so we omit them.

5.5.3 Simulations Are Sound for Testing Preorders

In this section we show that simulation is sound for may testing and failure simulation
is sound for must testing. That is, we aim to prove that (i) P

S Q implies P pmay Q

and (ii) P FS Q implies P pmust Q .

S is defined on pCSP , we now extend it to pCSP ˉ ,
keeping Definition 5.5 unchanged.

Originally, the relation