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

Finally, we need a property that is the converse of transitivity. If one executes
a given weak derivation partly, by stopping more often and moving on less often,
one makes another weak transition that can be regarded as an initial segment of the
given one. We need the property that after executing such an initial segment, it is
still possible to complete the given derivation.

which concludes the proof.

Definition 6.5 A weak derivation Φ ⃒ ʓ is called an initial segment of a weak

, ʓ k , ʨ k 0 there are ʓ k , ʓ k , ʨ k , ʨ k derivation Φ ⃒ ʨ if for k ≥ ∈ D sub ( S ) such

that ʓ 0 = ʨ 0 = Φ and

ʓ k ʓ k ʨ k ʨ k ʓ k ʨ k

ʓ k = + ʨ k = + ≤

˄
−ₒ

˄
−ₒ

ʓ k ʨ k

ʓ k + 1 ʨ k + 1 ʓ k ≤ ʨ k

= i = 0 ʓ k = i = 0 ʨ k

˄
−ₒ ( ʨ k ʓ k ʓ ʨ − ) ( ʨ k + 1 − ʓ k + 1 ) .

Intuitively, in the derivation Φ ⃒ ʨ , for each k ≥ 0, we only allow a portion of

ʨ k to make ˄ moves, and the rest remains unmoved even if it can enable ˄ moves,
so as to obtain an initial segment Φ ʓ . Accordingly, each ʓ k includes the

corresponding unmoved part of ʨ k , which is eventually collected in ʓ . Now from
ʓ if we let those previously unmoved parts perform exactly the same ˄ movesasin
Φ

⃒

ʨ , we will end up with a derivation leading to ʨ . This is formulated in the
following proposition.

⃒

Proposition 6.4 If Φ ⃒ ʓ is an initial segment of Φ ⃒ ʨ , then ʓ ⃒ ʨ .

Proof For any subdistributions ʔ , ʘ ∈ D sub ( S ), we define two new subdistributions

ʔ ∩ ʘ ∈ D sub ( S ) by letting ( ʔ ∩ ʘ )( s ): = min ( ʔ ( s ), ʘ ( s )) and ʔ − ʘ ∈ D sub ( S )

by ( ʔ − ʘ )( s ): = max ( ʔ ( s ) − ʘ ( s ), 0). So we have ʔ − ʘ = ʔ − ( ʔ ∩ ʘ ). Observe

that in case ʘ ≤ ʔ , and only then, we have that ( ʔ − ʘ ) + ʘ = ʔ .

, ʓ k , ʨ k , ʨ k , ʨ k

Let ʓ k , ʓ k

∈ D sub ( S ) be as in Definition 6.5 . By induction on

0 we define ʔ ki , ʔ ki and ʔ ki , for 0 k ≤ ≤ i ≤ k , such that

ʓ k (i) ʔ k 0 =

(ii) ʨ k = i = 0 ʔ ki + ʓ k

(iii) ʨ k = i = 0 ʔ ki
(iv) ʔ ki = ʔ ki + ʔ ki
(v) ʔ ki

˄
−ₒ

ʔ ( k + 1)( i + 1)

ʓ 0

= =

ʓ 0 − ʓ 0

=

ʨ 0 − ʓ 0 Induction Base: Let ʔ 00 : . This way the first two

equations are satisfied for k = 0. All other statements will be dealt with fully by the

induction step.

Induction Step: Suppose ʔ ki for 0 ≤ i ≤ k are already known, and moreover

we have ʨ k = i = 0 ʔ ki + ʓ k

. With induction on i we define ʔ ki

: = ʔ ki ∩

( ʨ k − i − 1

0 ʔ kj ) and establish j = 0 ʔ kj ≤

ʨ k . Namely, writing ʘ ki for i − 1

0 ʔ kj , j = j =

ʨ k ʨ k surely ʘ k 0 = ʵ ≤ , and when assuming that ʘ ki ≤ and defining