MobilityReadingGroup

Event Structures for the Reversible Early Internal Pi-Calculus

Eva GRAVERSEN, Iain PHILLIPS, Nobuko YOSHIDA

The pi-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the pi-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics.

The early version allows a process to receive names it already knows from the environment, while the late semantics and reduction semantics do not. All existing reversible versions of the π-calculus use reduction or late semantics, despite the early semantics of the (forward-only) π-calculus being more widely used than the late. We define piIH, the first reversible early pi-calculus, and give it a denotational semantics in terms of reversible bundle event structures. The new calculus is a reversible form of the internal π-calculus, which is a subset of the pi-calculus where every link sent by an output is private, yielding greater symmetry between inputs and outputs.

@inproceedings{GPY2020,
  author = {Eva Graversen and Iain Phillips and Nobuko Yoshida},
  title = {{Event Structures for the Reversible Early Internal Pi-Calculus}},
  booktitle = {12th Conference on Reversible Computation},
  series = {LNCS},
  volume = {12227},
  pages = {71--90},
  publisher = {Springer, Cham},
  year = 2020
}

@inproceedings{GPY2020,
  author = {Eva Graversen and Iain Phillips and Nobuko Yoshida},
  title = {{Event Structures for the Reversible Early Internal Pi-Calculus}},
  booktitle = {12th Conference on Reversible Computation},
  series = {LNCS},
  volume = {12227},
  pages = {71--90},
  publisher = {Springer, Cham},
  doi = "10.1007/978-3-030-52482-1 4",
  year = 2020
}