For the most recent entries see the Petri Nets Newsletter.

On Combining the Subborn Set Method with the Sleep Set Method.

Varpaaniemi, K.

In: Valette, R.: Lecture Notes in Computer Science, Vol. 815; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain, pages 548-567. Springer-Verlag, 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. The paper shows that at east 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


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography