On Combining the Stubborn Set Method with the Sleep Set Method

Reference:

Kimmo Varpaaniemi. On combining the stubborn set method with the sleep set method. In Robert Valette, editor, Application and Theory of Petri Nets 1994: 15th International Conference, Zaragoza, Spain, June 20–24, 1994, Proceedings, volume 815 of Lecture Notes in Computer Science, pages 548–567. Springer-Verlag, Berlin, Germany, 1994. © Springer-Verlag Berlin Heidelberg 1994.

Abstract:

Reachability analysis is a powerful formal method for analysis of concurrent and distributed finite state systems. It suffers from the state space explosion problem, however: the state space of a system can be far too large to be completely generated. This paper considers two promising methods, Valmari's stubborn set method and Godefroid's sleep set method, to avoid generating all of the state space when searching for undesirable reachable terminal states, also called deadlocks. These methods have been combined by Godefroid, Pirottin, and Wolper to further reduce the number of inspected states. However, the combination presented by them places assumptions on the stubborn sets used. This paper shows that at least in place/transition nets, the stubborn set method can be combined with the sleep set method in such a way that all reachable terminal states are found, without having to place any assumption on the stubborn sets used. This result is shown by showing a more general result which gives a sufficient condition for a method to be compatible with the sleep set method in the detection of reachable terminal states in place/transition nets.

Keywords:

place/transition nets, reachability analysis, deadlock detection, stubborn set method, sleep set method

Suggested BibTeX entry:

@inproceedings{VarpaaniemiKimmo-Vrp94b,
    author = {Kimmo Varpaaniemi},
    booktitle = {{A}pplication and Theory of {P}etri Nets 1994: 15th International Conference, {Z}aragoza, {S}pain, {J}une 20--24, 1994, Proceedings},
    editor = {Robert Valette},
    note = {© Springer-Verlag Berlin Heidelberg 1994},
    pages = {548--567},
    publisher = {Springer-Verlag, Berlin, Germany},
    series = {Lecture Notes in Computer Science},
    title = {{O}n Combining the Stubborn Set Method with the Sleep Set Method},
    volume = {815},
    year = {1994},
}