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

† ʘ if and only if there is a collection of states

Lemma 6.1 ʔ R { s i } i ∈ I , a collection

of subdistributions { ʘ i } i ∈ I , and a collection of probabilities { p i } i ∈ I , for some finite

index set I , such that i ∈ I p i ≤

1 and ʔ , ʘ can be decomposed as follows:

= i ∈ I p i · 1. ʔ s i ;

= i ∈ I p i ·

2. ʘ ʘ i ;

3. For each i ∈ I we have s i R ʘ i .

A simple but important property of this lifting operation is the following:

† ʘ, where

Lemma 6.2 Suppose ʔ R R is any relation in S × D sub ( S ) . Then

(i) | ʔ |≥| ʘ | .

(ii) If R is a relation in S × D ( S ) then | ʔ |=| ʘ | .

Proof This follows immediately from the characterisation in Lemma 6.1 .

† ʘ then 0

So, for example, if ʵ R =| ʵ |≥| ʘ | , whence ʘ is also ʵ .

Remark 6.2 From Lemma 6.1 it also follows that lifting enjoys the following two

properties:

† ʘ , p † p

R ∈ R ≥ 0 and | · |≤ · R ·

(i) (Scaling) If ʔ p ʔ 1 then p ʔ ʘ .

| i ∈ I ʔ i |≤

1 then ( i ∈ I ʔ i )

† †

R ∈ R

(ii) (Additivity) If ʔ i ʘ i for i I and

( i ∈ I ʘ i ), where I is a finite index set.
In fact, we could have presented Definition 6.2 using scaling and additivity instead
of linearity.
The lifting operation has yet another characterisation, this time in terms of choice
functions .

Definition 6.3 Let R ↆ S × D sub ( S ) be a binary relation from states to subdis-

tributions. Then f : S ₒ D sub ( S )isa choice function for R if s R f ( s ) for every

s ∈ dom ( R ). We write Ch ( R ) for the set of all choice functions of R .

then f behaves properly at each state s
in the domain of R , but for each state s outside the domain of

Note that if f is a choice function of R

R , the value f ( s ) can

be arbitrarily chosen.

Proposition 6.1 Suppose R ↆ S × D sub ( S ) is a convex relation. Then for any

† ʘ if and only if there is some choice function

subdistribution ʔ ∈ D sub ( S ) , ʔ R

f ∈ Ch ( R ) such that ʘ = Exp ʔ ( f ) .

Proof First suppose ʘ = Exp ʔ ( f ) for some choice function f ∈ Ch ( R ), that is

= s ∈ ʔ

† ʘ since s

ʘ ʔ ( s ) · f ( s ). It now follows from Lemma 6.1 that ʔ R R f ( s )

for each s ).

Conversely, suppose ʔ

∈ dom ( R

†

R ʘ . We have to find a choice function f ∈ Ch ( R )

such that ʘ = Exp ʔ ( f ). Applying Lemma 6.1 we know that

= i ∈ I p i ·

s i , for some index set I , with i ∈ I p i ≤ (i) ʔ 1

= i ∈ I p i · (ii) ʘ ʘ i .

Now let us define the function f : S ₒ D sub ( S ) as follows:

ʘ i for some ʘ i satisfying s i R