A distributed state space for modular Petri nets

This paper deals with the modular verification of modular Petri nets. We propose a new modular structure of the state space of a given modular Petri. Such a structure associates a graph with each module of the system allowing to describe the module behaviours and some global information. Thanks to the modularity of the proposed structure, the explosion problem of the state space is attenuated. Further, the proposed structure allows to limit the verification of some generic properties that concern one module to the exploration of its associated graph.