A stable non-interleaving early operational semantics for the pi-calculus

Research output: Contribution to journalJournal articlepeer-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 journalJournal articlepeer-review

Harvard

Hildebrandt, TT, Johansen, C & Normann, H 2019, 'A stable non-interleaving early operational semantics for the pi-calculus', Journal of Logical and Algebraic Methods in Programming, vol. 104, pp. 227-253. https://doi.org/10.1016/j.jlamp.2019.02.006

APA

Hildebrandt, T. T., Johansen, C., & Normann, H. (2019). A stable non-interleaving early operational semantics for the pi-calculus. Journal of Logical and Algebraic Methods in Programming, 104, 227-253. https://doi.org/10.1016/j.jlamp.2019.02.006

Vancouver

Hildebrandt TT, Johansen C, Normann H. A stable non-interleaving early operational semantics for the pi-calculus. Journal of Logical and Algebraic Methods in Programming. 2019;104:227-253. https://doi.org/10.1016/j.jlamp.2019.02.006

Author

Hildebrandt, Thomas Troels ; Johansen, Christian ; Normann, Håkon. / A stable non-interleaving early operational semantics for the pi-calculus. In: Journal of Logical and Algebraic Methods in Programming. 2019 ; Vol. 104. pp. 227-253.

Bibtex

@article{d1b95fbbba3845248c6783dee2626b3d,
title = "A stable non-interleaving early operational semantics for the pi-calculus",
abstract = "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.",
keywords = "Asynchronous transition systems, Causality, Early semantics, Non-interleaving, Pi-calculus, Stability",
author = "Hildebrandt, {Thomas Troels} and Christian Johansen and H{\aa}kon Normann",
year = "2019",
doi = "10.1016/j.jlamp.2019.02.006",
language = "English",
volume = "104",
pages = "227--253",
journal = "Journal of Logical and Algebraic Methods in Programming",
issn = "2352-2208",
publisher = "Elsevier",

}

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