Biomedical Engineering Reference
In-Depth Information
Tabl e 1
The -calculus
Process and channels
P;Q;:::
Process names
x
,
y
;:::
Channel names
x, y;:::
Channel co-names
Events
WWD
x
.y/
Receive y along x
WWD
x
i
y
h
Send y along x
Process syntax
P
WWD
P
1
j
P
2
Parallel processes
:P
1
Sequential prefixing by communication
1
:P
1
C
2
:P
2
Mutually exclusive communication
. x/P
Restricted communication scope
0
Inert process
Structural congruence
P
j
Q
Q
j
P
Commutativity of PAR
.P
j
Q/
j
R
P
j
.Q
j
R/
Associativity of PAR
P
C
Q
Q
C
P
Commutativity of summation
.P
C
Q/
C
R
P
C
.Q
C
R/
Associativity of summation
. x/0
D
0
Scope of inert process
. x/. y/P
. y/. x/P
Multiple communication scopes
.. x/P
j
Q//
. x/.P
j
Q/ if x
…
fn.Q/
Scope extrusion
A. y/
f
y=x
g
Q
A
Recursive parametric definition
x.y/:P
D
x.
z
/:.
f
z
=y
g
P/ if
z
…
fn.P/
Renaming of input channel y
. y/P
D
.
z
/:.
f
z
=y
g
P/ if
z
…
fn.P/
Renaming of restricted channel y
Reaction rules
.
C
x
i
x
h
:Q/
j
.
C
x.y/:P/
!
Q
j
P
f
x=y
g
Communication (COMM)
!
P
0
then P
j
Q
!
P
0
j
Q
if P
Reaction under parallel composition
!
P
0
then . x/P
!
. x/P
0
if P
Reaction within restricted scope
!
P
0
and P
0
Q
0
then Q
!
Q
0
if Q
P ,P
Reaction up to structural congruence
by communication. The processes are constructed using channel names according
to the syntax, show in Table
1
, in which the channel are indicated with their names
x;y;::: and the process with the capital letters P;Q;:::. The simplest process is
the empty process 0. The communication between to process consists of two types
of atomic actions, denoted as and cal
le
d
prefix
:the
input
x.y/ to receive a name
for y along the channel x and the
output
x
h
z
i
to send the name
z
along the channel x.
A process P may be prefixed with an input or output action : P will occur
only after the action is performed. Processes may also be combined to create
more complex ones. The
mutual exclusive choice operator
C
allows summation
of processes and denotes a complex process able to perform exactly one of several
alternative actions. The choice between the actions is non-deterministic and depends
on the actual communication that will occur. In fact, since several alternative
