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

p i
ʔ ( s ) ·

• f s ∈ ʔ then f ( s ) = ʘ i ;

{ i ∈ I | s i = s }

ʘ for any ʘ with s ʘ ;

• f s ∈ dom ( R ) \ ʔ then f ( s ) = R

• otherwise, f ( s ) = ʵ , where ʵ is the empty subdistribution.

= { i ∈ I | s i = s } p i and therefore by convexity s ∈ R

Note that if s ʔ , then ʔ ( s ) f ( s );

so f is a choice function for R as s R f ( s ) for each s ∈ dom ( R ). Moreover, a simple

= i ∈ I p i · calculation shows that Exp ʔ ( f ) ʘ i , which by (ii) above is ʘ .

An important further property is the following:

( i ∈ I p i

† ʘ

Proposition 6.2 (Left-Decomposable) If · ʔ i ) R then ʘ =

i ∈ I p i ·

† ʘ i for each i

ʘ i for some subdistributions ʘ i such that ʔ i R ∈ I .

Proof It is possible to adapt the proof of Proposition 3.3. But here we provide
another proof that takes advantage of choice functions.
Let ʔ

= i ∈ I p i ·

† †

R ʘ , where ʔ ʔ i . By Proposition 6.1 , using that R =

R ) † , there is a choice function f

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

† ʘ i

ʘ i : = Exp ʔ i ( f ) for i ∈ I . Using that ʔ i ↆ ʔ , Proposition 6.1 yields ʔ i R

for i ∈ I . Finally,

i ∈ I p i ·

ʘ i = i ∈ I p i · s ∈ ʔ i ʔ i ( s ) · f ( s )

= s ∈ ʔ i ∈ I p i · ·

ʔ i ( s ) f ( s )

= s ∈ ʔ ʔ ( s ) · f ( s )

= Exp ʔ ( f )

= ʘ.

( i ∈ I p i ·

†

The converse to the above is not true in general; from ʔ ʘ i )it

does not fo llow tha t ʔ can corr espondingl y be decomposed. For example, we have
a. ( b 2 ↕

R

a
−ₒ

1 1 1 1

c )

2 ·

b +

2 ·

c , yet a. ( b 2 ↕ c ) cannot be written as

2 ·

ʔ 1 +

2 ·

ʔ 2 such

a
−ₒ

a
−ₒ

that ʔ 1 c .

In fact, a simplified form of Proposition 6.2 holds for unlifted relations, provided
they are convex:

b and ʔ 2

If ( i ∈ I p i ·

= i ∈ I p i ·

† ʘ and

R R

Corollary 6.1 s i ) is convex, then ʘ ʘ i for

subdistributions ʘ i with s i R

∈

ʘ i for i I .

= i ∈ I p i · Proof Take ʔ i to be s i in Pr oposition 6.2 , whence ʘ ʘ i for some

† ʘ i for i ∈ I . Because

subdistributions ʘ i such that s i R R is convex, we then have

s i R ʘ i from Remark 6.1 .

As we have seen in Proposition 3.4, the lifting operation is monotone, that is
R 1 ↆ R 2 implies R 1 † ↆ R 2 † , and satisfies the following monadic property with

respect to composition.

Lemma 6.3 Let R 1 , R 2 ↆ S × D sub ( S ) . Then the forward relational composition

R 1 † · R 2 † R 1 · R 2 ) † . is equal to the lifted composition (