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

of derivatives; they are closed in the sense (from analysis) of containing all its limit
points where, in turn, limit depends on a Euclidean-style metric defining the distance
between two subdistributions in a straightforward way. Another consequence is that
we can find in any derivation that partially diverges (by no matter how small an
amount) a point at which the divergence is distilled into a state that wholly diverges;
we call this distillation of divergence .

6.5.1 Finite Generability

n , and

A subdistribution over the finite state space S can now be viewed as a point i n R

therefore a set of subdistributions, such as the set of weak derivatives { ʔ | s ⃒ ʔ }

n with the standard Euclidean metric and
proceed to establish useful topological properties of such sets of subdistributions. Re-
call that a set X

n . We endow

corresponds to a subset of R R

n is (Cauchy) closed if for every Cauchy sequence

ↆ R { x n | n ≥ 0 }

with limit x ,if x n ∈ X for every n ≥ 0 then x is also in X .

n then

Lemma 6.9 If X is a finite subset of R X is closed.

In Definition 4.8, we gave a definition of extreme policies for pLTSs of the form

Proof Straightforward.

and showed how they determine resolutions. Here, we generalise these
to derivative policies and show that these generalised policies can also be used to
generate arbitrary weak derivatives of subdistributions over S .

S , ʩ ˄ , ₒ

Definition 6.12 A (static) derivative policy forapLTS S , Act ˄ , ₒ , is a partial

˄
−ₒ function dp : S D ( S ) with the property that dp ( s ) = ʔ implies s ʔ .If dp

is undefined at s , we write dp ( s ) .

A derivative policy dp , as i ts name suggests, can be used to guide the derivation
of a weak deriva t ive. Suppose s

↑ . Otherwise, we write dp ( s ) ↓

⃒ ʔ , using a derivation as given in Definition 6.4 .

Then, we write s ⃒ dp ʔ whenever, for all k ≥ 0,

⊧
⊨

ʔ k ( s ) f dp ( s ) ↓

(a) ʔ k ( s ) =

⊩

0 otherwise

(b) ʔ ( k + 1) = s ∈ ʔ k ʔ k

( s ) · dp ( s )

Intuitively, these conditions mean that the derivation of ʔ from s is guided at each
stage by the policy dp :

Condition (a) implies that the division of ʔ k into ʔ k , the subdistribution that
will continue marching, and ʔ k , the subdistribution that will stop, is determined
by the domain of the derivative policy dp .

•

Condition (b) ensures that the derivation of the next stage ʔ k + 1 from ʔ k

• is

determined by the action of the function dp on the support of ʔ k

.