Event structures for the reversible early internal Pi-calculus

TL;DR

This paper introduces piIH, the first reversible early internal pi-calculus, with a denotational semantics based on reversible bundle event structures, emphasizing the importance of early semantics in reversible process calculi.

Contribution

It presents the first reversible version of the early pi-calculus, filling a gap in reversible process calculus research and providing a new denotational semantics framework.

Findings

Defines piIH, a reversible early internal pi-calculus.

Provides a denotational semantics using reversible bundle event structures.

Highlights the significance of early semantics in reversible process models.

Abstract

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 pi-calculus use reduction or late semantics, despite the early semantics of the (forward-only) pi-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 pi-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.