Since their first appearance, 2D barcodes have evolved with additional features including security, error detection and correction capability and the ability to encode different languages. The ability to encode a robust portable data file has made 2D symbologies attractive regardless of their extra space requirements. Accordingly, industries and organisations in various fields have adopted applications that use 2D barcodes within their systems. These range from medicine labelling for the healthcare industry and the marking of small items such as integrated circuit boards for IT vendors through to the secure transmission of battle-field plans in the defence industry. However, despite its potential for wider use, this technology has been adopted by only a few industries and organisations.

Mobile devices such as mobile phones and personal digital assistants (PDAs) are another notable technology that has evolved during the last decade. With their current sophisticated functions these devices can provide an entertainment centre, performing the role of a game console, a jukebox, a digital camera and a social organiser. As more advanced features and applications are developed, they should become less expensive and more commonly used. In fact, PDAs and mobile phones are now virtually universally used in industrialised countries across different age groups. Furthermore, they are always available, providing seamless and ubiquitous connectivity. As the research firm Gartner has predicted [19], this trend is expected to continue for some years.

Two-dimensional barcodes and mobile phones have a lot in common. They have become smaller, yet smarter, in the last decade and are still being improved.

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.