Modular State Space Analysis of Coloured Petri Nets

Abstract

State Space Analysis is one of the most developed analysis methods for Petri Nets. The main problem of state space analysis is the size of the state spaces. Several ways to reduce it have been proposed but cannot yet handle industrial size systems.

Large models often consist of a set of modules. Local properties of each module can be checked separately, before checking the validity of the entire system. We want to avoid the construction of a single state space of the entire system.

When considering transition sharing, the behaviour of the total system can be capture by the state spaces of modules combined with a Synchronisation Graph. To verify that we do not lose information we show how the full state space can be conctructed.

We show how it is possible to determine usual Petri Nets properites, without unfolding to the ordinary state space.