Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 142

5.11.1 Probabilistic Equivalences

Whereas the testing semantics explored in the present chapter is based on the idea
that processes should be distinguished only when there is a compelling reason to do
so, (strong) bisimulation semantics [ 15 ] is based on the idea that processes should
be identified only when there is a compelling reason to do so. It has been extended to
reactive probabilistic processes in [ 18 ], to generative ones in [ 19 ], and to processes
combining nondeterminism and probability in [ 12 ]. The latter paper also features a
complete axiomatisation of a probabilistic extension of recursion-free CCS.
Weak and branching bisimulation [ 15 , 20 ] are versions of strong bisimulation that
respect the hidden nature of the internal action ˄ . Generalisations of these notions
to nondeterministic probabilistic processes appear, amongst others, in [ 7 , 14 , 21 -
25 ], with complete axiomatisations reported in [ 23 , 24 , 26 , 27 ]. The authors of
these paper tend to distinguish whether they work in an alternating [ 21 , 22 , 25 ,
27 ]ora nonalternating model of probabilistic processes [ 7 , 14 , 24 , 26 ], the two
approaches being compared in [ 23 ]. The nonalternating model stems from [ 14 ] and
is similar to our model of Sect. 5.2.2 . The alternating model is attributed to [ 12 ],
and resembles our graphical representation of processes in Sect. 5.2.4 . It is easy to
see that mathematically the alternating and nonalternating model can be translated
into each other without loss of information [ 23 ]. The difference between the two
is one of interpretation. In the alternating interpretation, the nodes of form in

our graphical representations are interpreted as actual states a process can be in,
whereas in the nonalternating representation they are not. Take for example the
process R 1 = a. ( b 2 ↕ c ) depicted in Fig. 5.5 . In the alternating representation this
process passes through a state in which a has already happened, but the probabilistic
choice between b and c has not yet been made. In the nonalternating interpretation
on the other hand the execution of a is what constitutes this probabilistic choice;
after doing a there is a fifty-fifty chance of ending up in either state. Although in
strong bisimulation semantics the alternating and nonalternating interpretation lead
to the same semantic equivalence, in weak and branching bisimulation semantics the
resulting equivalences are different, as illustrated in [ 21 , 23 , 25 ]. Our testing and
simulation preorders as presented here can be classified as nonalternating; however,
we believe that an alternating approach would lead to the very same preorders.
Early additions of probability to CSP include work by Lowe [ 28 ], Seidel [ 29 ]
and Morgan et al. [ 30 ]; but all of them are forced to make compromises of some
kind in order to address the potentially complicated interactions between the three
forms of choice. The last [ 30 ] for example applies the Jones/Plotkin probabilistic
powerdomain [ 31 ] directly to the failures model of CSP [ 10 ], the resulting com-
promise being that probability distributed outwards through all other operators; one
controversial result of that is that internal choice is no longer idempotent, and that it
is “clairvoyant” in the sense that it can adapt to probabilistic-choice outcomes that
have not yet occurred. Mislove addresses this problem in [ 32 ] by presenting a de-
notational model in which internal choice distributes outwards through probabilistic

ⓦ