Wan Fokkink
Introduction to Process Algebra
Computer Science { Monograph (English)
2nd edition
April 10, 2007
Springer-Verlag
Berlin Heidelberg NewYork
London Paris Tokyo
Hong Kong Barcelona
Budapest
Preface
Computer software and network protocols are increasingly important in daily
life. At the same time the complexity of software has rocketed, so that its
correctness is at stake. New methodologies and disciplines are being devel-
oped to bring structure to the ever growing jungle of computer technology.
(Semi-)automated manipulation has become an important means in discover-
ing aws in software and hardware systems. Process algebra is a mathematical
framework in which system behaviour is expressed in the form of algebraic
terms, enhancing the available techniques for manipulation.
Concurrency is omnipresent in system behaviour, and in a large part
responsible for its complexity: even simple behaviours become wildly compli-
cated when they are executed in parallel. In order to study such systems in
detail, it is imperative that they are dissected into their concurrent compo-
nents. Fundamental to process algebra is a parallel operator, to break down
systems into their concurrent components. A set of equations is imposed
to derive whether two terms are behaviourally equivalent. In this framework,
non-trivial properties of systems can be established in an elegant fashion. For
example, it may be possible to equate an implementation to the speciflcation
of its required input/output relation. In recent years a variety of automated
tools have been developed to facilitate the derivation of such properties.
Applications of process algebra exist in diverse flelds such as safety criti-
cal systems, network protocols, and biology. In the educational vein, process
algebra has been recognised to teach skills to deal with complex concurrent
systems, by representing and reasoning about such systems in a mathemati-
cally clear and precise manner.
This text developed from an undergraduate course on process algebra at
the computer science department of the University of Wales Swansea during
the autumn of 1997 and of 1998. Chapters 2-7 contain su–cient material
for more than twenty hours of lecturing; a set of slides and further mate-
rial to support such a course are available from my homepage (currently
at http://www.cwi.nl/»wan). It is recommended to use a tool set based on
process algebra, such as the „CRL tool set, the Concurrency Workbench Ed-
inburgh, or the Labelled Transition System Analyser to enliven the course.
„CRL speciflcations of the protocols in Chapter 6 can be obtained from the
VI
Preface
author. Appendices A and B provide useful background information; they
are not intended to be included in the course.
I am grateful to John Tucker for his encouragement to further develop a
raw set of lecture notes, and to Judi Romijn for her support. Over the years
I have beneflted from discussions with Jan Bergstra, Rob van Glabbeek, Jan
Friso Groote, Frits Vaandrager, Alban Ponse, Chris Verhoef, Jaco van de
Pol, Jos Baeten, Luca Aceto, Jos van Wamel, Steven Klusener, Bas Luttik,
Dennis Dams, and many others.
Amsterdam, November 1999
Wan Fokkink
Contents
1.
Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :
1
7
2. Basic Process Algebra : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :
7
2.1 Basic Process Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
8
2.2 Transition Rules for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Bisimulation Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.4 Axioms for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3. Algebra of Communicating Processes : : : : : : : : : : : : : : : : : : : : : 19
3.1 Parallelism and Communication . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.2 Left Merge and Communication Merge . . . . . . . . . . . . . . . . . . . . 21
3.3 Axioms for PAP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.4 Deadlock and Encapsulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4. Recursion : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 33
4.1 Guarded Recursive Speciflcations . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2 Transition Rules for Guarded Recursion . . . . . . . . . . . . . . . . . . . 35
4.3 Recursive Deflnition and Speciflcation Principles . . . . . . . . . . . 38
4.4 Completeness for Regular Processes . . . . . . . . . . . . . . . . . . . . . . . 41
4.5 Approximation Induction Principle . . . . . . . . . . . . . . . . . . . . . . . 44
5. Abstraction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 49
5.1 Rooted Branching Bisimulation Equivalence . . . . . . . . . . . . . . . 49
5.2 Guarded Linear Recursion Revisited . . . . . . . . . . . . . . . . . . . . . . 53
5.3 Axioms for the Silent Step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
5.4 Abstraction Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.5 An Example with Bufiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.6 Cluster Fair Abstraction Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6. Protocol Veriflcations : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 71
6.1 Alternating Bit Protocol
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.2 Bounded Retransmission Protocol . . . . . . . . . . . . . . . . . . . . . . . . 80
6.3 Veriflcation Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
6.4 Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
VIII
Contents
7. Extensions : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 97
7.1 Renaming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.2 State Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
7.3 Priorities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.4 Further Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
A. Equational Logic : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 113
A.1 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
A.2 Axiomatisations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
A.3 Initial Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
A.4 Term Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
B. Structural Operational Semantics : : : : : : : : : : : : : : : : : : : : : : : : : 123
B.1 Transition System Speciflcations . . . . . . . . . . . . . . . . . . . . . . . . . . 123
B.2 The Meaning of Negative Premises . . . . . . . . . . . . . . . . . . . . . . . 125
B.3 Bisimulation as a Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
B.4 Branching Bisimulation as a Congruence . . . . . . . . . . . . . . . . . . 132
B.5 Conservative Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
B.6 Modal Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
Solutions to Selected Exercises : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 141
References : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 155
Index : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 167
1. Introduction
System behaviour generally consists of processes and data. Processes are
the control mechanisms for the manipulation of data. While processes are
dynamic and active, data are static and passive. System behaviour tends
to be composed of several processes that are executed concurrently, where
these processes exchange data in order to inuence each other’s behaviour.
The picture below presents a typical architecture for a concurrent system.
Each process Pi sends messages to its neighbouring processes Pi¡1 and Pi+1,
giving them information on the state of Pi. The neighbouring processes use
this information in their internal computations, to update their own states.
¢¢¢
P¡1
P0
P1
P2
¢¢¢
Some examples of concurrent systems are:
† A colony of ants;
Ants behave as separate entities, which inuence each other’s behaviour. As
soon as one ant discovers a goody such as a lump of sugar, it radiates a smell
to attract other ants. Tofts [192] was able to explain certain phenomena of
colonies of ants by modelling such colonies as concurrent systems in process
algebra.
† A network protocol, being a high-level description of a data communication
procedure.
As an example we consider the so-called alternating bit protocol [31]. A
Sender and a Receiver are the separate processes, which in concurrency
make up the system;
2
1. Introduction
Sender
Receiver
Data elements d1; d2; d3; : : : are sent from the Sender to the Receiver via
a faulty channel, so that data may be corrupted. In the alternating bit
protocol, the Sender attaches a bit 0 to data elements d2k¡1 and a bit 1
to data elements d2k for positive natural numbers k. As soon as the Re-
ceiver receives a datum, it sends the attached bit to the Sender via a faulty
channel, to acknowledge reception. If the Receiver receives a corrupted
message, then it resends the previous acknowledgement. The Sender keeps
on sending out the pair (di; b) until it receives the acknowledgement b.
Then it starts sending out the next pair (di+1; 1 ¡ b) until it receives the
acknowledgement 1 ¡ b, et cetera. Alternation of the attached bit enables
the Receiver to determine whether a received datum is really new, and al-
ternation of the acknowledgement enables the Sender to determine whether
a datum reached the Receiver unscathed.
† A pocket calculator;
5765
+ ¡
8
9
5
2
6
3
⁄
0
=
C
7
4
1
The buttons represent the separate actions of this system, which all inu-
ence the state (i.e., the intermediate result of a computation) of the pocket
calculator in a difierent way. The pocket calculator in combination with a
user make up a concurrent system.
In this text, system behaviour is represented as a labelled transition sys-
tem, which basically consists a set of nodes together with a set of labelled
edges between these nodes. For example, a fraction of the full labelled tran-
sition system of the pocket calculator is depicted in Fig. 1.1. Each node in
this labelled transition system represents a difierent state of the calculator,
and an edge from one node to the other expresses that the calculator can
change from one state to the other, by pushing a button; the label of an edge
represents the button that has to be pushed in order to realise this state
transition.
In general it is much easier to study a concurrent system such as the
pocket calculator by breaking it up into its concurrent components. Although
its full labelled transition system is enormous, the process behaviour of the
1. Introduction
3
=
0
+
7
C
7..
0 +..
¡
0 ¡..
1
0 ¡ 1..
=
8
0 + 8..
3
0 + 83..
=
83
¡1
⁄
7 ⁄..
4
7 ⁄ 4..
=
28
Fig. 1.1. Labelled transition system of a pocket calculator
pocket calculator is not so di–cult. It can be captured by specifying the
behaviour of the separate buttons, and putting them in parallel. For example,
the behaviour of the +-button is displayed in Fig. 1.2, where d1; : : : ; dk are
digits and m = n + d1 ¢¢¢ dk. Execution is started in the state that is pictured
at the top, where the computation has the intermediate value n. Similarly,
the arithmetic operations subtraction and multiplication can be specifled on
the data domain of numbers. An extra error element needs to be added to
the data domain, to represent that the result of an arithmetic computation
exceeds the screen size, or that an operation is undeflned (such as division
by zero).
n
+
n + ::
d1
...
dk
+
m + ::
C
0
m
n + d1:::dk::
=
¡
m ¡ ::
⁄
m ⁄ ::
Fig. 1.2. Behaviour of the plus button
A process graph is a labelled transition system in which one state is se-
lected to be the root state, i.e., the initial state of the process. If the labelled