Probabilistic Testing Semantics - Semantics of Probabilistic Processes: An Operational Approach - page 72

nonempty subsets of X , we define Exp ʔ F : ; here f ∈ F

means that f : S ₒ X is a choice function , that is, it satisfies the constraint that
f ( s )

={ Exp ʔ ( f ) | f ∈ F }

∈ F ( s ) for all s ∈ S . Recall that a set O is convex if o 1 , o 2 ∈ O and p ∈ [0, 1],

then the weighted average o 1 p ↕ o 2 is also in O .

S , ʔ ⓦ , Act ˄ ,

Definition 4.1 A (probabilistic) process is defined by a tuple ₒ ,

where Act ˄ is a set of actions Act augmented with a special action ˄ , is

apLTSand ʔ ⓦ is a distribution over S , called the initial distribution of the pLTS. We
sometimes identify a process with its initial distribution when the underlying pLTS
is clear from the context.
We now define the parallel composition of two processes.

S , Act ˄ , ₒ

S 1 , ʔ 1 , Act ˄ , S 2 , ʔ 2 , Act ˄ , Definition 4.2 be two

processes, and A a set of visible actions. The parallel composition P 1 | A P 2 is the com-
posite process

Let P 1 = ₒ 1 and P 2 = ₒ 2

S 2 , ʔ 1 × ʔ 2 , Act ˄ ,

S 1 × ₒ where ₒ is the least relation satisfying

the following rules:

ʱ
−ₒ 1 ʔʱ

ʱ
−ₒ 2 ʔʱ s 1 ∈ A s 2 ∈ A

ʱ
−ₒ

ʱ
−ₒ

( s 1 , s 2 ) ʔ × s 2 ( s 1 , s 2 ) s 1 × ʔ

.

a
−ₒ 1 ʔ 1 ,

a
−ₒ 2 ʔ 2

s 1 s 2 a ∈ A

˄
−ₒ

( s 1 , s 2 ) ʔ 1 × ʔ 2

Parallel composition is the basis of testing: it models the interaction of the observer
with the process being tested; and models the observer himself—as a process. Let
ʩ : be a countable set of success actions , disjoint from Act ˄ , define

an ʩ test to be a process

={ ˉ 1 , ˉ 2 , ···}

ˉ i
−ₒ S , ʔ ⓦ , Act ˄ ∪

ʩ , ₒ with the constraint that s and

ˉ j
−ₒ s imply i = j . Let T be the class of all such tests, and write T n for the subclass

T N for n ∈N T n .
To apply test T to process P , we first form the composition T

T

of that uses at most n success actions ˉ 1 , ... , ˉ n ; we write

| Act P and then
resolve all nondeterministic choices into probabilistic choices. Thus, we obtain a set
of resolutions as in Definition 4.3 below. For each resolution, any particular success
action ˉ i will have some probability of occurring; and those probabilities, taken
together, give us a single success tuple for the whole resolution, so that if o is the
tuple, then o ( ˉ i ) is the recorded probability of ˉ i 's occurrence. The set of all those
tuples, i.e. overall resolutions of T | Act P , is then the complete outcome of applying

test T to process P : as such, it will be a subset of [0, 1] ʩ .

Definition 4.3 A resolution of a distribution ʔ ∈ D ( S )inapLTS S , ʩ ˄ , ₒ is a

triple R , ʘ , ₒ R where R , ʩ ˄ , ₒ R is a deterministic pLTS and ʘ ∈ D ( R ), such

that there exists a resolving function f ∈ R ₒ S satisfying

(i) Img f ( ʘ ) = ʔ

ʱ
−ₒ R ʘ for ʱ

ʱ
−ₒ Img f ( ʘ )

(ii) if r ∈ ʩ ˄ , then f ( r )

ʱ
−ₒ

ʱ
−ₒ R .

(iii) if f ( r ) for ʱ ∈ ʩ ˄ , then r

A resolution R , ʩ ˄ , ₒ R is said to be static if its resolving function f R is injective.