CHAPTER 9
PROCESS ALGEBRA
A computer process is a program or section of a program (such as a function) in
execution. It may be in one of the following states: ready, running, waiting, or termi-
nated. A process algebra is a concise language for describing the possible execution
steps of computer processes. It has a set of operators and syntactic rules for spec-
ifying a process using simple, atomic components. It is usually not a logic-based
language.
Central to process algebras is the notion of equivalence, which is used to show
that two processes have the same behavior. Well-established process algebras such
as Hoare’s Communicating Sequential Processes (CSP) [Hoare, 1978; Hoare, 1985],
Milner’s Calculus of Communicating Systems (CCS) [Milner, 1980; Milner, 1989],
and Bergstra and Klop’s Algebra of Communicating Processes (ACP) [Bergstra and
Klop, 1985] have been used to specify and analyze concurrent processes with in-
terprocess communication. These are untimed algebras since they allow one to only
reason about the relative ordering of the execution steps and events.
To use a process algebra or a process-algebraic approach to specify and analyze a
system, we write the requirements specification of the system as an abstract process
and the design specification as a detailed process. We then show that these two pro-
cesses are equivalent, thus showing the design specification is correct with respect to
the requirements specification. Here, the requirements specification may include the
desired safety properties.
9.1 UNTIMED PROCESS ALGEBRAS
A process algebra has four basic components: (1) a concise language to specify a
system as a process or set of processes, (2) an unambiguous semantics to provide
237
Real-Time Systems: Scheduling, Analysis, and Verification. Albert M. K. Cheng
Copyright
¶
2002 John Wiley & Sons, Inc.
ISBN: 0-471-18406-3

