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

h ep ( ʔ ) and so we

We already know, from Proposition 4.4 , that V

min ( ʔ )

≤ V

ep ( ʔ ) min ( ʔ ). Recall that the function ep is the

concentrate on the converse, V ≤ V V

h defined in ( 4.10 ) above, and interpreted in the
above resolution. So the result follows if we can show that the function

least fixed point of the function C

h
min

V is also

a fixed point. This amounts to proving

⊧
⊨

ˉ
−ₒ

h ( ˉ ) if s

min ( s )

V = −ₒ

0 if s

⊩

min ( ep ( s ))

V otherwise .

However this is a straightforward consequence of ( 4.17 ) above.

ʩ

Theorem 4.2 Let P and Q be any finitely branching processes. Then P

er must Q if

nr must Q

and only if P

Proof It follows from two previous propositions that

h h ( ʘ )

V

min ([[ T | Act P ]] )

= min {V | R , ʘ , ₒ is a resolution of [[ T | Act P ]] }

for any test T , process P and reward vector h . Thus, it is immediate that er must

coincides with nr must .

4.6.2 May Testing

Here we can try to apply the same proof strategy as in the previous section. The
analogue to Proposition 4.4 goes through:

Proposition 4.6 If R , ʘ , ₒ R is a resolution of ʔ, then for any reward vector h,

h ( ʔ ) h

we have

max ( ʘ ) .
Proof Similar to the proof of Proposition 4.4 .
However the proof strategy used in Proposition 4.5 cannot be used to show that

V ≤ V

max can be realised by some static resolution, as the following example shows.
Example 4.7 In analogy with the definition used in the proof of Proposition 4.5 ,
we say that an extreme policy ep (

V

− )is max-seeking if its domain is precisely the set

{ s ∈ S | s −ₒ} , and

˄
−ₒ

˄
−ₒ

ˉ

h h

if s −ₒ but s then V

max ( ʔ )

≤ V

max ( ep ( s )) whenever s

ʔ.

ˉ

˄
−ₒ

max ( s ) max ( ep ( s )), whenever s

This ensures that , and again it is

straightforward to define a max-seeking extreme policy in a finitely branching pLTS.
However the resulting resolution does not in general realise the function

V = V and s −ₒ

max .
To see this, let us consider the (finitely branching) pLTS used in Example 4.6 .
Here in addition to the two states ˉ. 0 and 0 , there is the infinite set

V

{ s 1 , ...s k , ... }

and the transitions