Affiliations: Département d'informatique, Université Libre de Bruxelles, B-1050 Bruxelles, Belgium | LACL, Université Paris 12, 61, avenue du
général de Gaulle, 94010 Créteil, France | Department of Computing Science, University of Newcastle upon Tyne, NE1 7RU, UK
Abstract: IThe starting point of this paper is an algebraic Petri net
framework allowing one to express net compositions, such as iteration and
parallel composition, as well as transition synchronisation and restriction. We
enrich the original model by introducing new constructs supporting asynchronous
interprocess communication. Such a communication is made possible thanks to
special 'buffer' places where different transitions (processes) may deposit and
remove tokens. We also provide an abstraction mechanism, which hides buffer
places, effectively making them private to the processes communicating through
them. We then provide an algebra of process expressions, whose constants and
operators directly correspond to those used in the Petri net framework. Such a
correspondence is used to associate nets to process expressions in a
compositional way. That the resulting algebra of expressions is consistent with
the net algebra is demonstrated by showing that an expression and the
corresponding net generate isomorphic transition systems. This results in the
Asynchronous Box Calculus (or ABC), which is a coherent dual model,
based on Petri nets and process expressions, suitable for modelling and
analysing distributed systems whose components can interact using both
synchronous and asynchronous communication.
Keywords: Petri nets, process algebra, synchronous and asynchronous communication, structured operational semantics
