Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Graversen:2022:10.1016/j.jlamp.2021.100720,
author = {Graversen, E and Phillips, I and Yoshida, N},
doi = {10.1016/j.jlamp.2021.100720},
journal = {Journal of Logical and Algebraic Methods in Programming},
pages = {1--46},
title = {Event structures for the reversible early internal π-calculus},
url = {http://dx.doi.org/10.1016/j.jlamp.2021.100720},
volume = {124},
year = {2022}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - The -calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operationalsemantics of the -calculus have been proposed, which can be classified according towhether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a processto receive names it already knows from the environment, while the late semantics andreduction semantics do not. All existing reversible versions of the -calculus use reduction or late semantics, despite the early semantics of the (forward-only) -calculusbeing 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 asubset of the -calculus where every link sent by an output is private, yielding greatersymmetry between inputs and outputs. One of the new reversible calculi uses staticreversibility, 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. Forthe static calculus we define denotational event structure semantics, which generate anevent structure inductively on the structure on the process. For the dynamic calculus wedefine operational event structure semantics, which generate an event structure basedon a labelled asynchronous transition system. We describe a correspondence betweenthe resulting event structures.
AU  - Graversen,E
AU  - Phillips,I
AU  - Yoshida,N
DO  - 10.1016/j.jlamp.2021.100720
EP  - 46
PY  - 2022///
SN  - 2352-2208
SP  - 1
TI  - Event structures for the reversible early internal π-calculus
T2  - Journal of Logical and Algebraic Methods in Programming
UR  - http://dx.doi.org/10.1016/j.jlamp.2021.100720
UR  - https://www.sciencedirect.com/science/article/pii/S2352220821000833?via%3Dihub
UR  - http://hdl.handle.net/10044/1/91740
VL  - 124
ER  -
Download