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

The required ( 6.3 ) above will follow if we can show ( i ≥ 0

w i

ʔ ( s ) · ʘ i s )

∈ R ( s ) for

each s ∈ ʔ .

From ( 6.4 ) we know ʘ i s

∈ R ( s ), and therefore, by construction we have

that ( i ≥ 0

w i

ʔ ( s ) ·

ʘ i s ) ∈ ˉ R ( s ). But now an application of Lemma 6.4 yields

ˉ R ( s ) = R ( s ), and this coincides with R ( s ) because (_) is a closure

operator.

Consequently, for finite-state pLTSs we can freely use the infinite linearity
property of the lifting operation.

6.3.2 Weak Transitions

We now formally define a notion of weak derivatives.

Definition 6.4 (Weak ˄ Moves to Derivatives) Suppose we have subdistributions
ʔ , ʔ k

, ʔ k , for k

≥ 0, with the following properties:

ʔ 0 ʔ 0 ʔ = +

˄
−ₒ

ʔ 0 ʔ 1 ʔ 1 +

.

˄
−ₒ ʔ k + 1 + ʔ k + 1 .
.

ʔ k

˄
−ₒ

The moves above with subdistribution sources are lifted in the sense of the

previous section. Then we call ʔ :

= k = 0 ʔ k a weak derivative of ʔ , and write

ʔ to mean that ʔ can make a weak ˄ move to its derivative ʔ .
There is always at least one derivative of any distribution (the distribution itself)
and there can be many. Using Lemma 6.2 it is easily checked that Definition 6.4 is
well-defined in that derivatives do not sum to more than one.
Example 6.2

ʔ ⃒

˄
−ₒ

denote the reflexive transitive closure of the relation ˄

−ₒ
over subdistributions. By the judicious use of the empty distribution ʵ in the definition
of

Let ʔ

⃒ and property ( 6.1 ) above, it is easy to see that

˄
−ₒ

ʘ

ʔ implies ʔ ⃒ ʘ

˄
−ₒ

ʘ means the existence of a finite sequence of subdistributions such

because ʔ

that ʔ = ʔ 0 , ʔ 1 , ... , ʔ k = ʘ , k ≥ 0 for which we can write