An Operational Petri Net Semantics for A2CCS

• Autorzy: Gorrieri R. , Versari C.
• Języki publikacji: EN

Abstrakty

EN

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 wellrepresented in the net, we also prove that a process p and its associated net Net(p) are step bisimilar (Theorem 5.2).

Słowa kluczowe

EN

Labelled Transition Systems (LTS); P/T Petri nets; language A2CCS; step semantics; net transitions; DDM semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 109, nr 2
• Strony: 135--160
• Opis fizyczny: Bibliogr. 27 poz., wykr.

Twórcy

autor

Gorrieri R.

autor

Versari C.

• Dipartimento di Scienze dell’Informazione, Universita di Bologna, Mura A. Zamboni, 7, 40127 Bologna, Italy,

Bibliografia

• [1] M. Bernardo, N. Busi, R. Gorrieri, "A Distributed Semantics for EMPA Based on Stochastic Contextual Nets", The Comp. Jour. 38(7): 492-509, 1995.
• [2] E. Best, R. Devillers, M. Koutny, "The Box Algebra = Petri Nets + Process Expressions.", Inf. Comput., 178(1):44-100, 2002.
• [3] A. Brogi, R. Gorrieri:, "A Distributed, Net Oriented Semantics for Delta Prolog", in Theory and Practice of Software Development - Colloquium on Trees in Algebra and Programming (TAPSOFT 89), LNCS 351, 162-177, Springer-Verlag, 1989.
• [4] N. Busi, R. Gorrieri, "Distributed Conflicts in Communicating Systems", in Object-Based Models and Languages for Concurrent Systems, LNCS 924, 49-65, Springer-Verlag, 1994.
• [5] N. Busi, R. Gorrieri, "A Petri Net Semantics for π- calculus", In Proc. Concur'95, LNCS 962, Springer-Verlag, 145-159, 1995.
• [6] N. Busi, R. Gorrieri, "Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs", Journal of Logic and Alg. Prog. 78(3):138-162, 2009.
• [7] P. Degano, R. De Nicola, U. Montanari, "A Distributed Operational Semantics for CCS based on C/E Systems", Acta Informatica 26(1-2):59-91, 1988.
• [8] P. Degano, R. Gorrieri, S. Marchetti, "An Exercise in Concurrency: A CSP Process as a Condition/Event System", Advances in Petri Nets 1988, LNCS 340, 85-105, Springer-Verlag, 1988.
• [9] E.W.Dijkstra, "Hierarchical ordering of sequential processes", Acta Informatica 1(2):115-138, 1971.
• [10] R. van Glabbeek, F. Vaandrager, "Petri Net Models for Algebraic Theories of Concurrency", in Proc. PARLE'87, LNCS 259, 224-242, Springer-Verlag, 1987.
• [11] U. Goltz, "On Representing CCS Programs by Finite Petri Nets", in Proc. MFCS'88, LNCS 324, 339-350, Springer-Verlag, 1988.
• [12] U. Goltz, "CCS and Petri Nets", LNCS 469, 334-357, Springer-Verlag, 1990.
• [13] R. Gorrieri, "A Hierarchy of System Descriptions via Atomic Linear Refinement", Fundamenta Informaticae, 16 (3/4):289-336, 1992.
• [14] R. Gorrieri, U. Montanari, "SCONE: A Simple Calculus of Nets", in Proc. CONCUR'90, LNCS 458, 2-30, Springer-Verlag, 1990.
• [15] R. Gorrieri, U. Montanari, "Towards Hierarchical Specification of Systems: A Proof System for Strong Prefixing", Int. Journal of Foundations of Computer Science, 1(3):277-293, 1990.
• [16] R. Gorrieri, S. Marchetti, U. Montanari, "A2CCS: Atomic Actions for CCS", Theoretical Computer Science 72(2-3): 203-223, 1990.
• [17] R. Gorrieri, C. Versari, "A Process Calculus for expressing finite Place/Transition Petri Nets", in Procs. Express'10, EPTCS, 2010.
• [18] C.A.R. Hoare, Communicating Sequential Processes Prentice-Hall International Series in Computer Science, 1985.
• [19] R. Milner, Communication and Concurrency, Prentice-Hall, 1989.
• [20] R. Milner. Communicating and mobile systems: the π-calculus, Cambridge University Press, 1999.
• [21] E. R. Olderog, Nets, Terms and Formulas, Cambridge Tracts in Theoretical Computer Science 23, Cambridge University Press, 1991.
• [22] S. Patil "Limitations and Capabilities of Dijkstra's Semaphore Primitives for Coordination Among Processes", Computation Structures Group Memo 57, Project MAC, MIT, 1971.
• [23] J.L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
• [24] G. D. Plotkin "A structural approach to operational semantics", Technical Report DAIMI FN-19, Aarhus University (1981)
• [25] G. D. Plotkin "A structural approach to operational semantics", J. Logic and. Algebraic Programming 60-61: 17-139 (2004).
• [26] W. Reisig, Petri Nets: An Introduction, EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1985.
• [27] A.W. Roscoe, The Theory and Practice of Concurrency Prentice-Hall,