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

This equational theory allows us to reduce terms to a form in which the external
choice operator is applied to prefix terms only.

Definition 5.8 (Normal Forms) The set of normal forms N is given by the following
grammar:

i ∈ I a i .N i .

N :: = N 1 p ↕ N 2 | N 1 N 2 |

Proposition 5.7 For every P ∈ nCSP , there is a normal form N such that P = E N .

Proof

We can also show that the axioms ( P1 )-( P3 ) and ( D1 ) are in some sense all that are
required to reason about probabilistic choice. Let P

A fairly straightforward induction, heavily relying on ( D1 )-( D3 ).

= prob Q denote that equivalence
of P and Q can be derived using those axioms alone. Then we have the following
property.

Lemma 5.14 Let P , Q ∈ nCSP . Then [[ P ]] = [[ Q ]] implies P = prob Q.

Here [[ P ]] [[ Q ]] says that [[ P ]] a n d [[ Q ]] are the very same distributions of state-

based processes in sCSP ; this is a much stronger prerequisite than P and Q being
testing equivalent.

=

Proof The axioms ( P1 )-( P3 ) and ( D1 ) essentially allow any processes to be written

in the unique form i ∈ I p i s i , where the s i ∈

sCSP are all different.

5.9 Inequational Theories

In order to characterise the simulation preorders, and the associated testing preorders,
we introduce inequations . We write P

E may Q when P

Q is derivable from the
inequational theory obtained by adding the four may inequations in the middle part
to the upper part of Fig. 5.8 . The first three additions, ( May0 )-( May2 ), are used in
the standard testing theory of CSP [ 1 , 3 , 4 ]. For the must case, we write P E must Q
when P Q is derivable from the equations and inequations in the upper and
lower parts of Fig. 5.8 . In addition to the standard inequation ( Must1 ), we require an
inequational schema, ( Must2 ); this uses the notation inits(P) to denote the (finite)
set of initial actions of P . Formally,

inits (0) =∅

inits ( a.P ) ={ a }

= ∪

inits ( P p ↕ Q ) inits ( P ) inits ( Q )

inits ( P Q ) = inits ( P ) ∪ inits ( Q )

inits ( P Q ) ={ ˄ } .