Model checking safety properties in modular high-level nets

Reference:

Marko Mäkelä. Model checking safety properties in modular high-level nets. In Wil M.P. van der Aalst and Eike Best, editors, Application and Theory of Petri Nets 2003: 24^th International Conference, ICATPN 2003, number 2679 in Lecture Notes in Computer Science, pages 201–220, Eindhoven, The Netherlands, June 2003. Springer-Verlag, Berlin, Germany.

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

Suggested BibTeX entry:

@inproceedings{MakelaMarko-Makela:modular,
    address = {Eindhoven, The Netherlands},
    author = {Marko M{\"a}kel{\"a}},
    booktitle = {Application and Theory of Petri Nets 2003: 24\textsuperscript{th} International Conference, ICATPN 2003},
    editor = {Wil M.P. van der Aalst and Eike Best},
    month = {June},
    number = {2679},
    pages = {201--220},
    publisher = {Springer-Verlag, Berlin, Germany},
    series = {Lecture Notes in Computer Science},
    title = {Model checking safety properties in modular high-level nets},
    year = {2003},
}