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

ʔ ₒ = ʔ × = p i · s i , p i · s i

i ∈ ( I − J ) i ∈ J

ʔ next ʓ i , ʓ × =

= p i · p i · ʓ i

i ∈ ( I − J ) i ∈ J

By construction (i) and (iv) are satisfied, and (ii) and (iii) follow by property (2) of
Definition 6.2 .

ʵ then there is a ʔ ∈ D sub ( S ) such that ʔ ʔ and Lemma 6.29 If ʔ | A t ⃒ ⃒

˄
−ₒ p ⃒ ʔ | A t

ʵ.

Proof Suppose ʔ 0 | A t ⃒ ʵ . By Lemma 6.24 there is an infinite sequence

˄
−ₒ

˄
−ₒ

˄
−ₒ ʔ 0 | A t ʨ 1 ʨ 2 ... (6.23)

0, we find distributions ʓ k + 1 , ʔ k , ʔ k , ʔ k + 1 , ʓ k + 1 such that

By induction on k ≥

˄
−ₒ

(i) ʔ k | A t ʓ k + 1

(ii) ʓ k + 1 ≤ ʨ k + 1

ʔ k

ʔ k

(iii) ʔ k = +

˄
−ₒ ʔ k + 1
(v) ʔ k | A t

(iv) ʔ k

˄
−ₒ p ʓ k + 1

ʓ k + 1 .
Induction Base Take ʓ 1 :

(vi) ʓ k + 1 = ʔ k + 1 | A t

+

ʨ 1 and apply Lemma 6.28 .
Induction Step Assume we already have ʓ k , ʔ k and ʓ k

=

. Since ʔ k | A t ≤ ʓ k ≤ ʨ k

˄
−ₒ

˄
−ₒ and ʨ k ʨ k + 1 , Proposition 6.2 givesusa ʓ k + 1 such that ʔ k | A t ʓ k + 1 and

ʓ k + 1 ≤ ʨ k + 1 . Now apply Lemma 6.28 .

Let ʔ :

= k = 0 ʔ k .

By (iii) and (iv) above, we obtain a weak ˄ move

= k = 0 ( ʔ k | A t ), by (v) and Definition 6.2 we have

ʔ 0 ⃒ ʔ . Since ʔ | A t

−ₒ p k = 1 ʓ k

˄

ʔ | A t Note that here it does not matter if ʔ . = ʵ . Since

ʓ k ʵ , it follows from Theorem 6.5 (ii) that ʓ k ≤ ʓ k ≤ ʨ k and ʨ k ⃒ ⃒ ʵ .

Hence by using Theorem 6.5 (i), we obtain that k = 1 ʓ k

⃒ ʵ .

We are now ready to prove the main result of this section, namely that FS is

preserved by the parallel operator.

FS ʔ then ʘ | A Φ FS ʔ | A Φ.

Proposition 6.11 In a finitary pLTS, if ʘ

Proof We first construct the following relation

C

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

FS ʘ

}

FS . As in the proof of Theorem 5.1, one can check that
each strong transition from s

and check that R ↆ

| A t , and the
matching of failures can also be established. So we concentrate on the requirement
involving divergence.
Suppose s

| A t can be matched by a transition from ʘ

FS ʘ and s | A t ⃒ ʵ . We need to find some ʓ , ʨ such that