Event structures for the reversible early internal π-calculus
File(s)
Accepted version
Author(s)
Graversen, Eva
Phillips, Iain
Yoshida, Nobuko
Type
Journal Article
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.
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.
Date Issued
2022-01
Date Acceptance
2021-09-15
Citation
Journal of Logical and Algebraic Methods in Programming, 2022, 124, pp.1-46
ISSN
2352-2208
Publisher
Elsevier
Start Page
1
End Page
46
Journal / Book Title
Journal of Logical and Algebraic Methods in Programming
Volume
124
Copyright Statement
© 2021 Elsevier Ltd. All rights reserved. This manuscript is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International Licence http://creativecommons.org/licenses/by-nc-nd/4.0/
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
GCHQ
The National Cyber Security Centre (NCSC)
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
Identifier
https://www.sciencedirect.com/science/article/pii/S2352220821000833?via%3Dihub
Grant Number
ERI 025567 (EP/K034413/1)
EP/K011715/1
EP/N027833/1
EP/T006544/1
EP/T014709/1
PO 20131167
EP/L00058X/1, PO 20131167
PO 20224051
4207702 / RFA 15845
4214176 / RFA 20601
EP/V000462/1
PO 20237614
Publication Status
Published
Date Publish Online
2021-09-21