MobilityReadingGroup

A Parametric Framework for Reversible Pi-Calculi

Doriana MEDIC, Claudio ANTARESMEZZINA, Iain PHILLIPS, Nobuko YOSHIDA

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in π-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible π-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible π-calculus causal semantics.

@article{MMPY2020,
  author = {Doriana Medic and Claudio Antares Mezzina and Iain Phillips and Nobuko Yoshida},
  title = {{A Parametric Framework for Reversible Pi-Calculi}},
  journal = {IC},
  volume = {275},
  pages = {1--57},
  publisher = {Elsevier},
  year = 2020
}

@article{MMPY2020,
  author = {Doriana Medic and Claudio Antares Mezzina and Iain Phillips and Nobuko Yoshida},
  title = {{A Parametric Framework for Reversible Pi-Calculi}},
  journal = {Information and Computation},
  volume = {275},
  pages = {1--57},
  publisher = {Elsevier},
  doi = "10.1016/j.ic.2020.104644",
  year = 2020
}