Introduction

The process theories introduced so far describe the main features of imperative concurrent programming without the explicit mention of time. Implicitly, time is present in the interpretation of many of the operators introduced before. In the process a.x, the action a must be executed before the execution of process x. The process theories introduced so far allow for the description of the ordering of actions relative to each other. This way of describing the execution of actions through time is called qualitative time. Many systems though rely on time in a more quantitative way.

Consider for example the following caller process. A caller takes a phone off the hook. If she hears a certain tone, she dials some number. It does not matter which one. If she does not hear the tone, she puts the phone back on the hook. After dialing the number, the caller waits some time for the other side to pick up the phone. After some conversation, the caller puts the phone back on the hook. In case the call is not answered within some given time, the caller gives up and also puts the phone back on the hook.

To be able to describe such systems in process theory in the same framework as untimed systems, many process theories have been extended with a quantitative notion of timing. In extending the untimed process theories with timing a number of fundamental choices have to be made with respect to the nature of the time domain, the way time appears syntactically in the equational theory, and the way time is incorporated semantically.

What is this book about?

This book sets the standard for process algebra. It assembles the relevant results of most process algebras currently in use, and presents them in a unified framework and notation. It addresses important extensions of the basic theories, like timing, data parameters, probabilities, priorities, and mobility. It systematically presents a hierarchy of algebras that are increasingly expressive, proving the major properties each time.

For researchers and graduate students in computer science, the book will serve as a reference, offering a complete overview of what is known to date, and referring to further literature where appropriate.

Someone familiar with CCS, the Calculus of Communicating Systems, will recognize the minimal process theory MPT as basic CCS, to which a constant expressing successful termination is added, enabling sequential composition as a basic operator, and will then find a more general parallel-composition operator. Someone familiar with ACP, the Algebra of Communicating Processes, will see that termination is made explicit, leading to a replacement of action constants by action prefixing, but will recognize many other things. The approaches to recursion of CCS and ACP are both explained and integrated. Someone familiar with CSP, Communicating Sequential Processes, will have to cope with more changes, but will see the familiar operators of internal and external choice and parallel composition explained in the present setting.

Interleaving

So far, the focus has been on sequential processes: actions can be executed, or alternatives can be explored, starting from a single point of control. In this chapter, the step is taken towards the treatment of parallel or distributed systems: it is allowed that activities exist in parallel. Just allowing separate activity of different components is not enough. A genuine treatment of parallel activity requires in addition a description of interaction between parallel activities.

Suppose there are two sequential processes x and y that can execute actions, and choose alternatives, independently. The merge operator ‖ denotes parallel composition. Thus, the parallel composition of x and y is denoted x ‖ y. To illustrate the intuition behind the algebraic treatment of parallel composition, consider an external observer O that observes process x ‖ y. Observations can be made of executions of actions. Assume that these observations are instantaneous. Then, it can be seen that the observations of actions of x and actions of y will be merged or interleaved in time.

Consider the example a.0 ‖ b.0. This process involves the execution of two actions, one from each component. Observer O might see the execution of a first, and then the execution of b. After this, no further activity is possible. On the other hand, observer O might see the execution of b first, then the execution of a followed by inaction. Finally, the observer might observe the two actions simultaneously.

Transition-system spaces

This chapter introduces the semantic domain that is used throughout this book. The goal is to model reactive systems; the most important feature of such systems is the interaction between a system and its environment. To describe such systems, the well-known domain of transition systems, process graphs, or automata is chosen. In fact, it is the domain of non-deterministic (finite) automata known from formal language theory. An automaton models a system in terms of its states and the transitions that lead from one state to another state; transitions are labeled with the actions causing the state change. An automaton is said to describe the operational behavior of a system. An important observation is that, since the subject of study is interacting systems, not just the language generated by an automaton is important, but also the states traversed during a run or execution of the automaton. The term ‘transition system’ is the term most often used in reactive-systems modeling. Thus, also this book uses that term.

The semantic domain serves as the basis for the remainder of the book. The meaning of the various equational theories for reasoning about reactive systems developed in the remaining chapters is defined in terms of the semantic domain, in the way explained in the previous chapter. Technically, it turns out to be useful to embed all transition systems that are of interest in one large set of states and transitions, from which the individual transition systems can be extracted.

Introduction

This second chapter introduces the basic concepts and notations related to equational theories, algebras, and term rewriting systems that are needed for the remainder of the book. Throughout the book, standard mathematical notations are used, in particular from set theory. Notation N = {0, 1, 2, …} denotes the natural numbers.

Equational theories

A central notion of this book is the notion of an equational theory. An equational theory is a signature (defining a ‘language’) together with a set of equations over this signature (the basic laws). Every process algebra in this book is presented as a model of an equational theory, as outlined in the previous chapter.

Definition 2.2.1 (Signature) A signature Σ is a set of constant and function symbols with their arities.

The objects in a signature are called constant and function symbols. The reason for doing so is to distinguish between these purely formal objects and the ‘real’ constants and functions they are meant to represent. In Section 2.3, where interpretations of equational theories are discussed, this point is elaborated further. Note that a constant symbol can also be seen as a function symbol of arity zero.

