A stable non-interleaving early operational semantics for the pi-calculus
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Dokumenter
- A stable non-interleaving early operational semantics for the pi-calculus
Forlagets udgivne version, 843 KB, PDF-dokument
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.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Journal of Logical and Algebraic Methods in Programming |
Vol/bind | 104 |
Sider (fra-til) | 227-253 |
Antal sider | 27 |
ISSN | 2352-2208 |
DOI | |
Status | Udgivet - 2019 |
Antal downloads er baseret på statistik fra Google Scholar og www.ku.dk
ID: 241102789