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

A resolution has as its main effect the choice in any state of a single outgoing
transition from all available ones with a same label; but f can be noninjective, so
that the choice can vary between different departures from that state, depending,
e.g., on the history of states and actions that led there. Further, since a single state
of S can be split into a distribution over several states of R , all mapped to it by f ,
probabilistic interpolation between distinct choices is obtained automatically.
Static restrictions are particularly simple, in that they do not allow states to be
resolved into distributions, or computation steps to be interpolated.

Example 4.1 Consider the pLTS in Fig. 4.1 (a), with initial distribution s 1 . One of its
resolutions is described in (b). The associated resolving function f is the following.

f ( r 1 ) = f ( r 2 ) = f ( r 4 ) = f ( r 5 ) = s 1

= =

f ( r 3 ) f ( r 6 ) s 2

f ( r 7 ) = s 3

f ( r 8 ) = s 4 .

From state s 1 , there are three outgoing transitions all labelled with ˄ . According to
the resolution in (b), the first time s 1 is visited, the transition s 1

˄
−ₒ

s 1 is chosen with

˄
−ₒ

probability 2 / 3 and the transition s 1 s 2 with probability 1 / 3. The second time

˄
−ₒ s 1 is visited, the transition s 1 s 2 is taken with probability 1 / 4 and the transition

˄
−ₒ

s 1 s 4 with probability 3 / 4.

We now explain how to associate an outcome with a particular resolution which,
in turn, will associate a set of outcomes with a distribution in a pLTS. Given a
deterministic pLTS

s 3 2 ↕

R , ʩ ˄ , ₒ , consider the function

[0, 1] ʩ ) [0, 1] ʩ ) defined by

C :( R ₒ ₒ ( R ₒ

⊧
⊨

ˉ
−ₒ 1 if r

ˉ ˄

C ( f )( r )( ˉ ): = −ₒ −ₒ (4.1)

0 if r and r

⊩

˄
−ₒ

ˉ

Exp ʔ ( f )( ˉ ) f r −ₒ and r ʔ .

We view the unit interval [0, 1] ordered in the standard manner as a complete lattice;
this induces the structure of a complete lattice on the product [0, 1] ʩ and in turn

[0, 1] ʩ

on the set of functions R ₒ via the partial order ≤ defined pointwise by

letting f is easily seen to be

monotone and therefore has a least fixed point, which we denote by

≤ g iff f ( r ) ≤ f ( g ) for all r ∈ R . The function C

V R , ʩ ˄ , ₒ ; this

is abbreviated to V when the resolution in question is understood.

A

Now let ( T , P ) denote the set of vectors

Exp ʘ V R , ʩ ˄ , ₒ | A ( T , P ): ={ R , ʘ , ₒ is a resolution of [[ T | Act P ]] } (4.2)

where [[ T | Act P ]] stands for the initial distribution of the process T | Act P .
We note that the result set A ( T , P ) is convex.