Example 2.2.2 (Signature) As an example, consider the signature Σ1 consisting of the constant symbol 0, the unary function symbol s, and the binary function symbols a and m.

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.

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.

Definition

This book is about process algebra. The term ‘process algebra’ refers to a loosely defined field of study, but it also has a more precise, technical meaning. The latter is considered first, as a basis to delineate the field of process algebra.

Consider the word ‘process’. It refers to behavior of a system. A system is anything showing behavior, in particular the execution of a software system, the actions of a machine, or even the actions of a human being. Behavior is the total of events or actions that a system can perform, the order in which they can be executed and maybe other aspects of this execution such as timing or probabilities. Always, the focus is on certain aspects of behavior, disregarding other aspects, so an abstraction or idealization of the ‘real’ behavior is considered. Rather, it can be said that there is an observation of behavior, and an action is the chosen unit of observation. Usually, the actions are thought to be discrete: occurrence is at some moment in time, and different actions can be distinguished in time. This is why a process is sometimes also called a discrete event system.

The term ‘algebra’ refers to the fact that the approach taken to reason about behavior is algebraic and axiomatic. That is, operations on processes are defined, and their equational laws are investigated. In other words, methods and techniques of universal algebra are used (see e.g., (MacLane & Birkhoff, 1967)). To allow for a comparison, consider the definition of a group in universal algebra.

Introduction

Chapter 3 has introduced the notion of transition systems both as an abstract operational model of reactive systems and as a means to give operational semantics to equational theories. The latter has been illustrated by giving an operational interpretation of the equational theory of natural numbers. The aim of this book, however, is to develop equational theories for reasoning about reactive systems. This chapter provides the first simple examples of such theories. Not surprisingly, the semantics of these theories is defined in terms of the operational framework of the previous chapter. For clarity, equational theories tailored towards reasoning about reactive systems are referred to as process theories. The objects being described by a process theory are referred to as processes. The next two sections introduce a minimal process theory with its semantics. This minimal theory is mainly illustrative from a conceptual point of view. Sections 4.4 and 4.5 provide some elementary extensions of the minimal theory, to illustrate the issues involved in extending process theories. Incremental development of process theories is crucial in tailoring a process theory to the specifics of a given design or analysis problem. The resulting framework is flexible and it allows designers to include precisely those aspects in a process theory that are relevant and useful for the problem at hand. Incremental design also simplifies many of the proofs needed for the development of a rich process theory.

Introduction

In the previous chapters, data types have been handled in an informal way. An alternative composition parameterized by a finite data type D, written as ΣdΣDt with t some process term possibly containing d, was introduced as an abbreviation of a finite expression, and the d occurring in term t was not treated as a (bound) variable. This chapter takes a closer look at data expressions. Such expressions are considered in a more formal way, and the interplay between data and processes is studied. All issues involved can be illustrated by considering just two concrete data types, namely the (finite) data type of the Booleans and the (infinite) data type of the natural numbers. The data type of the natural numbers was also used in the previous chapter to denote time behavior. Considering an uncountable data type as the reals causes additional problems that are avoided in the present text. The use of an uncountable data type in a parameterized alternative composition would, just like the use of an uncountable time domain, provide a means to specify uncountable processes, which is not possible with any of the theories developed in this book.

Notation 10.1.1 (Booleans, propositional logic) Recall from Example 2.3.2 the algebra of the Booleans B = (B, ^, ¬, true). In addition to the constant true and the operators ^ and ¬, the binary operators ∨ (or) and ⊃ (implication), and the constant false are also used in the remainder. The not so common symbol ⊃ is used for implication in order to avoid the use of too many arrows in notations.

The various chapters so far have introduced the basics of process-algebraic reasoning, including essential concepts such as recursion, parallel composition, and abstraction, and several extensions of this basic framework with time, data, and state. This one-but-last chapter introduces two more extensions, to reason about priorities and probabilities, and elaborates briefly on mobility and variants of parallel composition in Sections 11.3 and 11.4.

Priorities

In order to specify certain applications, it is useful to be able to restrict the non-determinism in process descriptions, by allowing certain actions to have priority over others in a choice context. A priority mechanism has proved itself useful in the following circumstances:

1. (i) when describing interrupts and disrupts, where the normal execution of a system is pre-empted by an event that has priority;

2. (ii) when giving semantics to certain features of programming languages such as interrupt or error handling mechanisms;

3. (iii) when timing is involved, when some events may not happen prematurely and other events may need to happen as soon as possible (maximal progress);

4. (iv) when describing scheduling algorithms.

This section introduces a priority mechanism in the equational and operational frameworks introduced in earlier chapters. Assume that certain actions have priority over other actions. This is expressed by assuming there is some (irreflexive) partial ordering ≺ on the set of actions A. For simplicity, consider this partial ordering to be fixed. This means the priority is static.

This book about process algebra improves on its predecessor, written by Jos Baeten and Peter Weijland 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.