A Stable Non-interleaving Early Operational Semantics for the Pi-Calculus

详细信息    查看全文

• 关键词：Concurrency ; Non ; interleaving ; Pi ; calculus ; Early operational semantics ; Asynchronous transition systems ; Stability
• 刊名：Lecture Notes in Computer Science
• 出版年：2017
• 出版时间：2017
• 年：2017
• 卷：10168
• 期：1
• 页码：51-63
• 丛书名：Language and Automata Theory and Applications
• ISBN：978-3-319-53733-7
• 卷排序：10168

文摘

We give the first non-interleaving early operational semantics for the pi-calculus which generalizes 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. The semantics is conservatively extended 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.