Petri Net Reactive Modules

In this paper we model (discrete) reactive systems that may interact with each other by Petri net reactive modules (modules, for short) which are classical Petri nets together with a distinguished subset of interface places. We consider then an asynchronous composition operation of modules and, closely related to it, a decomposition operation. We show that any process (concurrent execution) of a composition of two modules can be decomposed into processes of shifted components for which a p-composition function exists, and vice versa. Based on this result, a compositional semantics of modules is then defined. Applications of process decomposition to replacement techniques of Petri nets and in proving correctness of Petri net structural transformations, are further discussed. © 2006 Elsevier B.V. All rights reserved