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

ʔ ki ( ʨ k − ʘ ki ) we obtain ʘ k ( i + 1) = ʔ ki + ʘ ki ≤ ( ʨ k − ʘ ki ) + ʘ ki = ʨ k : = ʔ ki ∩ .

So in particular i = 0 ʔ ki ≤ ʨ k .

Using that ʓ k ʨ k

≤ ,wefind

k − 1 k − 1 k − 1

( ʨ k − ʓ k ( ʨ k + ( ʨ k − ʓ k ʔ ki ≥ ʨ k −

ʔ kk = ) − ʔ ki = )) − ʔ ki ,

i = 0 i = 0 i = 0

( ʨ k − k − 1 ʨ k − k − 1 = i = 0 ʔ ki .

hence, ʔ kk =

i = 0 ʔ ki ) i = 0 ʔ ki and thus ʨ k

ʔ kk ∩ =

Now define ʔ ki ʔ ki . This yields ʔ ki = ʔ ki + ʔ ki : = ʔ ki − and thereby

k

k k

ʨ k ʨ k ʓ k ʔ ki = ʔ ki + ʓ k . = ʨ k − = ʔ ki + −

i = 0 i = 0 i = 0

Since i = 0 ʔ ki =

˄
−ₒ ( ʨ k ʓ k

− ) ( ʨ k + 1 − ʓ k + 1 ), by Proposition 6.2 we have

ʓ k + 1 = i = 0 ʔ ( k + 1)( i + 1) for some subdistributions ʔ ( k + 1)( i + 1) such that they
form the transitions ʔ ki

ʨ k + 1 −

˄
−ₒ

ʔ ( k + 1)( i + 1) for i = 0, ... , k . Furthermore, let us define

ʓ k + 1 = ʓ k + 1 . It follows that

ʔ ( k + 1)0 : = ʓ k + 1 −

k k + 1 k + 1

( ʔ ( k + 1)0 + ʓ k + 1 ) ʔ ( k + 1) i + ʓ k + 1 .

ʨ k + 1 = ʔ ( k + 1)( i + 1) + ʓ k + 1 = ʔ ( k + 1) i + =

i = 0 i = 1 i = 0

= k = i ʔ ki ,

This ends the inductive definition and proof. Now let us define ʘ i :

= k = i ʔ ki = k = i ʔ ki . We have that ʘ 0 = k = 0 ʔ k 0 = and ʘ i ʘ i : :

k = 0 ʓ k

˄
−ₒ

ʘ i

ʘ i , and, using Remark 6.2 (ii), ʘ i

= ʓ , ʘ i = + ʘ i + 1 .

Moreover,

∞ ∞ ∞ ∞ k ∞

ʘ i ʔ ki = ʔ ki = ʨ k = = ʨ.

i = 0 i = 0 k = i k = 0 i = 0 k = 0

Definition 6.4 yields ʓ ⃒ ʨ .

6.4 Testing rpCSP Processes

Applying a test to a process results in a nondeterministic, but possibly probabilistic,
computation structure. The main conceptual issue is how to associate outcomes
with these nondeterministic structures. In Sect. 4.2, we have seen an approach of
testing, in which we explicitly associate with a nondeterministic structure a set of
deterministic computations called resolutions, each of which determines a possible
outcome. In this section, we describe an alternative approach, in which intuitively
the nondeterministic choices are resolved implicitly in a dynamic manner. We show
that although these approaches are formally quite different, they lead to exactly the
same testing outcomes.