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