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

Fig. 5.1 Operational semantics of pCSP

In order to interpret the full pCSP operationally we need to use pLTSs, the proba-
bilistic generalisation of LTSs (see Sect. 3.2). We mimic the operational interpretation
of CSP as an LTS by associating with pCSP a particular pLTS ₒ

in which sCSP is the set of states and Act ˄ is the set of transition labels. However
there are two major differences:

sCSP , Act ˄ ,

(i) only a subset of terms in pCSP will be used as the set of states in the pLTS
(ii) terms in pCSP will be interpreted as distributions over sCSP , rather than as
elements of sCSP .

We interpret pCSP processes P as distributions [[ P ]] ∈ D ( sCSP ) via the function

[[ − ]] : rpCSP ₒ D ( sCSP ) defined by

= ∈ sCSP , =

[[ s ]] : s for s and [[ P p ↕ Q ]] : [[ P ]] p ↕ [[ Q ]] .

ʱ
−ₒ

The definition of the relations is given in Fig. 5.1 , where a ranges over Act and

ʱ over Act ˄ .
These rules are very similar to the standard ones used to interpret CSP as a
labelled transition system [ 11 ], but are modified so that the result of an action is a
distribution. The rules for external choice and parallel composition use an obvious
notation for distributing an operator over a distribution; for example ʔ

s represents

the distribution, given by

⊧
⊨

ʔ ( s ) f t s

= s

( ʔ s )( t ) =

⊩

0 otherwise.

˄
−ₒ We sometimes write ˄.P for P P , thus giving ˄.P [[ P ]] .