In: Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (ICATPN 2003), Eindhoven, The Netherlands, June 23-27, 2003, pages 201-220. Volume 2679 of Lecture Notes in Computer Science / Wil M. P. van der Aalst and Eike Best (Eds.) --- Springer-Verlag, June 2003.
Abstract: 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.