Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 150

Fig. 6.2 Operational semantics of rpCSP

6.2 The Language rpCSP

Let Act be a set of visible actions that a process can perform, and let Var be an infinite
set of variables. The language rpCSP of probabilistic CSP processes is given by the
following two-sorted syntax, in which p ∈ [0, 1], a ∈ Act and A ↆ Act :

P :: = S | P p ↕ P

S :: = 0 | x ∈ Var | a.P | P P | S S | S | A S | rec x.P

This is essentially the finite language pCSP given in Sect. 5.2 plus the recursive
construct rec x.P in which x is a variable and P a term. The notions of free and
bound variables are standard; by Q [ x

ₒ

P ] we indicate substitution of term P for
variable x in Q , with renaming if necessary. We write rpCSP for the set of closed
P -terms defined by this grammar, and still use sCSP for its state-based subset of
closed S -terms.
The operational semantics of rpCSP is defined in terms of a particular pLTS

, in which sCSP is the set of states and Act ˄ is the set of transition
labels. We interpret rpCSP processes P as distributions [[ P ]]

sCSP , Act ˄ , ₒ

∈ D ( sCSP ), as we

did for pCSP processes in Sect. 5.2.2.
The transition relation is defined in Fig. 6.2 , where A ranges over subsets of Act ,

and actions a , ʱ are elements of Act , Act ˄ respectively. This is a slight extension of
the rules in Fig. 5.1 for finite processes; one new rule is required to interpret recursive
processes. The process rec xP performs an internal action when unfolding. As our
testing semantics will abstract from internal actions, these ˄ -steps are harmless and
merely simplify the semantics.
We graphically depict the operational semantics of a rpCSP expression P by
drawing the part of the pLTS reachable from [[ P ]] as a directed graph with states

ₒ