Title: On Combining the Stubborn Set Method with the Sleep Set Method

Appears in: Valette, R. (Ed.), Proceedings of the 15th International Conference on Application and Theory of Petri Nets, Zaragoza, Spain, June 1994. Lecture Notes in Computer Science 815, Springer-Verlag, Berlin 1994.

Pages: 548-567

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.

Topics: system verification using nets, analysis and behaviour of nets