Event structure semantics of (controlled) reversible CCS - Graversen,E; Phillips,ICC; Yoshida,N (Springer Verlag, 2018)
CCSK is a reversible form of CCS which is causal, meaning that ac-tions can be reversed if and only if each action caused by them has already beenreversed; there is no control on whether or when a computation reverses. We pro-pose an event structure semantics for CCSK. For this purpose we define a cat-egory of reversible bundle event structures, and use the causal subcategory tomodel CCSK. We then modify CCSK to control the reversibility with a rollbackprimitive, which reverses a specific action and all actions caused by it. To definethe event structure semantics of rollback, we change our reversible bundle eventstructures by making the conflict relation asymmetric rather than symmetric, andwe exploit their capacity for non-causal reversibility.