PROCESS ALGEBRA: A UNIFYING APPROACH
Ton yH oare · 2005
Process algebra studies systems that act and react continuously with their en- vironment. It model st hem by transition graphs, whose nodes represent their states, and whose edges are labelled with the names of events by which the yi n- teract with thei re nvironment. A trace of the behaviour of a process is recorded as a sequence of observable events i nw hich the process engages. Refinement is defined as the inclusion of all traces of a more refined process i nt hose 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 sim- ilarity 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 man yy ears has produced aw id ev ariety of process algebras, dis- tinguishe db ythe manner i nw hich 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 identit yb etween similarity and trace refinement, even for non-deterministi cs ystems. Obviously ,t hi su n ifying approac hi s 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.