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

For the first claim, we observe that static resolutions are still resolutions and by
Lemma 4.1 , the set ( T , P ) is convex. If P and T are finitary, their composition

P | Act T is finitary too. The set

A

A f ( T , P ) is the convex closure of a finite number of
points, so it is clearly Cauchy closed.
For the second claim, we observe that Proposition 4.6 and Theorem 4.3 imply
that

f ( T , P ) max ([[ T h ( T , P ) .

A = V | Act P ]] ) = A (4.23)

Similarly, Propositions 4.4 and 4.5 imply that

h min ([[ T h ( T , P ) .

A

f ( T , P )

= V | Act P ]] ) = A (4.24)

We also note that for any deterministic process R , ʘ , ₒ , it holds that

h ( r )

· V = V

h ( r ) (4.25)

for any r ∈ R , since an easy inductive proof establishes that

n ( r ) h , n ( r )

h · V = V

for all n .

For the only-if direction, we apply Theorem 4.1 ; this direction does not require
p -closure.
For the if direction, we prove the must-case in the contrapositive; the may-case
is similar.

∈ N

pmust Q

P

iff A ( T , P ) ≤ Sm A ( T , Q ) for some ʩ test T

implies

A f ( T , P )

≤ Sm A ( T , Q ) by Claim 1

iff h · A f ( T , P ) ≤ h · A ( T , Q ) for some h ∈ [0, 1] ʩ ; Claim 1 ; Theorem 4.1

h
f ( T , P ) ≤

h ( T , Q )

iff

A A

by ( 4.25 )

h ( T , P ) h ( T , Q )

iff

A

≤

A

Claim 2

ʩ
nr must Q.

implies P

We now show that for finitary processes, scalar testing is equally powerful as
finite-dimensional reward testing.
Theorem 4.6

For any n ∈ N and finitary processes P , Q, we have

nr may Q

P iff P nr may Q

nr must Q

P iff P nr must Q.

Proof The only-if direction is trivial in both cases. For if we prove the must-case

in the contrapositive; the may-case is similar.