Sequential composition

In the process theory BSP(A) discussed in Chapter 4, the only way of combining two processes is by means of alternative composition. For the specification of more complex systems, additional composition mechanisms are useful. This chapter treats the extension with a sequential-composition operator. Given two process terms x and y, the term x · y denotes the sequential composition of x and y. The intuition of this operation is that upon the successful termination of process x, process y is started. If process x ends in a deadlock, also the sequential composition x · y deadlocks. Thus, a pre-requisite for a meaningful introduction of a sequential-composition operator is that successful and unsuccessful termination can be distinguished. As already explained in Chapter 4, this is not possible in the theory MPT(A) as all processes end in deadlock. Thus, as before, as a starting point the theory BSP(A) of Chapter 4 is used. This theory is extended with sequential composition to obtain the Theory of Sequential Processes TSP(A). It turns out that the empty process is an identity element for sequential composition: x · 1 = 1 · x = x.

The process theory TSP

This section introduces the process theory TSP, the Theory of Sequential Processes. The theory has, as before, a set of actions A as its parameter. The signature of the process theory TSP(A) is the signature of the process theory BSP(A) extended with the sequential-composition operator.