Open AccessModular State Space Analysis of Coloured Petri Nets
Author(s) -
Søren Christensen,
Laure Petrucci
Publication year - 1997
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v26i524.7053
Subject(s) - petri net , state space , modular design , state (computer science) , graph , space (punctuation) , theoretical computer science , stochastic petri net , mathematics , computer science , discrete mathematics , algorithm , topology (electrical circuits) , combinatorics , programming language , operating system , statistics
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.