## Monday, April 14, 2014

### 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.