MobilityReadingGroup

Event Structure Semantics of (controlled) Reversible CCS

Eva GRAVERSEN, Iain PHILLIPS, Nobuko YOSHIDA

CCSK is a reversible form of CCS which is causal, meaning that actions can be reversed if and only if each action caused by them has already been reversed; there is no control on whether or when a computation reverses. We propose an event structure semantics for CCSK. For this purpose we define a category of reversible bundle event structures, and use the causal subcategory to model CCSK. We then modify CCSK to control the reversibility with a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we change our reversible bundle event structures by making the conflict relation asymmetric rather than symmetric, and we exploit their capacity for non-causal reversibility.

@article{GPY2021,
  author = {Eva Graversen and Iain Phillips and Nobuko Yoshida},
  title = {{Event Structure Semantics of (controlled) Reversible CCS}},
  journal = {JLAMP},
  series = {LNCS},
  volume = {121},
  pages = {--},
  publisher = {Elsevier},
  year = 2021
}

@article{GPY2021,
  author = {Eva Graversen and Iain Phillips and Nobuko Yoshida},
  title = {{Event Structure Semantics of (controlled) Reversible CCS}},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  series = {LNCS},
  volume = {121},
  pages = {--},
  publisher = {Elsevier},
  doi = "10.1016/j.jlamp.2021.100686",
  year = 2021
}