Two reversible forms of CCS

Danos, V. and Krivine, J., Reversible communicating systems. CONCUR 2004, LNCS, 3170. pp. 292-307.

Iain C. C. Phillips, Irek Ulidowski: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1-2): 70-96 (2007)

These two papers present different views on reversibility for CCS.  In both cases, a key question is how to deal with a process term such as $(a.P | a.Q | \bar{a}.R| \bar{a}.S) \backslash a$ which can evolve in two different ways, both leading to the same state $(P|Q|R|S)$: one where the $a.P$ and $\bar{a}.R$ synchronize, and one where $a.P$ and $\bar{a}.S$ synchronize.  A key question is, what additional information do we need to record so that the right synchronizations are undone.



Danos and Krivine present Reversible CCS (RCCS), in which processes are tagged with "histories".  When two processes communicate, the communication is recorded in each process's history, so that the right thing will happen on reversing the transition. 

Philips and Ulidowski present a general scheme for making a process calculus reversible, provided its rules fit certain constraints known from the Structural Operational Semantics (SOS) literature.  In contrast to RCCS, the idea is to preserve the structure of the process terms and record the "history" by adding "marks" to the operators to indicate which parts have been performed and which are still active.  Synchronization steps make use of "keys", or names, which are equal for two complementary actions that synchronize and otherwise different from each other.  This records the information about which   Calculi such as CCS and CSP are used as examples, in particular a reversible form of CCS called CCSK (CCS with Keys) is presented.  The different ways an "ambiguous" term such as $(a.P | a.Q | \bar{a}.R| \bar{a}.S) \backslash a$ can evolve become evident in the keys, for example, $(a[m].P | a[n].Q | \bar{a}[m].R| \bar{a}[n].S) \backslash a$ vs. $(a[m].P | a[n].Q | \bar{a}[n].R| \bar{a}[m].S) \backslash a$.

These two approaches, based on explicit histories vs. implicit naming/tagging of parts of terms, seem complementary. Their formal results are however somewhat different: Danos and Krivine study the issue of reachability and causal equivalence of reductions, whereas Philips and Ulidowski study bisimulation (forward and reverse).  It might be interesting to formally relate the two approaches (if this hasn't already been done).