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

We capture the conjunction of two formulae by a probabilistic choice between the
corresponding tests; in order to prevent the results from these tests getting mixed up,
we employ the vector-based tests of [ 2 ], so that we can use different success actions
in the separate probabilistic branches. Therefore, we complete our proof by recalling
Theorem 4.7 that the scalar testing preorders imply the vector-based ones.
It is well-known that may and must testing for standard CSP can be captured
equationally [ 3 , 4 , 10 ]. In Sect. 5.3 we show that most of the standard equations are
no longer valid in the probabilistic setting of pCSP . However, we show in Sect. 5.9
that both P

pmust Q can still be captured equationally over full pCSP .
In the may case the essential (in)equation required is

pmay Q and P

a. ( P p ↕ Q ) a.P p ↕ a.Q.

The must case is more involved: in the absence of the distributivity of the external and
internal choices over each other, to obtain completeness we require a complicated
inequational schema.

5.2 The Language pCSP

We first define the language and its operational semantics. Then we show how the
general probabilistic testing theory outlined in Sect. 4.1 can be applied to processes
from this language.

5.2.1 The Syntax

Let Act be a set of visible (or external ) actions, ranged over by a , b , c , ... , which
processes can perform. Then the finite probabilistic CSP processes are given by the
following two sorted syntax:

P :: = S | P p ↕ P

S :: = 0 | a.P | P P | S S | S | A S

We write pCSP , ranged over by P , Q , for the set of process terms defined by
this grammar, and sCSP , ranged over by s , t , for the subset comprising only the
state-based process terms (the subsort S above).
The process P p ↕ Q , for 0 1, represents a probabilistic choice between P

and Q : with probability p it will act like P and with probability 1

≤ p ≤

p it will act
like Q . Any process is a probabilistic combination of state-based processes built by
repeated application of the operator p ↕ . The state-based processes have a CSP-like
syntax, involving the stopped process 0 , action prefixing a. __ for a

−

∈ Act , internal -

and external choices and , and a parallel composition | A for A ↆ Act .