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

FS ) † ʘ implies that ʔ = i ∈ I p i · s i , s i

e e

Proof By Lemma 6.1 ʔ (

FS ʘ i , as well

= i ∈ I p i ·

ʱ
⃒ ʔ

as ʘ ʘ i . By Corollary 6.7 and Proposition 6.2 we know from ʔ

for ʔ i ∈ D sub ( S ) such that ʔ = i ∈ I p i ·

ʱ
⃒ ʔ i ʔ i . For each i

that s i ∈ I we

ʱ
⃒

ʱ
⃒

e

ʔ i that there is a ʘ i ∈ D sub ( S ) with ʘ i ʘ i infer from s i

FS ʘ i and s i

and

= i ∈ I p i ·

FS ) † ʘ . Let ʘ :

ʔ i

e

ʘ i . Then Definition 6.2 (2) and Theorem 6.5 (i)

(

ʱ
⃒

FS ) † ʘ and ʘ

yield ʔ (

e

ʘ .

FS ) † ʘ and ʔ

A A e

Lemma 6.22 Suppose ʔ ( ⃒ −ₒ . Then ʘ ⃒ −ₒ .

A e

FS ) †

ʔ

Proof Suppose ʔ ( ʘ and ʔ ⃒ −ₒ . By Lemma 6.21 there exists

some subdistribution ʘ such t ha t ʘ ʘ and ʔ (

e

FS ) † ʘ . From Lemma 6.1

⃒

we know that ʔ = i ∈ I p i ·

FS ʘ i , ʘ = i ∈ I p i ·

e

ʔ s i , s i ʘ i , with s i ∈

A A

for all i ∈ I . Since ʔ

−ₒ , we have that s i −ₒ for all i ∈ I . It follows from

. By Theorem 6.5 (i), we obtain that i ∈ I p i · ʘ i ⃒

A e

FS ʘ i that ʘ i ⃒ ʘ i

s i −ₒ

i ∈ I p i ·

A A

ʘ i

The next result shows how the failure simulation preorder can alternatively be
defined in terms of failure similarity. This is consistent with Definition 5.5 for finite
processes.
Proposition 6.7 Fo r ʔ , ʘ ∈ D sub ( S ) we have ʘ FS ʔ just when there is a ʘ match
with ʘ ⃒ ʘ match

−ₒ . By the transitivity of ⃒ we have that ʘ ⃒ −ₒ .

e

FS ) † ʘ match .

and ʔ (

FS ↆ S × D sub ( S ) be the relation given by s FS ʘ iff ʘ FS s . Then FS Proof Let

= i p i · FS ↆ

e

is a failure simulation; hence

FS . Now supp os e ʘ

FS ʔ . Let ʔ : s i .

⃒ i p i · ʘ i and ʘ i FS s i for each i , whence s i FS ʘ i ,

Then there are ʘ i with ʘ

= i p i ·

e

FS ʘ i . Take ʘ match

e

FS ) † ʘ match .

and thus s i : ʘ i . Definition 6.2 yields ʔ (

e

FS ) †

For the other direction, it suffices to show that the relation ( ·⃐ satisfies

e

FS ) †

the two clauses of Definition 6.19 , yielding ( ·⃐ↆ FS . Here we write ⃐

∈ D sub ( S ), there is a ʘ match with for the inverse of ⃒ . So suppose, for given ʔ , ʘ

FS ) † ʘ match .

ʘ match

e

ʘ ⃒ and ʔ (

⃒ i ∈ I p i ·

ʱ

ʔ i

Suppose ʔ for some ʱ ∈ Act ˄ . By Lemma 6.21 , there is some

ʘ and ( i ∈ I p i ·

ʱ
⃒

e FS ) † ʘ . From Proposition 6.2 ,

ʘ such that ʘ match ʔ i )(

we know that ʘ = i ∈ I p i ·

e FS ) †

ʘ i for subdistributions ʘ i such that ʔ i ( ʘ i

⃒ i p i ·

ʱ

ʘ i

∈ ⃒

for i I . Thus ʘ by the transitivity of (Theorem 6.6 ) and

ʔ i ((

e FS ) †

) ʘ i

·⃐ for each i ∈ I by the reflexivity of ⃐ .

A A

. By Lemma 6.22 we have ʘ match

Suppose ʔ ⃒ −ₒ ⃒ −ₒ . It follows that

A

ʘ ⃒ −ₒ by the transitivity of ⃒ .

ʘ match in Proposition 6.7
immediately above. For the same reason explained in Example 5.14, defining

Note the appearance of the “anterior step” ʘ ⃒

FS

FS ) †

e

simply to be ( (i.e. without anterior step) would not have been suitable.

e

Remark 6.3 FS s ; here no

anterior step is needed. One direction of this statement has been obtained in the
beginning of the proof of Proposition 6.7 ; for the other note that s

For s ∈ S and ʘ ∈ D sub ( S ), we have s

FS ʘ iff ʘ

e

FS ʘ implies