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

and

( r )( ˉ )

n ≥ 0 C

( f n ) ( r )( ˉ ) C f n = 0 =

n ≥ 0

for all ˉ =

ˉ .

2. r −ₒ . Similar to the last case; we have

( r )( ˉ )

n ≥ 0 C

( f n ) ( r )( ˉ )

C f n = 0 =

n ≥ 0

for all ˉ ∈ ʩ .
3. Otherwise, r

˄
−ₒ ʔ for some ʔ ∈ D

( R ). Then we infer that for any ˉ ∈ ʩ ,

n ≥ 0 f n ( r )( ˉ ) n ≥ 0 f n ( ʔ )( ˉ )

C =

by ( 4.1 )

n ≥ 0 f n ( r )( ˉ )

r ∈ ʔ

= ʔ ( r ) ·

n ≥ 0 f n ( r ) ( ˉ )

r ∈ ʔ

= ʔ ( r ) ·

r ∈ ʔ n ≥ 0 ʔ ( r )

= · f n ( r )( ˉ )

r ∈ ʔ

= ·

lim n ₒ∞ ʔ ( r ) f n ( r )( ˉ )

lim n ₒ∞ r ∈ ʔ

= ʔ ( r ) · f n ( r )( ˉ ) by Proposition 4.2

n ≥ 0 r ∈ ʔ

= ʔ ( r ) · f n ( r )( ˉ )

n ≥ 0 f n ( ʔ )( ˉ )

=

n ≥ 0 C

= ( f n )( r )( ˉ )

n ≥ 0 C

( f n ) ( r )( ˉ ) .

=

In the above reasoning, Proposition 4.2 is applicable because we can define the
function f : R

× N ₒ R ≥ 0 by letting f ( r , n ) = ·

f n ( r )( ˉ ) and check that
f satisfies the three conditions in Proposition 4.2 .If R is finite, we can extend it
to a countable set R ↇ

ʔ ( r )

R and require f ( r , n ) = 0 for all r ∈ R \ R and n ∈ N .

a) f satisfies condition C1 . For any r ∈ R and n 1 , n 2 ∈ N ,if n 1 ≤ n 2 , then

f n 1 ≤ f n 2 . It follows that

f ( r , n 1 ) = ʔ ( r ) · f n 1 ( r )( ˉ ) ≤ ʔ ( r ) · f n 2 ( r )( ˉ ) = f ( r , n 2 ) .

} n = 0
is nondecreasing and bounded by ʔ ( r ). Therefore, the limit lim n ₒ∞ f ( r , n )
exists.

∈ { ·

b) f satisfies condition C2 . For any r R , the sequence ʔ ( r ) f n ( r )( ˉ )