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

FS ) †

˄
−ₒ p

C

Proposition 6.10 Suppose ʔ ( ʘ and ʔ | A t ʓ . Then

˄
−ₒ⃒

†

ʘ | A t ⃒ ʨ for some ʨ such that ʓ R ʨ , where R is the relation

FS ʘ

{ ( s | A t , ʘ | A t ) | s } .

FS ʘ and

Proof We first show a simplified version of the result. Suppose that s

˄
−ₒ p ʓ ; we prove this entails ʘ

˄
−ₒ⃒

† ʨ . There
are only two possibilities for inferring the above productive move from s

s | A t | A t ⃒ ʨ such that ʓ R

| A t :

˄
−ₒ

(i) ʓ = s | A Φ where t Φ and

a
−ₒ

a
−ₒ

= | A Φ where for some a ∈

(ii) ʓ ʔ A , s ʔ and t Φ .

˄
−ₒ In the first case, we have ʘ | A t ʘ | A Φ by using Lemma 6.27 (2) and also

†

FS ʘ

that ( s | A Φ ) R ( ʘ | A Φ ) by Lemma 6.27 (5), whereas in the second case, s

a
−ₒ⃒

FS ) † ʘ , and we have

ʘ for some ʘ ∈ D sub ( S ) with ʔ (

C

implies ʘ ⃒

˄
−ₒ⃒ ʘ | A Φ by Lemma 6.27 (1) and (3), and ( ʔ | A Φ )

†

( ʘ | A Φ )by

ʘ | A t ⃒ R

Lemma 6.27 (5).
The general case now follows using a standard decomposition/recomposition
argument. Since ʔ

˄
−ₒ p ʓ , Lemma 6.1 yields

| A t

˄
−ₒ p ʓ i ,

=

p i · s i | A t

=

p i ·

ʔ s i , ʓ ʓ i ,

i ∈ I i ∈ I

S , ʓ i ∈ D sub ( S ) and i ∈ I p i ≤

for certain s i ∈ 1. In analogy with Proposition 6.8 ,

FS ) †

C
FS

C

we can show that is convex. Hence, since ʔ ( ʘ , Corollary 6.1 yields

= i ∈ I p i ·

C

that ʘ ʘ i for some ʘ i ∈ D sub ( S ) such that s i

FS ʘ i for i

∈ I . By the

˄
−ₒ⃒

above argument, we have ʘ i | A t ⃒ ʨ i for some ʨ i ∈ D sub ( S ) such that

† ʨ i . The required ʨ can be taken to be i ∈ I p i ·

ʓ i R ʨ i as Definition 6.2 (2) yields

˄
−ₒ⃒

† ʨ and Theorem 6.5 (i) and Definition 6.2 (2) yield ʘ

Our next result shows that we can always factor out productive moves from an
arbitrary action of a parallel process.

R | A t ⃒ ʨ .

ʓ

˄
−ₒ ʓ . Then there exists subdistributions ʔ ₒ , ʔ × ,

ʔ next , ʓ × (possibly empty) such that

Lemma 6.28 Suppose ʔ | A t

ʔ ₒ + ʔ ×

(i) ʔ =

˄
−ₒ (ii) ʔ ₒ ʔ next

˄
−ₒ p ʓ ×

(iii) ʔ × | A t

ʔ next ʓ × (iv) ʓ = | A t +

˄
−ₒ Proof By Lemma 6.1 ʔ | A t ʓ implies that

˄
−ₒ

ʔ = p i · s i , s i | A t ʓ i , ʓ = p i · ʓ i ,

i ∈ I i ∈ I

S , ʓ i ∈ D sub ( S ) and i ∈ I p i ≤

˄
−ₒ p ʓ i } for certain s i ∈ 1. Let J ={ i ∈ I | s i | A t .

J ) the subdistribution ʓ i has the form ʓ i | A t , where

Note that for each i ∈ ( I −

˄