Translation of CCS into CSP, Correct up to Strong Bisimulation

Abstract

We present a translation of CCS into CSP which is correct with respect to strong bisimulation. To our knowledge this is the first such translation to enjoy a correctness property. This contributes to the unification of the CCS and CSP families of concurrent calculi, in the spirit of Hoare and He’s unification programme through Unifying Theories of Programming. To facilitate this translation, we define CCSTau, the extension of CCS with visible synchronisation actions and the hiding operator. This separation of concerns between synchronisation and hiding turns out be sufficient to obtain our correct translation. Our translation, implemented in a Haskell prototype, makes it possible to use CSP-based verifiers such as FDR to reason about trace and failure (hence may- and must-testing) preorders for CCS processes.