Specifying Termination in CSP

In the original failure-divergence semantic model for Communicating Sequential Processes (CSP) the incomplete treatment of successful process termination, and in particular parallel termination, permitted unnatural processes to be defined where the behaviour of the system did not match the intention of the specification. In response to this problem we propose the introduction of three distinct but related parallel operators that between them provide a transparent and intuitive means for specifying the desired termination of concurrent processes where no such unnatural behaviours take place. We provide a comprehensive account of their semantics, algebraic properties and the relationship between them, and demonstrate that these new operators can replace the set of parallel operators defined in the original treatment of CSP. By way of a number of examples of the use of these operators we demonstrate how they provide a much more expressive, intuitive and robust system for the specification of parallel composition.