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

6.4.2 Comparison with Resolution-Based Testing

The derivation of extreme derivatives, via the schema in Definition 6.4 , involves the
systematic dynamic resolution of nondeterministic states, in each transition from
ʔ k to ʔ k + 1 . In the literature, various mechanisms have been proposed for making
these choices; for example policies are used in [ 6 ], adversaries in [ 7 ], schedulers
in [ 8 ], ... . Here, we concentrate not on any such mechanism but rather the results
of their application. In general, they reduce a nondeterministic structure, typically a
pLTS, to a set of deterministic structures. To describe these deterministic structures,
in Sect. 4.2, we adapted the notion of resolution defined in [ 9 , 10 ] for probabilistic
automata, to pLTSs.
Therefore, we have now seen at least two ways of associating sets of outcomes
with the application of a test to the process. The first, in Sect. 6.4.1 , uses extreme
derivations in which nondeterministic choices are resolved dynamically as the deriva-
tion proceeds, while in the second, in Sect. 4.2, we associate with a test and a process
a set of deterministic structures called resolutions. In this section, we show that the
testing preorders obtained from these two approaches coincide.
First, let us see how an extreme derivation can be viewed as a method for
dynamically generating a resolution.
Theorem 6.7 (Resolutions from Extreme Derivatives) Suppose ʔ ⃒ ʔ in

apLTS of ʔ, with resolving

function f , such that ʘ ⃒ R ʘ for some ʘ with ʔ = Img f ( ʘ ) .
Proof

S , ʩ ˄ , ₒ . Then there is a resolution R , ʘ , ₒ R

Consider an extreme derivation of ʔ ⃒ ʔ , as given in Definition 6.4 where

all ʔ k

are assumed to be stable. To define the corresponding resolution R , ʘ , −ₒ R

we refer to Definition 4.3. First, let the set of states R be S × N and the resolving

function f : R ₒ S be given by f ( s , k ) = s . To complete the description, we must

ʱ
−ₒ

define the partial functions , for ʱ = ˉ and ʱ = ˄ . These are always defined

ʱ
−ₒ so that if ( s , k ) ʓ then the only states in the support of ʓ are of the form

( s , k 1). In the definition we use ʘ ↓ k , for any subdistribution ʘ over S ,tobethe

subdistribution over R given by

+

ʘ ( s ) f t

= ( s , k )

ʘ ↓ k ( t ) =

0 otherwise

Note that by definition
(a) Img f ( ʘ ↓ k ) =

ʘ

(b) ʔ ↓ k
k

ʔ ₒ↓ k
k

ʔ ×↓ k
k

= +

ˉ
−ₒ R is straightforward; its domain consists of states ( s , k ), where

The definition of

ˉ
−ₒ ʔ k ʔ ↓ k + 1 s ∈ and is defined by letting ( s , k ) for some arbitrarily chosen

s

ˉ
−ₒ s ʔ s .