Power simulation and its relation to traces and failures refinement

AbstractThere are two quite distinct approaches commonly used when giving meaning to process algebra expressions: an operational semantics, often associated with the CCS language, defines an equivalence between terms by considering whether each can simulate the other; a denotational semantics, often associated with CSP, provides a mapping, recursively defined over the structure of the language, taking each term into a carefully chosen collection of set-theoretic objects. (The traces and failures models are well-known examples of such semantic domains.) We present a formal link between the two approaches, consisting in defining a variant of the bisimulation equivalence that naturally gives rise to the traces and failures ordering. We have no way at present to extend this result to the failures/divergence model