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

The process P Q will first do a so-called internal action ˄ ∈ Act , choosing

nondeterministically between P and Q . Therefore , like a. __ , acts as a guard ,in

the sense that it converts any process arguments into a state-based process.
The process s

t on the other hand does not perform actions itself but rather
allows its arguments to proceed, disabling one argument as soon as the other has
done a visible action. In order for this process to start from a state rather than a
probability distribution of states, we require its arguments to be state-based as well;
the same requirement applies to

| A .

Act , represents processes s and t running
in parallel. They may synchronise by performing the same action from A simultane-
ously; such a synchronisation results in ˄ . In addition s and t may independently do
any action from ( Act ˄ \

Finally, the expression s | A t , where A ↆ

A ), where Act ˄ : = Act ∪{ ˄ } .

| A can only be applied to state-based
processes, informally we use expressions of the form P

Although, formally the operators and

| A Q , where
P and Q are not state-based, as syntactic sugar for expressions in the above syntax
obtained by distributing

Q and P

and | A over p ↕ . Thus, for example s ( t 1 p ↕ t 2 ) abbreviates

the term ( s t 2 ).

The full language of CSP [ 1 , 10 , 11 ] has many more operators; we have simply
chosen a representative selection, and have added probabilistic choice. Our parallel
operator is not a CSP primitive, but it can easily be expressed in terms of them—in
particular P

t 1 ) p ↕ ( s

A are the parallel composition and
hiding operators of [ 11 ]. It can also be expressed in terms of the parallel composition,
renaming and restriction operators of CCS. We have chosen this (nonassociative)
operator for convenience in defining the application of tests to processes.
As usual we may elide 0 ; the prefixing operator a. __ binds stronger than any
binary operator; and precedence between binary operators is indicated via brackets
or spacing. We will also sometimes use indexed binary operators, such as i ∈ I p i ·

| A Q = ( P A Q ) \ A , where A and \

P i

with i ∈ I p i = 1 and all p i > 0, and i ∈ I P i , for some finite index set I .

5.2.2 The Operational Semantics

The above intuitive reading of the various operators can be formalised by an op-
erational semantics that associates with each process term a graph-like structure
representing the manner in which it may react to users' requests. Let us briefly recall
this procedure for nonprobabilistic CSP.
The operational semantics of CSP is obtained by endowing the set of terms with
the structure of an LTS. Specifically

(i) the set of states S is taken to be all terms from the language CSP
(ii) the action relations P

ʱ
−ₒ

Q are defined inductively on the syntax of terms.

A precise definition may be found in [ 11 ].