Modularity and Petri Nets

The systems to model are nowadays very large. Their specification is often decomposed into several steps. This leads to modularly or incrementally designed models. Petri nets analysis is generally achieved via state space analysis, which is often impossible to perform due to the so-called state space explosion problem. Several methods allow to reduce the occurrence graph size, e.g. using partial orders, symmetries, ... Here, we focus on techniques which take advantage of the modular design of the system, and hence build the state space in a modular or incremental way