Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 202

Proof The most difficult case is the closure of failure simulation under parallel
composition, which is proved in Proposition 6.11 . The other cases are simpler, thus
omitted.

Lemma 6.30 In a finitary pLTS, if P FS Q then [ P | Act T ] FS [ Q | Act T ] for any

test T .

Proof We first construct the following relation

C

R : ={ ( s | Act t , ʘ | Act t ) | s

FS ʘ

}

where s | Act t is a state in [ P | Act T ] and ʘ | Act t is a subdistribution in [ Q | Act T ], and

C

show that

FS .
1. The matching of divergence between s

R ↆ

| Act t is almost the same as the
proof of Proposition 6.11 , besides that we need to check the requirements t

| Act t and ʘ

ˉ

−ₒ

ˉ

are always met there.
2. We now consider the matching of transitions.

and ʓ −ₒ

ˉ
−ₒ

ˉ
−ₒ

• f s | Act t then this action is actually performed by t . Suppose t

ˉ
−ₒ

ˉ
−ₒ ʓ . Then s | Act t s | Act ʓ and ʘ | Act t ʘ | Act ʓ . Obviously we have

† .

( s | Act ʓ , ʘ | Act ʓ ) ∈ R

˄
−ₒ

ˉ

• f s , otherwise the ˄ transition would

be a “scooting" transition and the pLTS is not ˉ -respecting. It follows that
t

| Act t then we must have s | Act t −ₒ

ˉ

−ₒ . There are three subcases.

˄
−ₒ

˄
−ₒ

- t ʓ . So the transition s | Act t s | Act ʓ can simply be matched by

˄
−ₒ

ʘ | Act t ʘ | Act ʓ .

˄
−ₒ ʔ . Since s

C

FS ʘ , there exists some ʘ such that ʘ ⃒ ʘ and

- s

FS ) †

ˉ

ʘ . Note that in this case t ʘ | Act t ʔ ( −ₒ . Hence ʘ | Act t ⃒

which can match the transition s | Act t −ₒ ʔ | Act t because we also have

† .

| Act t , ʘ | Act t )

( ʔ ∈ R

a
−ₒ

a
−ₒ

C

- s ʔ and t ʓ for some action a ∈ Act . Since s

FS ʘ , there

a
⃒

FS ) †

exists some ʘ such that ʘ ʘ and ʔ (

C

ʘ . Note that in this

ˉ

ʘ | Act ʓ which can match case t −ₒ . It easily follows that ʘ | Act t ⃒

| Act ʓ , ʘ | Act ʓ )

† .

the transition s | Act t −ₒ ʔ | Act ʓ because ( ʔ ∈ R

A

• Suppose s | Act −ₒ for any A ↆ Act ∪{ ˉ } . There are two possibilities.

ˉ ˉ

- f s | Act t −ₒ , then t −ₒ and there are two subsets A 1 , A 2 of A such that

A 1 A 2

FS ʘ there exists some ʘ such that

s −ₒ , t −ₒ and A = A 1 ∪ A 2 . Since s

A 1 A

ʘ and ʘ ʘ | Act t ʘ ⃒ −ₒ . Therefore, we have ʘ | Act t ⃒ −ₒ .

ˉ
−ₒ

ˉ
−ₒ

ˉ
−ₒ - f s | Act t then t and ˉ ∈ A . Therefore, we have ʘ | Act t and

˄

ʘ | Act t −ₒ because there is no “scooting” transition in ʘ | Act t . It follows

A

that ʘ | Act t −ₒ .

C

Therefore, we have shown that

FS , from which our expected result can
be established by using similar arguments as in the last part of the proof of
Proposition 6.11 .

R ↆ