Information Technology Reference
In-Depth Information
5.2.3
The Precedence of Probabilistic Choice
Our operational semantics entails that
and
| A distribute over probabilistic choice:
[[ P
( Q p R )]]
=
[[ ( P
Q ) p ( P
R )]]
[[ P
| A ( Q p R )]]
=
[[ ( P
| A Q ) p ( P
| A R )]]
These identities are not a consequence of our testing methodology: they are hardwired
in our interpretation [[__]] of pCSP expressions as distributions.
A consequence of our operational semantics is that, for example, in the process
a. ( b 2
| d the action d can be scheduled either before a , or after the probabilistic
choice between b and c —but it cannot be scheduled after a and before this proba-
bilistic choice. We justify this by thinking of P p Q not as a process that starts with
making a probabilistic choice, but rather as one that has just made such a choice, and
with probability p is no more and no less than the process P . Thus a. ( P p Q )isa
process that in doing the a -step makes a probabilistic choice between the alternative
targets P and Q .
This design decision is in full agreement with previous work featuring nonde-
terminism, probabilistic choice and parallel composition [ 5 , 7 , 12 ]. Moreover, a
probabilistic choice between processes P and Q that does not take precedence over
actions scheduled in parallel can simply be written as ˄. ( P p Q ). Here ˄.P is an
abbreviation for P
c )
P . Using the operational semantics of
in Fig. 5.1 , ˄.P is a
˄
−ₒ
process whose sole initial transition is ˄.P
P , hence ˄. ( P p Q ) is a process
that starts with making a probabilistic choice, modelled as an internal action, and
with probability p proceeds as P . Any activity scheduled in parallel with ˄. ( P p Q )
can now be scheduled before or after this internal action, hence before or after the
making of the choice. In particular, a.˄. ( b 2
| d allows d to happen between a
c )
and the probabilistic choice.
5.2.4
Graphical Representation of pCSP Processes
The set of states reachable from a subdistribution ʔ is the smallest set that contains
ʔ
and is closed under transitions, meaning that if some state s is reachable and
ʱ
−ₒ
s
is reachable as well. We graphically depict the
operational semantics of a pCSP expression P by drawing the part of the pLTS
defined above that is reachable from [[ P ]] as a finite acyclic directed graph in the way
described in Sect. 3.2.
Two examples are described in Fig. 5.2 . Th e interpretation of the simple process
( b c )
ʘ then every state in
ʘ
ʔ , where ʔ is the distribution
resulting from the interpretation of ( d 2 a ), itself a two-point distribution mapping
both the states d. 0 and a. 0 to the probability
( d 2 a ) is the distribution ( b c )
1
2 . The result is again a two-point
distribution, this time mapping the two states ( b c )
1
d and ( b c )
a to
2 . The
Search WWH ::




Custom Search