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.