An Operational Petri Net Semantics for A 2 CCS

Abstract

A²CCS is a conservative extension of CCS, enriched with an operator of strong prefixing, enabling the modeling of atomic sequences and multi-party synchronization (realized as an atomic sequence of binary synchronizations); the classic dining philosophers problem is used to illustrate the approach. A step semantics for A²CCS is also presented directly as a labeled transition system. A safe Petri net semantics for this language is presented, following the approach of Degano, De Nicola, Montanari and Olderog. We prove that a process p and its associated net Net(p) are interleaving bisimilar (Theorem 5.1). Moreover, to support the claim that the intended concurrency is well-represented in the net, we also prove that a process p and its associated net Net(p) are step bisimilar (Theorem 5.2).