Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 130

1
q i ( p i o i +

p j p ji o ji )

o i =

j ∈ J

for each i 0.

It can be checked by arithmetic that q i , ʔ i , o i have the required properties,

∈ I , except that ʔ i and o i are chosen arbitrarily in case q i =

viz. that i ∈ I q i = = i ∈ I q i o i and that 1, that o

˄
⃒

ˆ

ʔ j s p i · s + p j ·

i ∈ I j ∈ J

˄
⃒

ʔ ji p i · s + p j · p ji · by ( 5.17 ) and Lemma 5.4

i ∈ I j ∈ J i ∈ I

=

q i ·

ʔ i .

i ∈ I

Finally, it follows from ( 5.15 ) and ( 5.19 ) that o i ∈ A ( T i , ʔ i ) for each i ∈ I .

(b) Let ʔ ( s j ). Without loss of generality we may as-

sume that J is a nonempty finite set disjoint from I . Using the condition that
A

ʔ ={ s j } j ∈ J and r j =

( T , ʔ ): = Exp ʔ A ( T , __), if o ∈ A ( T , ʔ ) then

r j o j

=

o (5.20)

j ∈ J

o j ∈ A

( T , s j ) . (5.21)

For each j ∈ J , we know by the induction hypothesis that

˄
⃒

ʔ ji s j q ji · (5.22)

i ∈ I

o j = q ji o ji (5.23)

i ∈ I

o ji ∈ A ( T i , ʔ ji ) (5.24)

{ q ji } i ∈ I with i ∈ I q ji = for some 1. Thus let

q i = r j q ji

j ∈ J

1
q i

r j q ji · ʔ ji

ʔ i =

j ∈ J

1
q i

r j q ji o ji o i =

j ∈ J

again choosing ʔ i and o i arbitrarily in case q i = 0. As in the first case, it can be

shown by arithmetic that the collection r i , ʔ i , o i has the required properties.