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

m ∈N n ≥ m C

ʴ n , h ( lfp ( ʴ n , h ))

≤ C by Lemma 4.6 (2)

n ∈N C

ʴ n , h ( lfp ( ʴ n , h ))

= C

n ∈N

ʴ n , h ) .

= lfp ( C

This completes the proof of ( 4.20 ).

∈

(0, 1] and ʔ ⓦ is a subdistribution in a pLTS

ₒ

Lemma 4.8 Suppose ʴ S , ʩ ˄ , .

If T , ʘ ⓦ , ₒ is a resolution of ʔ ⓦ , then we have V

ʴ , h ( ʘ ⓦ )

≤ V

ʴ , max ( ʔ ⓦ ) for any

reward vector h.

Proof Let f : T ₒ S be the resolving function associated with the resolution

T , ʘ ⓦ , ₒ , we show by induction on n that

ʴ , h , n ʴ , h , n ( t ) for any t ∈ T.

V

max ( f ( t ))

≥ V (4.21)

ˉ
−ₒ

The base case n = 0 is trivial. We consider the inductive step. If t ʘ , then

ˉ
−ₒ

ˉ ʴ , h , n ʴ , h , n ( t ). Now suppose that t

f ( t ) f ( ʘ ), thus V

max ( f ( t ))

= h ( ˉ ) = V −ₒ and

˄
−ₒ

˄
−ₒ

ˉ

t ʘ . Then, f ( t ) −ₒ and f ( t ) f ( ʘ ). We can infer that

˄
−ₒ

ʴ , h ,( n + 1)
max

ʴ , h , n

V ( f ( t )) = ʴ · max {V

max ( ʔ )

| f ( t ) ʔ }

ʴ , h , n

≥ ʴ · V

max ( f ( ʘ ))

· s ∈ S f ( ʘ )( s )

ʴ , h , n

= ʴ · V

max ( s )

· t ∈ T ʘ ( t )

ʴ , h , n

max ( f ( t ))

= ʴ · V

· t ∈ T ʘ ( t )

ʴ , h , n ( t )

≥ ʴ · V by induction

ʴ , h , n ( ʘ )

= ʴ · V

ʴ , h ,( n + 1) ( t ) .

= V

So we have proved ( 4.21 ), from which it follows that

ʴ , h
max ( f ( t ))

ʴ , h ( t ) for any t

V ≥ V ∈ T. (4.22)

Therefore, we have that

ʴ , h

max ( ʔ ⓦ )

ʴ , h

max ( f ( ʘ ⓦ ))

V = V

s ∈ S f ( ʘ ⓦ )( s )

ʴ , max ( s )

= · V

t ∈ T ʘ ⓦ ( t )

ʴ , h

= · V

max ( f ( t ))

t ∈ T ʘ ⓦ ( t )

ʴ , h ( t )

≥ · V ( 4.22 )

ʴ , h ( ʘ ⓦ ) .

= V