Our first view of a concurrent process is that of a machine where every detail of its behaviour is explicit. We could take as our machine model automata in the sense of classical automata theory [RS59], also known as transition systems [Kel76]. Automata are fine except that they cannot represent situations where parts of a machine work independently or concurrently. Since we are after such a representation, we use Petri nets [Pet62, Rei85] instead. This choice is motivated by the following advantages of nets:

1. Concepts. Petri nets are based on a simple extension of the concepts of state and transition known from automata. The extension is that in nets both states and transitions are distributed over several places. This allows an explicit distinction between concurrency and sequentiality.

2. Graphics. Petri nets have a graphical representation that visualises the different basic concepts about processes like sequentiality, choice, concurrency and synchronisation.

3. Size. Since Petri nets allow cycles, a large class of processes can be represented by finite nets. Also, as a consequence of (1), parallel composition will be additive in size rather than multiplicative.

An attractive alternative to Petri nets are event structures introduced in [NPW81] and further developed by Winskel [Win80, Win87]. Event structures are more abstract than nets because they do not record states, only events, i.e. the occurences of transitions. But in order to forget about states, event structures must not contain cycles. This yields infinite event structures even in cases where finite (but cyclic) nets suffice.

Many computing systems consist of a possibly large number of components that not only work independently or concurrently, but also interact or communicate with each other from time to time. Examples of such systems are operating systems, distributed systems and communication protocols, as well as systolic algorithms, computer architectures and integrated circuits.

Conceptually, it is convenient to treat these systems and their components uniformly as concurrent processes. A process is here an object that is designed for a possibly continuous interaction with its user, which can be another process. An interaction can be an input or output of a value, but we just think of it abstractly as a communication. In between two subsequent communications the process usually engages in some internal actions. These proceed autonomously at a certain speed and are not visible to the user. However, as a result of such internal actions the process behaviour may appear nondeterministic to the user. Concurrency arises because there can be more than one user and inside the process more than one active subprocess. The behaviour of a process is unsatisfactory for its user(s) if it does not communicate as desired. The reason can be that the process stops too early or that it engages in an infinite loop of internal actions. The first problem causes a deadlock with the user(s); the second one is known as divergence. Thus most processes are designed to communicate arbitrarily long without any danger of deadlock or divergence.

A crucial test for any theory of concurrent processes is case studies. These will clarify the application areas where this theory is particularly helpful but also reveal its shortcomings. Such shortcomings can be challenges for future research.

Considering all existing case studies based on Petri nets, algebraic process terms and logical formulas, it is obvious that these description methods are immensely helpful in specifying, constructing and verifying concurrent processes. We think in particular of protocol verification, e.g. [Vaa86, Bae90], the verification of VLSI algorithms, e.g. [Hen86], the design of computer architectures, e.g. [Klu87, DD89a, DD89b], and even of concurrent programming languages such as OCCAM [INM84, RH88] or POOL [Ame85, ABKR86, AR89, Vaa90]. However, these examples use one specific description method in each case.

Our overall aim is the smooth integration of description methods that cover different levels of abstraction in a top-down design of concurrent processes. This aim is similar to what Misra and Chandy have presented in their rich and beautiful book on UNITY [CM88]. However, we believe that their approach requires complementary work at the level of implementation, i.e. where UNITY programs are mapped onto architectures.

Our presentation of three different views of concurrent processes attempts to contribute to this overall aim. To obtain a coherent theory, we concentrated on a setting where simple classes of nets, terms and formulas are used. We demonstrated the applicability of this setting in a series of small but non-trivial process constructions.

The stepwise development of complex systems through various levels of abstraction is good practice in software and hardware design. However, the semantic link between these different levels is often missing. This book is intended as a detailed case study how such links can be established. It presents a theory of concurrent processes where three different semantic description methods are brought together in one uniform framework. Nets, terms and formulas are seen as expressing complementary views of processes, each one describing processes at a different level of abstraction.

• Petri nets are used to describe processes as concurrent and interacting machines which engage in internal actions and communications with their environment or user.

• Process terms are used as an abstract concurrent programming language. Due to their algebraic structure process terms emphasise compositionality, i.e. how complex terms are composed from simpler ones.

• Logical formulas of a first-order predicate logic, called trace logic, are used as a specification language for processes. Logical formulas specify safety and liveness aspects of the communication behaviour of processes as required by their users.

At the heart of this theory are two sets of transformation rules for the top-down design of concurrent processes. The first set can be used to transform logical formulas stepwise into process terms, and the second set can be used to transform process terms into Petri nets. These rules are based on novel techniques for the operational and denotational semantics of concurrent processes.

We now introduce a second view of concurrent processes whereby each process is a term over a certain signature of operator symbols. By interpreting these symbols on nets, we will solve the problem of compositionality. As interpretations we take a selection of the operators suggested in Lauer's COSY, Milner's CCS and Hoare's CSP.

Lauer's COSY (Concurrent Systems) is one of the first approaches to compositionality of processes on a schematic, uninterpreted level [LTS79]. It originates from path expressions [CH74] and can thus be seen as an extension of regular expressions to include parallelism. We use here COSY's operator for parallel composition because, as we shall see later in Chapter 4, it enjoys pleasant logical properties.

