Model checking by exhaustive state space enumeration is one of the most developed analysis methods for distributed event systems.
Its main problem—the size of the state spaces—has been addressed by various reduction methods.
Complex systems tend to consist of loosely connected modules, which may perform internal tasks in parallel. The possible interleavings
of these parallel tasks easily leads to a large number of reachable global states. In modular state space analysis, the internal
actions are explored separately in each module, and the global state space only includes synchronisations.
This article introduces nested modular nets, which are hierarchal collections of nets synchronising via shared transitions,
and presents a simple algorithm for model checking safety properties in modular systems.
Keywords modular systems - state space enumeration - model checking - high-level nets
This research was supported by Jenny and Antti Wihuri Fund and by Academy of Finland (Project 47754).