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: operational semantics, often associated with the CCS language, define equivalences between terms by considering whether each can simulate the other; denotational semantics, often associated with CSP, provide 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