Forewords
Foreword by Tony Hoare
Cambridge, United Kingdom, February 2009
Algebra is the simplest of all branches of mathematics. After the study of numerical calculation and arithmetic, algebra is the first school subject which gives the student an introduction to the generality and power of mathematical abstraction, and a taste of mathematical proof by symbolic reasoning. Only the simplest reasoning principle is required: the substitution of equals for equals.(Even computers are now quite good at it.) Nevertheless, the search for algebraic proof still presents a fascinating puzzle for the human mathematician, and yields results of surprising brevity and pleasing elegance.
A more systematic study of algebra provides a family tree that unifies the study of many of the other branches of mathematics. It identifies the basic mathematical axioms that are common to a whole sub-family of branches. The basic theorems that are proved from these axioms will be true in every branch of mathematics which shares them. At each branching point in the tree, the differences between the branches are succinctly highlighted by their choice between a pair of mutually contradictory axioms. In this way, algebra is both cumulative in its progress along the branches, and modular at its branching points.
It is a surprise to many computer programmers that computer programs, with all their astronomical complexity of structure and behavior, are as amenable to the axioms of algebra as simple numbers were at school. Indeed, algebra scales well from the small to the large. It applies to the large-scale behavior of systems evolving concurrently in parallel; and it underlies the manipulation of the minute detail of the individual instructions of code. At the highest level, algebraic reasoning provides the essential basis for program transformations that match the structure of a complete system to that of the available hardware configuration; and at the lowest level, it provides the justification for optimization instruction set.
This book exploits the power of algebra to explore the properties of concurrent programs, particularly those that control the behavior of distributed systems, communicating with neighbors on identified channels. It starts with the simplest theories at the base of the tree, and gradually extends them in a modular way by additional axioms to deal with sequential programming as well as concurrent, and with communication as well as assignment. In the later chapters, it exploits the modularity of algebra to describe priorities, probabilities, and mobility.
The technical approach of the book is grounded in Computer Science. It emphasizes term models based on the syntax of the operators used in the algebra, and it justifies the axioms by appeal to the execution of the terms as programs. Its crowning achievement is to exploit the unifying power of algebra to cover a range of historic theories, developed for various purposes up to 20 years ago. Earlier these theories were thought to be irreconcilable rivals; but as a result of research by the authors of this book and others, the rivals are now seen to be close family members, each superbly adapted to the particular range of problems that it was designed to tackle.
Foreword by Robin Milner
Cambridge, United Kingdom, February 2009 Nowadays, much of what is still called ‘computing’ involves the behavior of composite systems whose members interact continually with their environment. A better word is ‘informatics’, because we are concerned not just with calculation, but rather with autonomous agents that interact with – or inform – one another. This interactivity bursts the bounds of the sequential calculation that still dominates many programming languages. Does it enjoy a theory as firm and complete as the theory of sequential computation? Not yet, but we are getting there.
What is an informatic process? The answer must involve phenomena foreign to sequential calculation. For example can an informatic system, with many interacting components, achieve deterministic behavior? If it can, that is a special case; non-determinism is the norm, not the exception. Does a probability distribution, perhaps based upon the uncertainty of timing, replace determinism? Again, how exactly do these components interact; do they send each other messages, like email, to be picked up when convenient? – or is each interaction a kind of synchronized handshake?
Over the last few decades many models for interactive behavior have been proposed. This book is the fruit of 25 years of experience with an algebraic approach, in which the constructors by which an informatic system is assembled are characterized by their algebraic properties. The characteristics are temporal, in the same way that sequential processes are temporal; they are also spatial, describing how agents are interconnected. And their marriage is complex.
The authors have teased out primitive elements of this structure. In doing so they have applied strict mathematical criteria. For example, to what extent can the dynamic characteristics of a set of process constructors be reflected, soundly or completely, by a collection of algebraic axioms? And to what extent can the authors’ calculus ACP (Algebra of Communicating Processes) be harmonized with other leading calculi, especially Hoare’s CSP (Communicating Sequential Processes) and Milner’s CCS (Calculus of Communicating
Systems)? Consideration of these questions gives the book a firm and appreciable structure. In particular, it shows up a shortcoming of what (for some 50 years) has been called automata theory: that theory never seriously attempted to model the ways in which two automata might interact.
So it may seem that the book is mainly an account of the frontiers of research into process theory. It is much more, and I hope that syllabus designers will take note: the presentation is lucid and careful, enriched with exercises, to the extent that many parts of it can be used as a basis for university courses, both undergraduate and postgraduate. If in such courses we expose students to theories that are still advancing, then they share the excitement of that progress.
Foreword by Jan Bergstra
Amsterdam, the Netherlands, February 2009 This book about process algebra improves on its predecessor, written by Jos Baeten and PeterWeijland almost 20 years ago, by being more comprehensive and by providing far more mathematical detail. In addition the syntax of ACP has been extended by a constant 1 for termination. This modification not only makes the syntax more expressive, it also facilitates a uniform reconstruction of key aspects of CCS, CSP as well as ACP, within a single framework.
After renaming the empty process (ε) into 1 and the inactive process (δ) into 0, the axiom system ACP is redesigned as BCP. This change is both pragmatically justified and conceptually convincing. By using a different acronym instead of ACP, the latter can still be used as a reference to its original meaning, which is both useful and consistent.
Curiously these notational changes may be considered marginal and significant at the same time. In terms of theorems and proofs, or in terms of case studies, protocol formalizations and the design of verification tools, the specific details of notation make no real difference at all. But by providing a fairly definitive and uncompromising typescript a major impact is obtained on what might be called ‘nonfunctional qualities’ of the notational framework. I have no doubt that these nonfunctional qualities are positive and merit being exploited in full detail as has been done by Baeten and his co-authors. Unavoidably, the notational evolution produces a change of perspective. While, for instance, the empty process is merely an add on feature for ACP, it constitutes a conceptual cornerstone for BCP.
Group theory provides different notational conventions (additive and multiplicative) for the same underlying structure, and in a similar fashion, the format of this book might be viewed as a comprehensive and consistent notational convention for a theory of process algebra. But the same theory might instead be captured, when used in another context, with a different preferred notation.
Process algebra as presented here is equational logic of processes viewed is a family of first order theories. Each theory is provided with its Tarski semantics, making use of many-sorted algebras with total operations and nonempty sorts. Although this may sound already quite technical and may be even prohibitive for a dedicated computer scientist, these are the most stable and clear-cut semantic principles that mathematical logic has developed thus far. When developing axioms for process algebras the authors do not deviate from that path for ad hoc reasons of any kind. Thus there is a very clear separation between the logical metatheory, consisting of first order equational logic and its model-theory on the one hand and the many design decisions concerning the subject matter that is process theory on the other hand. A prominent methodological principle underlying the work is that the significant ramification of design decisions concerning various process formalisms can be made systematic in a way comparable to the development of say ring theory in mathematics.
In addition to making use of first order logic, the equational form of most axioms allows a systematic exploitation of technical results from term rewriting. This is not a matter of process theory per se but it is proving helpful throughout the book.
One may ask why process algebra should be considered a topic in computer science and not just in applied mathematics. While some parts of process theory are now moving in the direction of systems biology, the process algebras covered in this book may sooner or later show up in physics. Quantum process algebras have not been covered here but various forms already exist and that kind of development is likely to continue for many more years.
Just like its predecessor has been for many years, this book will definitely be useful as a reference work for research in process theory.