Petri net reactive modules
Abbreviated Journal Title
Theor. Comput. Sci.
reactive system; Petri net; process semantics; replacement; structural; transformation; MODEL CHECKING; Computer Science, Theory & Methods
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. (C) 2006 Elsevier B.V. All rights reserved.
Theoretical Computer Science
"Petri net reactive modules" (2006). Faculty Bibliography 2000s. 6648.