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

Thomas Troels Hildebrandt, Christian Johansen*, Håkon Normann

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

2 Citations (Scopus)
153 Downloads (Pure)

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.

Original languageEnglish
JournalJournal of Logical and Algebraic Methods in Programming
Volume104
Pages (from-to)227-253
Number of pages27
ISSN2352-2208
DOIs
Publication statusPublished - 2019

Keywords

  • Asynchronous transition systems
  • Causality
  • Early semantics
  • Non-interleaving
  • Pi-calculus
  • Stability

Cite this