A stable non-interleaving early operational semantics for the pi-calculus
Research output: Contribution to journal › Journal article › peer-review
Standard
A stable non-interleaving early operational semantics for the pi-calculus. / Hildebrandt, Thomas Troels; Johansen, Christian; Normann, Håkon.
In: Journal of Logical and Algebraic Methods in Programming, Vol. 104, 2019, p. 227-253.Research output: Contribution to journal › Journal article › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - A stable non-interleaving early operational semantics for the pi-calculus
AU - Hildebrandt, Thomas Troels
AU - Johansen, Christian
AU - Normann, Håkon
PY - 2019
Y1 - 2019
N2 - We give the first non-interleaving early operational semantics for the pi-calculus which generalises the standard interleaving semantics and unfolds to the stable model of prime event structures. Our starting point is the non-interleaving semantics given for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject) causality and events are defined from a notion of locations derived from the syntactic structure of the process terms. We conservatively extend this semantics with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the dynamic communication topology of the pi-calculus. We prove that the semantics generalises both the standard interleaving early semantics for the pi-calculus and the non-interleaving semantics for CCS. In particular, it gives rise to a labelled asynchronous transition system unfolding to prime event structures.
AB - We give the first non-interleaving early operational semantics for the pi-calculus which generalises the standard interleaving semantics and unfolds to the stable model of prime event structures. Our starting point is the non-interleaving semantics given for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject) causality and events are defined from a notion of locations derived from the syntactic structure of the process terms. We conservatively extend this semantics with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the dynamic communication topology of the pi-calculus. We prove that the semantics generalises both the standard interleaving early semantics for the pi-calculus and the non-interleaving semantics for CCS. In particular, it gives rise to a labelled asynchronous transition system unfolding to prime event structures.
KW - Asynchronous transition systems
KW - Causality
KW - Early semantics
KW - Non-interleaving
KW - Pi-calculus
KW - Stability
U2 - 10.1016/j.jlamp.2019.02.006
DO - 10.1016/j.jlamp.2019.02.006
M3 - Journal article
AN - SCOPUS:85081549062
VL - 104
SP - 227
EP - 253
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
SN - 2352-2208
ER -
ID: 241102789