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

3. Another approach of testing [ 4 ] employs a countable set of special actions
ʩ ={ ˉ 1 , ˉ 2 , ... } to report success. When applied to probabilistic processes, this

approach uses the function space [0, 1] ʩ as the set of outcomes and the standard
partial order for real functions: for any o 1 , o 2 ∈ O

,wehave o 1 ≤ o 2 if and only

if o 1 ( ˉ ) ≤ o 2 ( ˉ ) for every ˉ ∈ ʩ . When ʩ is fixed, an outcome o ∈ O can be

considered as a vector , with o ( ˉ i ) representing the probability

of success observed by action ˉ i . Therefore, this approach is called vector-based
testing .

o ( ˉ 1 ), o ( ˉ 2 ), ...

For the second instance above, there is a useful simplification: the Hoare and Smyth
preorders on closed subsets of [0, 1], in particular on finite subsets of [0, 1], are
determined by their maximum and minimum elements, respectively.

Proposition 4.1 Let O 1 , O 2 be nonempty closed subsets of [0, 1] , we have

(i) O 1 ≤ Ho O 2 if and only if max ( O 1 ) ≤ max ( O 2 )

(ii) O 1 ≤ Sm O 2 if and only if min ( O 1 ) ≤ min ( O 2 ) .

Proof Straightforward calculations.

Remark 4.1 Another formulation of the Hoare and Smyth preorders can be given as
follows. Let ( X ,

≤ ↆ

) be a partially ordered set. If A X , then the upper set and the

lower set of A are defined by ↑ A ={ a ∈ X | a ≤ a for some a ∈ A } and dually

a ∈ a ≤

↓ A ={ X | a for some a ∈ A } , respectively. Then for any nonempty

A , B ↆ X ,wehave

1. A ≤ Ho B if and only if ↓ A ↆ↓ B ;

2. A ≤ Sm B if and only if ↑ A ↇ↑ B .

As in the nonprobabilistic case [ 1 ], we could also define a testing preorder combining
the may-must-preorders; we will not study this combination here.

4.2 Testing Probabilistic Processes

We start with some notation. For ʘ , a distribution over R and function f : R ₒ S ,

Img f ( ʘ ) is the distribution over S given by

Img f ( ʘ )( s ) = { ʘ ( r ) | r ∈ R and f ( r ) = s }

for any s ∈ S .For ʔ , a distribution over S and function f : S ₒ X into a vector
space X , we sometimes write Exp ʔ ( f ) or simply f ( ʔ ) for s ∈ S ʔ ( s ) f ( s ), the

expected value of f . Our primary use of this notation is with X being the vector space
of reals, but we will also use it with tuples of reals, or distributions over some set. In
the latter case, this amounts to the notation i ∈ I p i ·

·

ʔ i , where I is a finite index set

and i ∈ I p i = 1. When p ∈ [0, 1], we also write f 1 p ↕ f 2 for p · f 1 + (1 − p ) · f 2 .

ₒ P + ( X ) with P + ( X ) being the collection of More generally, for function F : S