Society becomes increasingly more dependent on complex computer-based systems that are composed of several components that act concurrently and interact -- to synchronize and communicate with each other. The complexity of these systems arises to a great extent from the many ways in which their components can interact. The presence of a need to act and interact also on time adds considerably to the complexity.
In developing such a system, it is important to be able to acquire a better understanding of the relevant issues at the conceptual level, to describe the system in a precise way at various levels of detail, and to analyse it on the basis of the descriptions. When the early algebraic theories about processes, such as ACP, CCS and CSP, were developed for that purpose, the established opinion was still that timing is a concern that can more often than not be treated independently. It is therefore not surprising that timing is deliberately ignored in those theories. At present, they have all been extended to deal with timing.
Timing may be needed for various reasons. Timing may simply be essential for the correct behaviour of a system. This is, for example, the case with most controllers. Their correct behaviour, often derived from physical laws, usually involves actions being performed between certain time bounds. Even if timing is not essential for the correct behaviour of a system, there may be good reasons to implement it in a way such that suitable timing becomes essential for the correct behaviour. For example, for certain data communication protocols, it depends on the timing of certain actions whether they behave, at an appropriate level of abstraction, like a queue. Still another reason may be that there is just a need to pay much attention to performance aspects of a system.
In this book, a coherent collection of four algebraic theories about processes, each dealing with timing in a different way, is presented. The timing of actions is either relative (to the time at which the preceding action is performed) or absolute and the time scale on which the time is measured is either discrete or continuous. The presented theories are all extensions of ACP (Algebra of Communicating Processes).
We use the term process to mean any system whose behaviour is made up of discrete actions. Each action of a process is either performed synchronously with an action of another process, in which case an interaction takes place between those processes, or it is performed on its own. In the latter case, the action is often nothing but an interaction between subprocesses of the process concerned, i.e. an internal interaction. Our point of view is that not only the system of interest is a process, but also the components of which it is composed and the environment with which it interacts.
Sending a message to another process and receiving a message from another process are typical examples of the kinds of actions that are performed by a process. Synchronous communication of a message between two processes is an example of an interaction that takes place when a send action of one process and a matching receive action of the other process are performed synchronously. Other examples of the kinds of actions that processes perform are: putting a message in a queue, fetching a message from a queue, reading a datum from a memory cell, and writing a datum to a memory cell.
The theories about processes presented in this book are algebraic in the following ways: operators are used to compose processes and equations are used to define the nature of processes. Our intuitive understanding of the nature of the processes concerned provides the primary justification of the equations that are taken as axioms. However, we also present for each theory a mathematical model which is close to the intuitive understanding.
Each theory makes fully precise, by introducing a collection of constants and operators, what terms can be used as mathematical expressions for the processes considered in the theory. These operators enable us to describe a system as a system composed of several components, and to describe the composition of the system and the environment with which it interacts. Each theory makes also fully precise, by introducing a collection of equations as axioms, how to establish whether two terms represent the same process. These equations enable us to analyse a described system by mere algebraic calculations. The presented model of the axioms is a suitable basis for checking properties that cannot be expressed in the form of an equation.
The four theories about processes that deal with timing make up a coherent collection in the following sense. All four theories are generalizations of ACP without timing. The theory with absolute timing in which time is measured on a continuous time scale is a generalization of the theory with absolute timing in which time is measured on a discrete time scale. The two theories with absolute timing can easily be extended with a mechanism for parametric absolute timing which provides a way to deal with relative timing. That is, the extended theories are generalizations of the corresponding theories with relative timing.
If one theory is a generalization of another theory, this roughly means that the processes considered in the former theory essentially include the processes considered in the latter theory. That is the reason why abstraction from timing is possible in a theory with timing and discretization is possible in the theory with absolute timing in which time is measured on a continuous time scale. Abstraction from timing yields processes considered in a theory with timing that correspond with processes considered in ACP without timing. Discretization yields processes considered in a theory in which time is measured on a continuous time scale that correspond with processes considered in a theory in which time is measured on a discrete time scale. Abstraction from timing enables analysis of systems without carrying the timing details wherever they are not needed. Discretization enables analysis of systems at a level where time is measured with a finite precision wherever that is sufficient.
All four theories about processes that deal with timing are extended with mechanisms for abstraction from (internal) actions. This, together with abstraction from timing, enables us to verify whether two descriptions, one containing more implementation details than the other, represent the same system after appropriate abstraction.
It seems appropriate to use the term process algebra to mean a model of an algebraic theory about processes. However, as customary, we mostly use the term process algebra to mean an algebraic theory about processes. Sometimes, we even use it to mean a collection of algebraic theories about processes -- as in the title of this book.
Chapter 1, which is an introductory chapter, is primarily meant to acquire a good insight into the basic concepts of ACP-style process algebras in a setting without timing. In Chapters 2 to 5, which build on Chapter 1, ACP is extended to capture timing in four different ways. Chapters 2 and 3 introduce versions of ACP with relative timing and absolute timing in which time is measured on a discrete time scale. The version introduced in Chapter 2 is considered to be the simplest version of ACP with timing. Chapters 4 and 5 introduce versions of ACP with relative timing and absolute timing in which time is measured on a continuous time scale.
In each of the Chapters 1 to 5, first the concepts around which the version concerned has been set up are explained informally and then a formal presentation of the version is given. The formal presentation includes the signature (fixing the constants and operators that are considered) and the axioms of the theory concerned as well as transition rules from which a model for the theory can be obtained in a standard way. Examples are given of how true equations are derived from the axioms, and how possible transitions of processes (representing their capabilities to perform actions or to idle) can be inferred from the transition rules. The use of each version is illustrated by means of some small examples concerning the description of simple processes found in practice. These small examples concern amongst other things a burglar alarm, a communication protocol known as the concurrent alternating bit protocol, a railroad crossing controller, and a gas burner controller. Larger examples including some algebraic calculations are also given. These larger examples concern a message passing system, a communication protocol known as the positive acknowledgement with retransmission protocol, a mutual exclusion protocol known as Fischer's protocol, and a bottle filling system.
Each of the Chapters 2 to 5 concludes with a section that establishes connections between the theory introduced in that chapter and the ones introduced in the preceding chapters. These connections explain why the presented theories are generalization of certain others.
In Chapter 6, the versions of ACP with timing introduced in Chapters 2 to 5 are extended with abstraction from (internal) actions. In Chapter 7, the version of ACP with timing introduced in Chapter 5 is extended with three interesting features, viz. a feature that enables processes to interact with a state, a feature that enables processes to create processes, and a feature to enforce that certain actions take place as soon as possible. These features can be added in a similar way to the other versions of ACP with timing introduced in this book.
There are also two appendices. Appendix A outlines the proofs of soundness and completeness for the axioms of the version of ACP with timing introduced in Chapter 2. Appendix B introduces the basic definitions and results from equational logic and structural operational semantics on which the formal presentation of all theories and models included in this book are founded, and reviews some further relevant topics.
The symbols used in the book are for the greater part listed in a glossary.
Each chapter is a prerequisite for all subsequent chapters with the exception of the following: Chapter 3 is not a prerequisite for Chapter 4, and Chapter 6 is not a prerequisite for Chapter 7. The examples and exercises are integrated with the text. They should not be ignored.
Many people contributed in one way or another to this book: Jan Bergstra, Lou van den Dries, Loe Feijs, Wan Fokkink, Rob van Glabbeek, Jan Friso Groote, Steven Klusener, Michel Reniers, Gheorghe Stefanescu, Jan Joris Vereijken, Chris Verhoef, Mark van der Zwaag and many others.
We also want to thank the participants of the Training School on Techniques for Software Specification and Verification at UNU/IIST (United Nations University, International Institute for Software Technology) in Macau, September 2001, and students attending the seminar on Process Algebra with Timing at Eindhoven University of Technology in the academic year 2000--2001, for pointing out errors and obscurities in drafts of the book.