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

Proof We first prove the case ʱ = ˄ . For each i ∈ I there is a number k i such that

˄
−ₒ

˄
−ₒ

˄
−ₒ ···

˄
−ₒ ʔ i . Let k

ʔ i = ʔ i 0 ʔ i 1 ʔ i 2 ʔ ik i = = max { k i | i ∈ I } ,

˄
−ₒ using that I is finite. Since we have Φ ( S ), we can add spurious

transitions to these sequences, until all k i equal k . After this preparation the lemma
follows by k applications of the linearity of the lifting operation (cf. Definition 5.3 ),
taking

Φ for any Φ ∈ D

˄
−ₒ for R .

Act now follows by one more application of the linearity of lifting
operation, this time with

The case ʱ ∈

a
−ₒ R =

, preceded and followed by an application of the

case ʱ = ˄ .

ʱ
−ₒ

ʱ
⃒ s ) † Φ and ʔ ʔ . Then Φ Φ for some Φ such

Lemma 5.5 Suppose ʔ (

that ʔ (

s ) † Φ .

Proof First ʔ ( s ) † Φ means that

ʔ = p i · s i , s i s Φ i , Φ = p i · Φ i ; (5.2)

i ∈ I i ∈ I

ʱ
−ₒ ʔ means

also ʔ

ʱ
−ₒ ʘ j , ʔ =

ʔ = q j · t j , t j q j · ʘ j , (5.3)

j ∈ J j ∈ J

and we can assume without loss of generality that all the coefficients p i , q j are
nonzero. Now define I j ={ i ∈ I | s i = t j } and J i ={ j ∈ J | t j = s i } , so that

trivially

{ ( i , j ) | i ∈ I , j ∈ J i }={ ( i , j ) | j ∈ J , i ∈ I j } (5.4)

and note that

ʔ ( s i ) = q j and ʔ ( t j ) = p i (5.5)

j ∈ J i i ∈ I j

Because of ( 5.5 )wehave

q j
ʔ ( s i ) ·

Φ = p i · Φ i = p i · Φ i

i ∈ I i ∈ I j ∈ J i

p i · q j

ʔ ( s i ) ·

= Φ i

i ∈ I j ∈ J i

Now for each j in J i we know that in fact t j = s i , and so from the middle parts of

ʱ
⃒ s ) † Φ ij . Lemma 5.4 yields ( 5.2 ) and ( 5.3 ) we obtain Φ i Φ ij such that ʘ j (

p i · q j

ʔ ( s i ) ·

ʱ
⃒

Φ = Φ Φ ij