Event structures for the reversible early internal π-calculus

Abstract

The 휋-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the 휋-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 introduce two reversible forms of the internal 휋-calculus; these are the first to use early semantics. The internal 휋-calculus is a subset of the 휋-calculus where every link sent by an output is private, yielding greater symmetry between inputs and outputs. One of the new reversible calculi uses static reversibility, where performing an action does not change the structure of the process, and the other uses dynamic reversibility, where performing an action moves it to a separate history. We show an operational correspondence between the two calculi. For the static calculus we define denotational event structure semantics, which generate an event structure inductively on the structure on the process. For the dynamic calculus we define operational event structure semantics, which generate an event structure based on a labelled asynchronous transition system. We describe a correspondence between the resulting event structures.