Since an observation congruence class is considered a behavior, CCS is thus an
algebra of behaviors in which each program stands for its congruence class. The
syntax of CCS consists of (1) value expressions; (2) labels, sorts, and relabeling;
(3) behavior identifiers; and (4) behavior expressions.
Value Expressions: Value expressions are constructed from simple variables, con-
stant symbols, and function symbols signifying known total functions over values.
Labels are  =  ∪
,andτ .Asort L is a subset of  and a sort L(B) is assigned
to each behavior expression B. Given that P and Q are sorts, S : P → Q is a re-
labeling from P to Q if (1) it is a bijection and (2) it respects complements; that is,
S(a) = S(a) for a, a ∈ L.
MILNER’S CALCULUS OF COMMUNICATING SYSTEMS
239
Each behavior identifier has a preassigned arity n(b) which indicates the number
of value parameters, and a sort L(b).
Behavior Expressions: Behavior expressions are constructed with six types of be-
havior operators, by parameterizing behavior identifiers and by conditionals. The
behavior operators are: inaction, summation, action, composition, restriction, and
relabeling.
The inaction operator NIL (null) produces no atomic actions. The summation
operator “+”inA + B adds the atomic actions of A and B, yielding a sum of A
and B’s actions. The action operator “.” is used to express axioms. The composition
operator “|”inA | B signifies that an action of A or B in the composition produces an
action of the composite in which the other component is unaffected. The restriction
operator “\”inA\b indicates that B is restricted so that there are no b or
b actions.
An identifier can be parameterized as in b( E
1
,...,E
n(b)

1
|T
2
.
More precisely, one choice is for the system’s two processes to stay in the non-critical
sections. The second choice is for process 1 to request to enter its critical section
while process 2 remains in the non-critical section. The third choice is for process
2 to request to enter its critical section while process 1 remains in the non-critical
section.
The following CCS statement specifies that action Q has a choice of executing the
critical section of process 1 or executing the critical section of process 2. Also, while
executing C
1
, C
2
is not allowed. Similarly, while executing C
2
, C
1
is not allowed.
Q
def
= C
1
\{C
2
}+C
2
\{C
1

Rel ∼ A[I ]= A, I : L → L is the identity mapping
A[S]=A[S

]
A[S][S

]=A[S

oS]
A[S]\β = A\α[S],β = name(S(α))
(A|B)[S]=A[S]|B[S]
Conditional if true then A else B = A
if false then A else B = B
Unobservable action τ g.τ.A = g.A
A + τ.A = τ.A
g.(A + τ.B) + g.B = g.(A + τ.B)
A + τ.(A + B) = τ.(A + B)
Observation equivalence A ≈ τ.A
¬(P ∧ Q) = (¬P ∨¬Q)
Figure 9.1 CCS laws.
Direct Equivalence: Two behavior programs are directly equivalent iff for every
input, both programs produce the same behavior, that is, same results.
Given a specification written in CCS, we can use equational laws to rewrite it in
a form we desire. To show that two specifications are equivalent, we can use these
laws to rewrite them to establish equivalence. We summarize selected CCS laws for
easy reference in Figure 9.1.
9.2.2 Congruence of Behavior Programs
The results of the actions of directly equivalent programs must be identical. To gen-
eralize the direct equivalence relation, a congruence relation that requires only the
TIMED PROCESS ALGEBRAS


, P
a
→P

and (P

, Q

) ∈ r .
This basically means that if P (or Q) can execute one step on event a, then Q (or P)
should be able to execute one step on event a such that both of the next states are
also bisimilar.
Weak Bisimulation: A binary relation r is a weak bisimulation for a given transi-
tion “→” if, for (P, Q) ∈ r and for any action or event a ∈ D,
1. if P
a
→P

, then ∃Q

, Q
ˆa
⇒ Q

and (P

, Q

) ∈ r ,and

the assumption that a single processor exists so that all process executions are inter-
leaved. Between these two extreme assumptions are real-time process algebras that
242
PROCESS ALGEBRA
assume a limited number of resources. One popular timed process algebra that as-
sumes a limited number of n resources capable of executing n actions is the ACSR
[Lee, Bremond-Gregoire, and Gerber, 1994].
9.4 ALGEBRA OF COMMUNICATING SHARED RESOURCES
The ACSR language is a discrete real-time process algebra based on CCS (described
earlier) that provides several operators to handle timing properties. These operators
can be used to bound the execution time of a sequence of actions, to delay the se-
quence’s execution by a number of time units, and to timeout while waiting for spe-
cific actions to occur. The exception operator can be inserted into any place within
a process and allows an exception to be raised, immediately handled by an external
exception-handling process, just like in an exception-handling mechanism of a real
computer process. The interrupt operator allows the specification of responses or re-
actions to asynchronous actions or events. The ACSR computation model views a
real-time system as a collection of communicating processes competing for shared
resources. Every execution step is either an action or an event.
Action: An action is set of consumptions of resources {r
1
,...,r
n
} at corresponding
non-negative priority levels p
1
,..., p
n
for one time unit. A resource consumption is
denoted by a pair (r

of zero or more events may appear between any two consecutive actions.
ALGEBRA OF COMMUNICATING SHARED RESOURCES
243
9.4.1 Syntax of ACSR
We next describe in detail the syntax and semantics of the different types of ACSR
processes. NIL is a process that performs no action and is always deadlocked. This
is the same as CCS’s inaction operator NIL, which produces no atomic actions. The
action prefix operator “:” in A : P indicates that the resource-consuming action A
executes at the first time unit, and then process P runs. The event prefix operator “.”
in (a, n).P indicates that the event (a, n) executes (occurs) instantly with no time
passage, and then process P runs. In CCS, “.” is the action operator used to express
axioms.
The choice operator “+” in P + Q is basically an “or,” signifying a choice is
available between processes P and Q. The effect is that this composed process may
behave like either P or Q.InCCS,“+” is the summation operator, so A + B adds
the atomic actions of A and B, yielding a sum of A and B’s actions. The parallel
operator “”inP  Q indicates that processes P and Q can execute in parallel. This
is similar to CCS’s composition operator “|”.
The close operator “[ ]” in [P]
I
creates a process that only uses resources in the
set I . The restriction operator “\”inP \F indicates that while process P is executing,
events with labels in F cannot execute. This is similar to CCS’s restriction operator
“\”asinA\b, which indicates that B is restricted so that there are no b or
b actions.
The hiding operator “\\”inP\\H hides the identity of the resources in the set H
from process P. The notation rec X .P signifies process P is recursive so that the
described behavior of P is infinite.
The following operator allows ACSR to specify absolute timing properties. The
notation P

is a labeled directed graph G = (V , E). V is a set of states of a process. E is a
244
PROCESS ALGEBRA
set of edges, each of which denotes an execution step or action e
i
such that an edge
(P
i
, P
j
) connects state P
i
to state P
j
iff there is a step e
i
that is enabled at state P
i
,
and executing e
i
will modify the state of the process to have the same values as the
tuple at state P
j
. An invocation of a process can be thought of as tracing a path in
the labeled transition system.
The states are described by a concrete syntax (a process) in process algebra. We
use a finite set of transition rules to infer the execution steps of the behavior of a
process. Two transition systems are available for defining the semantics of ACSR:
unconstrained and prioritized.

1, j
+{(cpu1, 1)}:C
1, j+1
+{(cpu2, 1)}:
C
1, j+1
, 0 ≤ j < c
1
. The last branch {(cpu2, 1)}:C
1, j+1
, 0 ≤ j < c
1
means that
this process can use the resource cpu2 at priority level 1 for one time unit and go to
process C
1, j+1
.
Axiom
The following axiom is for event prefix:
ActI
−
A : (a, n).P
(a,n)
−→ P
Example. The process T
1
def
= (s
1
, 1).C