Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
Compositional semantics for open Petri nets based on deterministic processes
@ARTICLE{BCEH05MSCS,
title = {{Compositional semantics for open Petri nets based on deterministic processes}},
author = {{Paolo} {Baldan} and {Andrea} {Corradini} and {Hartmut} {Ehrig} and {Reiko} {Heckel}},
journal = {Mathematical Structures in Computer Science},
pages = {1-35},
abstract = {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 Z3 results as the composition of two nets Z1 and Z2, having a common subnet Z0, then any two deterministic processes of Z1 and Z2 that agree on the common part, can be amalgamated to produce a deterministic process of Z3. Conversely, any deterministic process of Z3 can be decomposed into processes of the component nets. The amalgamation and decomposition operations are shown to be inverse to each other, leading to a bijective correspondence between the deterministic processes of Z3 and the pair of deterministic processes of Z1 and Z2 that agree on the common subnet Z0. 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.},
volume = {15},
number = {1},
year = {2005},
url = {http://www.dsi.unive.it/~baldan/Papers/Soft-copy-pdf/OpenLong.pdf},
ee = {http://dx.doi.org/10.1017/S0960129504004311},
partner = {PISA, ULEICES},
}
|
