© 2000 by British Computer Society
Modular Analysis of Petri Nets
1 Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000 ÅRHUS C, Denmark 2 LSV, CNRS UMR 8643, ENS de Cachan, 61 avenue du Pdt Wilson, F-94235 CACHAN Cedex, France Email: petrucci@lsv.ens-cachan.fr
This paper shows how two of the most important analysis methods for Petri nets can be performed in a modular way. We illustrate our techniques by means of modular Place/Transitions nets (modular PT-nets) in which the individual modules interact via shared places and shared transitions. For place invariants we show that it is possible to construct invariants of the total modular PT-net from invariants of the individual modules. For state spaces, we show that it is possible to decide behavioural properties of the modular PT-net from state spaces of the individual modules plus a synchronization graph, without unfolding to the ordinary state space. The generalization of our techniques to high-level Petri nets is rather straightforward.
Received 6 November, 1998. Revised 13 April, 2000.