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

for certain s i ∈ S , ʓ i ∈ D sub ( sCSP ) and i ∈ I p i ≤ 1. Let J 1 ={ i ∈ I | ʓ i

= s i | A T 1 } and J 2 ={ i ∈ I | ʓ i = s i | A T 2 } . Note that for each i ∈ ( I − J 1 − J 2 )

˄
−ₒ

we have ʓ i in the form ʓ i | A ( T 1 ʓ i . Now let

T 2 ), where s i

ʔ ₒ = ʔ k = ʔ next ʓ i .

p i · s i , p i · s i , = p i ·

i ∈ ( I − J 1 − J 2 ) i ∈ J k i ∈ ( I − J 1 − J 2 )

where k 1, 2. By construction (i) and (iii) are satisfied, and (ii) follows by property

(2) of Definition 6.2 .

=

| A ( T 1 ⃒

Lemma 6.41 If ʔ T 2 ) ʨ then there are Φ 1 and Φ 2 such that

⃒

Φ 1 +

(i) ʔ Φ 2

(ii) Φ 1 | A T 1 + Φ 2 | A T 2 ⃒ ʨ

Proof ⃒ ʨ . We know from Definition 6.4 that there is

a collection of subdistributions ʨ k , ʨ k

Suppose ʔ 0 | A ( T 1 T 2 )

, ʨ k

, for k ≥ 0, satisfying the properties

ʨ 0 ʨ 0

ʔ 0 | A ( T 1 T 2 ) = ʨ 0 = +

˄
−ₒ

ʨ 1

ʨ 0 ʨ 1

ʨ 1 = +

. .

˄
−ₒ

ʨ k ʨ k + 1 = ʨ k + 1 + ʨ k + 1

.

= k = 0 ʨ k

ʨ

and ʨ is stable.
Take ʓ 0 : 0, we find distributions ʓ k + 1 , ʔ k , ʔ k 1 , = ʨ 0 . By induction on k ≥

ʔ k 2 , ʔ k + 1 such that

˄
−ₒ

ʔ k | A ( T 1 (i) T 2 ) ʓ k + 1

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

(iii) ʔ k = ʔ k

+ ʔ k 1 + ʔ k 2

˄
−ₒ

(iv) ʔ k

ʔ k + 1

ʔ k 2 | A T 2
Induction Step: Assume we already have ʓ k and ʔ k . Note that

ʔ k 1 | A T 1 + (v) ʓ k + 1 = ʔ k + 1 | A ( T 1 T 2 ) +

≤ ʓ k ≤ ʨ k = ʨ k + ʨ k

ʔ k | A ( T 1 T 2 )

and T 1 T 2 can make a ˄ move. Since ʨ is stable, we know that there are two

possibilities— either ʨ k

˄

ʵ or ʨ k

= −ₒ . In both cases it holds that

ʨ k ʔ k | A ( T 1 T 2 ) ≤ .

Proposition 6.2 gives a subdistribution ʓ k + 1 ≤ ʨ k + 1 such that there exists the

˄
−ₒ ʓ k + 1 . Now apply Lemma 6.40 .

transition ʔ k | A ( T 1 T 2 )