Modular analysis of Petri nets

This paper shows how two of the most important analysis methods for Petri n ets can be performed in a modular way. We illustrate our techniques by mean s of modular Place/Transitions nets (modular PT-nets) in which the individu al modules interact via shared places and shared transitions. For place inv ariants we show that it is possible to construct invariants of the total mo dular PT-net from invariants of the individual modules. For state spaces, w e show that it is possible to deride behavioural properties of the modular PT-net from state spaces of the individual modules plus a synchronization g raph, without unfolding to the ordinary state space. The generalization of our techniques to high-level Petri nets is rather straightforward.