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

FS ) † ʘ by Definition 6.2 (1) which implies ʘ FS s by Proposition 6.7 and the
reflexivity of

e

s (

.
Example 5.14 also shows that

⃒

FS cannot be obtained as the lifting of any relation;
it lacks the decomposition property of Proposition 6.2 . Nevertheless, FS enjoys the

property of linearity, as occurs in Definition 6.2 :

I then i ∈ I p i · ʘ i FS i ∈ I p i · Lemma 6.23 If ʘ i FS ʔ i for i ∈ ʔ i for any

I ) with i ∈ I p i ≤ p i ∈ [0, 1] (i ∈ 1 .

FS ) †

e

Proof This follows immediately from the linearity of ( and ⃒ (cf.

Theorem 6.5 (i)), using Proposition 6.7 .

Example 6.16 (Divergence) From Example 6.3 we know that [[ rec x.x ]] ⃒ ʵ .

A

This, together with ( 6.1 ) in Sect. 6.3.1 , and the fact that ʵ −ₒ for any set of actions

e e

FS ) †

A , ensures that s

FS [[ rec x.x ]] for any s , hence ʘ (

[[ rec x.x ]] for any ʘ ,

and thus that [[ rec x.x ]] FS ʘ . Indeed similar reasoning applies to any ʔ with

˄
−ₒ

˄
−ₒ···

˄
−ₒ··· ʔ = ʔ 0 ʔ 1

because—as explained right before Example 6.3 —this also ensures that ʔ ⃒ ʵ .

⃒

ʵ and hence [[ rec x.x ]]

FS ʵ .

In particular, we have ʵ

Ye t 0

FS [[ rec x.x ]], because the move [[ rec x.x ]] ⃒

ʵ cannot be matched by a

corresponding move from [[ 0 ]]—see Lemma 6.20 .
Example 6.16 shows again that the anterior move in Proposition 6.7 is necessary;
although [[ rec x.x ]]

e FS ) †

FS ʵ , we do not have ʵ ( [[ rec x.x ]], since by Lemma 6.2

e

FS ) † ʘ must have

any ʘ with ʵ ( | ʘ |= 0.

Example 6.17 Referring to the process Q 1 of Example 6.4 , with Proposition 6.7 ,
we easily see that Q 1 FS a. 0 because we have a. 0

e

FS [[ Q 1 ]]. Note that the move

a
−ₒ [[ Q 1 ]] ⃒ [[ a. 0 ]] is crucial, since it enables us to match the move [[ a. 0 ]] [[ 0 ]]

a
−ₒ

A

with [[ Q 1 ]] ⃒ [[ a. 0 ]] [[ 0 ]]. It also enables us to match refusals; if [[ a. 0 ]] −ₒ

A

then A cannot contain the action a , and therefore also [[ Q 1 ]] ⃒ −ₒ .

The converse, that a. 0 FS Q 1 , is also true because it is straightforward to verify

that the relation

{ ( Q 1 ,[[ a. 0 ]]), ( ˄.Q 1 ,[[ a. 0 ]]), ( a. 0 ,[[ a. 0 ]]), ( 0 ,[[ 0 ]] ) }

e FS . We, therefore, have Q 1 FS a. 0 .

is a failure simulation and thus is a subset of

Example 6.18 Let P be the process a. 0 2 ↕ rec x.x and consider the state s 2 intro-

e FS ) †

1

2 ·

[[ a. 0 ]], since rec x.x

e FS ʵ .

duced in Example 6.5 . First, note that [[ P ]] (

1
2 ·

Then, because s 2 ⃒ [[ a. 0 ]] we have s 2 FS [[ P ]]. The converse, that [[ P ]] FS s 2

e FS [[ P ]] follows from the fact that the relation

holds, is true because s 2

{ ( s k ,[[ a. 0 ]] 1 /k ↕ [[ rec x.x ]] ) | k ≥ 2 }∪{ ( a. 0 ,[[ a. 0 ]]), ( 0 ,[[ 0 ]] ) }

is a failure simulation that contains the pair ( s 2 ,[[ P ]]).