Process Algebra: A Unifying Approach

Abstract

Process algebra studies systems that act and react continuously with their environment. It models them by transition graphs, whose nodes represent their states, and whose edges are labelled with the names of events by which they interact with their environment. A trace of the behaviour of a process is recorded as a sequence of observable events in which the process engages. Refinement is defined as the inclusion of all traces of a more refined process in those of the process that it refines. A simulation is a relation that compares states as well as events; by definition, two processes that start in states related by a simulation, and which then engage in the same event, will end in states also related by the same simulation. A bisimulation is defined as a symmetric simulation, and similarity is defined as the weakest of all simulations. In classical automata theory, the transition graphs are deterministic: from a given node, there is at most one edge with a given label; as a result, trace refinement and similarity coincide in meaning.

Research over many years has produced a wide variety of process algebras, distinguished by the manner in which they compare processes, usually by some form of simulation or by some form of refinement. This paper aims to unify the study of process algebras, by maintaining the identity between similarity and trace refinement, even for non-deterministic systems. Obviously, this unifying approach is entirely dependent on prior exploration of the diversity of theories that apply to the unbounded diversity of the real world. The aim of unification is to inspire and co-ordinate the exploration of yet further diversity; in no way does it detract from the value of such exploration.