Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 156

† ʘ if and only if ʘ can

Lemma 6.5 For subdistributions over a finite set S, ʔ R

be written in the form s ∈ ʔ ʔ ( s ) · ʘ s where each ʘ s ∈ R ( s ) .

= s ∈ ʔ

† ʘ ,it

Proof Suppose ʘ ʔ ( s ) · ʘ s with ʘ s ∈ R ( s ). To show that ʔ R

† ʘ s for each s †

suffices to prove that s R ∈ ʔ ,as R is linear. Since ʘ s ∈ R ( s ),

we can rewrite ʘ s as ʘ s = i ∈ I p i ·

ʘ i s where ʘ i s ∈ R ( s ) for some finite index set

= i ∈ I p i ·

† ʘ s .

I . The fact that s s and s R ʘ i s yields that s R

† ʘ . By Lemma 6.1 we have that

Conversely, suppose ʔ R

ʔ = p i · s i s i R ʘ i ʘ = p i · ʘ i . (6.2)

i ∈ I i ∈ I

= i ∈ I s p i . Hence, we For each s ∈ ʔ , let I s ={ i ∈ I | s i = s } . Note that ʔ ( s )

can rewrite ʘ as follows:

= s ∈ ʔ i ∈ I s p i ·

ʘ ʘ i

= s ∈ ʔ ( i ∈ I s

p i
ʔ ( s ) ·

ʔ ( s ) · ʘ i )

Since the subdistribution i ∈ I s

p i

ʔ ( s ) ·

ʘ i is a convex combination of { ʘ i | i ∈ I s } ,it

must be in R ( s ) due to ( 6.2 ), and the result follows.

Theorem 6.4 (Infinite Linearity) Suppose R is a relation over S × D sub ( S ) , where S

is finite and i ≥ 0 p i =

† ʘ i implies ( i ≥ 0 p i ·

( i ≥ 0 p i ·

†

1 . Then ʔ i R ʔ i ) R ʘ i ) .

Suppose i ≥ 0 p i =

†

Proof 1 and ʔ i R ʘ i for each i ≥ 0. Let ʔ , ʘ denote

i ≥ 0 p i ·

ʔ i and i ≥ 0 p i ·

† ʘ . By Lemma 6.5

ʘ i , respectively. We have to show ʔ R

it is sufficient to show

ʘ = ʔ ( s ) · ʓ s , (6.3)

s ∈ ʔ

where ʓ s ∈ R .

By the same lemma we know that for each i

( s ) for each s ∈ ʔ

† ʘ i ,

≥ 0, since ʔ i R

ʘ i = ʔ i ( s ) · ʘ i s with ʘ i s ∈ R ( s ) . (6.4)

s ∈ ʔ i

Therefore,

= i ≥ 0 p i ·

( s ∈ ʔ i ʔ i ( s )

·

ʘ ʘ i s )

= s ∈ ʔ i ≥ 0 ( p i · ʘ i s

Let w i denote p i · ʔ i ( s ) and note that ʔ ( s ) is the infinite sum i ≥ 0 w i . Therefore,
we can continue:

ʔ i ( s )) ·

= s ∈ ʔ i ≥ 0 w i ·

ʘ ʘ i s

= s ∈ ʔ ʔ ( s ) ( i ≥ 0

w i

·

ʔ ( s ) · ʘ i s ) .