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

1/2 1/2

1/3 1/3

1/3

˄ ˄ ˄ ˄

˄ ˄ a ˄

a ˄

a

d d

bd cdba ca

bd cdba ca

(a) (b)

Fig. 5.2 The pLTSs of example processes

end result in (a) is obtained by further interpreting these two states using the rules in
Fig. 5.1 . In (b) we show the graphical representation that results when this term is
combined probabilistically with the simple process a. 0 .
To sum up, the operational semantics endows pCSP with the structure of a pLTS,
and the function [[ ]] interprets process terms in pCSP as distributions in this pLTS,

which can be represented by finite acyclic directed graphs (typically drawn as trees),
with edges labelled either by probabilities or actions, so that edges labelled by actions
and probabilities alternate (although in pictures we may suppress 1-labelled edges
and point distributions).

−

5.2.5 Testing pCSP Processes

Let us now turn to applying the testing theory from Sect. 4.1 to pCSP . As with
the standard theory [ 3 , 4 ], we use as tests any process from pCSP itself, which
in addition can use a special symbol ˉ to report success. For example, the term
a.ˉ 4 ↕ ( b c.ˉ ) is a probabilistic test, which 25 % of the time requests an a action,

and 75 % requests that c can be performed. If it is used as must test, the 75 % that
requests a c action additionally requires that b is not possible. As in [ 3 , 4 ], it is not the
execution of ˉ that constitutes success, but the arrival in a state where ˉ is possible.
The introduction of the ˉ action is simply a method of defining a success predicate
on states without having to enrich the language of processes explicitly with such
predicates.
Formally, let ˉ Act ˄ and write Act ˉ and Act ˄ .

In Fig. 5.1 we now let a range over Act ˉ and ʱ over Act ˄ . Tests may have subterms
ˉ.P , but other processes may not. We write pCSP ˉ for the set of all tests. To apply
the test T to the process P we run them in parallel, tightly synchronised; that is, we
run the combined process T

∈ for Act ∪{ ˉ } for Act ∪{ ˄ , ˉ }

| Act P . Here P can only synchronise with T , and in turn
the test T can only perform the success action ˉ , in addition to synchronising with
the process being tested; of course both tester and testee can also perform internal
actions. An example is provided in Fig. 5.3 , where the test a.ˉ 4 ↕

( b c.ˉ ) is applied