Full Abstraction for Strongly Fair Communicating Processes

Stephen Brookes, Susan Older

Research output: Contribution to journalArticle

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)46-65
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
Volume1
Issue numberC
DOIs
StatePublished - 1995
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Full Abstraction for Strongly Fair Communicating Processes'. Together they form a unique fingerprint.

  • Cite this