Compositional semantics for open Petri nets based on deterministic processes

In order to model the behaviour of open concurrent systems by means of Petri nets, we introduce open Petri nets, a generalisation of the ordinary model where some places, designated as open, represent an interface between the system and the environment. Besides generalising the token game to reflect this extension, we define a truly concurrent semantics for open nets by extending the Goltz–Reisig process semantics of Petri nets. We introduce a composition operation over open nets, characterised as a pushout in the corresponding category, suitable for modelling both interaction through open places and synchronisation of transitions. The deterministic process semantics is shown to be compositional with respect to such a composition operation. If a net . Technically, our result is similar to the amalgamation theorem for data-types in the framework of algebraic specification. A possible application field of the proposed constructions and results is the modelling of interorganisational workflows, recently studied in the literature. This is illustrated by a running example.