View article

Readiness and failure semantics are studied in the setting of Algebra of Communicating Processes (ACP). A model of process graphs modulo readiness equivalence, respectively, failure equivalence, is constructed, and an equational axiom system is presented which is complete for this graph model. An explicit representation of the graph model is given, the failure model, whose elements are failure sets. Furthermore, a characterisation of failure equivalence is obtained as the maximal congruence which is consistent with trace semantics. By suitably restricting the communication format in ACP, this result is shown to carry over to subsets of Hoare’s Communicating Sequential Processes (CSP) and Milner’s Calculus of Communicating Systems (CCS). Also, the characterisation implies a full abstraction result for the failure model. In the above we restrict ourselves to finite processes without -steps. At the end of the paper a …