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

Example 6.1 consists of all total

distributions whose support is included in S . However, with a definition of con-
ve x closure that requires only binary interpolations of distributions to be included,
{

Let S ={ s i | i ∈ N} . Then { s i | i ∈ N}

s i | would merely consist of all such distributions with finite support.

Convex closure is a closure operator in the standard sense, in that it satisfies

i ∈ N}

• X ↆ X

• X ↆ Y implies X ↆ Y

• X = X .

We say a binary relation R ↆ Y × D sub ( S ) is convex whenever the set { ʔ | y R ʔ } is

convex for every y in Y , and let R denote the smallest convex relation containing R .

6.3.1 Lifting Relations

In a pLTS, actions are only performed by states, in that, actions are given by re-
lations from states to distributions. But rpCSP processes in general correspond to
distributions over states, so in order to define what it means for a process to perform
an action, we need to lift these relations so that they also apply to distributions. In
fact, we will find it convenient to lift them to subdistributions by a straightforward
generalisation of Definition 5.3.

Definition 6.2 Let ( S , L , ₒ )beapLTSand R ↆ S × D sub ( S ) be a relation from

†

states to subdistributions. Then R ↆ D sub ( S ) × D sub ( S ) is the smallest relation that

satisfies:

† ʘ and

(1) s R ʘ implies s R

I implies ( i ∈ I p i · ( i ∈ I p i ·

† ʘ i for all i †

(2) (Linearity) ʔ i R ∈ ʔ i ) R ʘ i ),

where I is a finite index set and i ∈ I p i ≤ 1.

†

R emark 6.1 By construction R is convex. Moreover, because s ( R ) ʘ implies

† ), which means that when considering a lifted relation
we can without loss of generality assume the o ri ginal relation to have been convex.
In fact when

† †

s R ʘ we have R = ( R

† ʘ and s

R is indeed convex, we have that s R R ʘ are equivalent.

ʱ
−ₒ An application of this notion is when the relation is for ʱ ∈ Act ˄ ; in that

ʱ
−ₒ

ʱ
−ₒ

ʱ
−ₒ ) † . Thus, as source of a relation

case we also write we now also

allow distributions, and even subdistributions. A subtlety of this approach is that for
any action ʱ ,wehave

for (

ʱ
−ₒ

ʵ ʵ (6.1)

or i ∈ I p i = simply by taking I 0 in Definition 6.2 . That will turn out to make

ʵ especially useful for modelling the “chaotic” aspects of divergence, in particular
that in the must-case a divergent process can simulate any other.
We have the following variant of Lemma 5.3.

=∅