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

where within the summations s i = t j , so that, using ( 5.4 ), Φ can also be written as

p i · q j

ʔ ( t j ) ·

Φ ij (5.6)

j ∈ J i ∈ I j

All that remains is to show that ʔ ( s ) † Φ , which we do by manipulating ʔ so that

it takes on a form similar to that in ( 5.6 ):

ʔ =

q j · ʘ j

j ∈ J

p i
ʔ ( t j ) · ʘ j

= q j · using ( 5.5 ) again

j ∈ J i ∈ I j

p i · q j

ʔ ( t j ) ·

= ʘ j .

j ∈ J i ∈ I j

Comparing this with ( 5.6 ) above we see that the required result, ʔ (

s ) † Φ , follows

from an application of the linearity of lifting operation.

ʱ
⃒

ʱ
−ₒ s ) † Φ and ʔ ʔ . Then Φ Φ for some Φ such Lemma 5.6 Suppose ʔ (

that ʔ ( s ) † Φ .

Proof First we consider two claims

˄
−ₒ

˄
⃒

s ) † Φ and ʔ

ʔ , then Φ Φ for some Φ such that ʔ (

s ) † Φ .

(i) If ʔ (

˄
⃒ ʔ , then Φ

ˆ ˄

⃒ Φ for some Φ such that ʔ (

ˆ

s ) † Φ .
The proof of claim (i) is similar to the proof of Lemma 5.5 . Claim (ii) follows from
claim (i) by induction on the length of the derivation of ˄

s ) † Φ and ʔ

(ii) If ʔ (

⃒ . By combining claim (ii)

with Lemma 5.5 , we obtain the required result.

s ) † is both reflexive and transitive on distributions.

Proposition 5.2 The relation (

Proof We leave reflexivity to the reader; it relies on the fact that s s s for every

state s .
For transitivity, let

s ) † Φ
for some intermediate distribution ʔ . Transitivity follows from the two claims

R ↆ sCSP × D ( sCSP )begivenby s R Φ iff s s ʔ (

s ) † ʔ ( s ) † Φ implies ʘ

† Φ

(i) ʘ ( R

s ) † .
Claim (ii) is a straightforward application of Lemma 5.6 , so let us look at (i). From
ʘ (

†

(ii) R is a simulation, hence R ↆ (

s ) † ʔ we have

ʘ = p i · s i , s i s ʔ i , ʔ = p i · ʔ i .

i ∈ I i ∈ I

= i ∈ I p i · s ) † Φ , in analogy to Proposition 3.3 we can show that Φ

Since ʔ ( Φ i

such that ʔ i ( s ) † Φ i . So for each i we have s i R Φ i , from which it follows that

ʘ R

† Φ .