A significant step beyond COSY is Milner's CCS (Calculus of Communicating Systems) with its conceptual roots in algebra and the λ-calculus [Mil80, Mil83]. From CCS we take the idea that processes are recursive terms over certain operator symbols, i.e. they form the smallest set that is generated by the operator symbols and closed under parameterless recursion. In COSY only iteration is present as might be clear from its background in regular expressions. By using recursion we ensure that process terms are Turing powerful even on the schematic level without the help of interpreted values or variables. We also take CCS's choice operator because it allows a very clear treatment on the level of nets, and its notion of action morphism by which actions can be renamed.

INTRODUCTION

This book provides a systematic introduction to process algebra, suitable for teaching purposes. By the term process algebra we mean the study of concurrent communicating processes in an algebraic framework, following the approach of J.A. Bergstra and J.W. Klop (see section 8.1). In the present book we treat concurrency theory (the theory of concurrent communicating processes) in an axiomatic way, just as for instance the study of mathematical objects as groups or fields starts with an axiomatization of the intended objects. This axiomatic method is algebraic in the sense that we consider structures (also called “process algebras”) as models of some set of (mostly) equational axioms. These structures are equipped with several operators, and so we use the term algebra in the sense of model theory. R. Milner, with his Calculus of Communicating Systems (CCS), is generally considered to be the initiator of the field of process algebra. CCS forms the basis for most of the axiom systems presented below.

There is ample motivation for such an axiomatic-algebraic approach to concurrency theory. The main reason is that there is not one definitive notion of process. There is a staggering amount of properties which one may or may not attribute to processes, there are dozens of views (semantics) which one may have on processes, and there are infinitely many models of processes. So an attempt to organize this field of process theories leads very naturally and almost unavoidably to an axiomatic methodology. A curious consequence is that one has to answer the question “What is a process?” with the seemingly circular answer “A process is something that obeys a certain set of axioms … for processes”.

BISIMULATION AND TRACE SEMANTICS

So far, we only considered models having the property of containing a submodel which is isomorphic to the initial algebra of the current theory (for instance see 2.7.35). In other words we may say that if two finite processes in a model are equal, this equality must be derivable from the theory.

Models that with respect to finite processes correspond to the graph model or the term model are said to be models in bisimulation semantics. Because for every one of our theories, its initial model is a model in bisimulation semantics, our axiom systems are said to be a complete axiomatization of bisimulation semantics. In this chapter we will consider other semantics than bisimulation semantics, and we will present complete axiomatizations of these alternative semantics as well.

Because all operators except for + and · can be eliminated from closed terms, we will mainly restrict ourselves to the theory BPA, with special constant 8. The addition of the special constant τ leads to many interesting observations, and a vastly increased complexity. We do not include it here, in order to focus on a few key issues.

We will discuss semantics that identify more processes than bisimulation semantics does. The advantage of this is clear: calculations become easier, and more simplifications can be made. On the other hand, some differences between processes are disregarded, and as a consequence, in some cases some operators cannot be defined any more.

We start with the repetition of an earlier result.

PRIORITIES AND INTERRUPTS

In this chapter will develop some additional features to the theory in the former chapters, in order to enlarge the area of its application. Let us start by introducing a mechanism to describe priorities in the system ACP of chapter 4 (see 4.2.1). In ACP with priorities some actions have priority over others in a sum. This mechanism can be used to model interrupts in a distributed system.

REMARK

We will not combine the system ACP with priorities with τ and the abstraction operator of chapter 5. This can be done in several ways, see 6.1.23.

PARTIAL ORDERING

Assume we have a partial ordering on the set of atomic actions A. This means that we have a relation < satisfying, for all a,b,c∈ A:

1. at most one< / i. of a < b, b < a, a = b is the case;

2. a<b and b<c imply a<c.

a<b now means that b has priority over a. Special constants like δ, are not included in the ordering, and thus never have priority over other actions (this is forced by axiom A6).

AIM

We want to define an operator ε implementing these priorities, i.e: if a<b, a<c, and b and c are not related, we want to have:

1. ε(a + b) = b; ε(a + c) = c;

2. ε(b + c) = b + c.

ACTION RELATIONS

It is relatively straightforward to give a definition by action relations of the priority operator. We present such a definition in table 68 below.

This book was written in the years 1989 and 1990 at the Centre for Mathematics and Computer Science in Amsterdam. Much of the material comes from a Dutch book (reference Baeten [1986]), that was used in university courses at the University of Amsterdam and the University of Utrecht.

For the first time, this book brings together a lot of work in the area of algebraic process theory, as this has been developed since 1982 by a group of people in Amsterdam and Utrecht under the guidance of Jan Bergstra. Most of the research that found its way into this book was funded by European programmes, notably METEOR (ESPRIT I), SPECS (RACE), CONCUR (ESPRIT II BRA).

Many people contributed in one way or another to this book. We want to mention (in alphabetical order) Gert-Jan Akkerman, Jan Bergstra, Wiet Bouma, Jeroen Bruijning, Nicolien Drost, Rob van Glabbeek, Jan Friso Groote, Jan Willem Klop, Karst Koymans, Evangelos Kranakis, Sjouke Mauw, Kees Middelburg, Hans Mulder, Eric Nieuwland, Ernst-Rudiger Olderog, Alban Ponse, Scott Smolka, Frits Vaandrager, Gert Veltink, Jos Vrancken, Han Zuidweg. Thanks are due to the head of the Department of Software Technology of the Centre for Mathematics and Computer Science, Jaco de Bakker, who created an excellent working atmosphere.

The first author wants to dedicate this book to his wife Jeanne, who was very important in its writing, but cannot see its completion.