This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality pi-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible pi-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible pi-calculus causal semantics. (C) 2020 Elsevier Inc. All rights reserved.
A parametric framework for reversible π-calculi
Doriana Medic;
2020-01-01
Abstract
This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality pi-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible pi-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible pi-calculus causal semantics. (C) 2020 Elsevier Inc. All rights reserved.File | Dimensione | Formato | |
---|---|---|---|
1-s2.0-S0890540120301322-main.pdf
Accesso aperto
Descrizione: A parametric framework for reversible π-calculi
Tipo di file:
PDF EDITORIALE
Dimensione
1.26 MB
Formato
Adobe PDF
|
1.26 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.