@inproceedings{
    Vrp94b,
    editor = "Valette, Robert",
    author = "Varpaaniemi, Kimmo",
    publisher = "Springer-Verlag, Berlin, Germany",
    note = "© Springer-Verlag Berlin Heidelberg 1994",
    title = "{O}n Combining the Stubborn Set Method with the Sleep Set Method",
    url = "http://users.tkk.fi/~kvarpaan/info/Vrp94b.html",
    series = "Lecture Notes in Computer Science",
    booktitle = "{A}pplication and Theory of {P}etri Nets 1994: 15th International Conference, {Z}aragoza, {S}pain, {J}une 20--24, 1994, Proceedings",
    errata = "http://users.tkk.fi/~kvarpaan/kvapn94e.html",
    volume = "815",
    flags = "public",
    pages = "548--567",
    year = "1994",
    keywords = "place/transition nets, reachability analysis, deadlock detection, stubborn set method, sleep set method",
    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."
}