Full Abstraction for Strongly Fair Communicating Processes

We present a denotational semantics for a language of parallel communicating processes based on Hoare's CSP [10] and Milner's CCS [14], and we prove that the semantics is fully abstract with respect to a deadlock-sensitive notion of fair behavior. The model incorporates the assumption of strong fairness: every process which is enabled infinitely often makes progress infinitely often. The combination of fairness and deadlock causes problems because the "enabledness" of a process may depend on the status of other processes. We formulate a parameterized notion of strong fairness, generalizing the traditional notion of strong fairness [5] in a way that facilitates compositional analysis. We then provide a denotational semantics which uses a form of trace, augmented with information about enabledness, and is related to the failures model for CSP [2] and to Hennessy's acceptance trees [7]. By introducing closure conditions on trace sets, we achieve full abstraction [13]: two processes have the same meaning if and only if they exhibit identical behaviors in all contexts.