An Operational Petri Net Semantics for A²CCS

Article type: Research Article

Authors: Gorrieri, Roberto | Versari, Cristian

Affiliations: Dipartimento di Scienze dell'Informazione, Università di Bologna, Mura A. Zamboni, 7, 40127 Bologna, Italy. {gorrieri, versari}@cs.unibo.it

Note: [] Address for correspondence: Dipartimento di Scienze dell'Informazione, Università di Bologna, Mura A. Zamboni, 7, 40127 Bologna, Italy

Abstract: A2CCS 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 A2CCS 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).

DOI: 10.3233/FI-2011-501

Journal: Fundamenta Informaticae, vol. 109, no. 2, pp. 135-160, 2011