In: 94, Warsaw: H.-D. Burkhard, L. Czaja & P.H. Starke (Eds.), Concurrency, Specification and Programming: Proceedings of the CS&P'93 Workshop,Nieborow near Warsaw, Poland, 14-16 October 1993, Zaklad Graficzny UW, zam. 261, pages 230-246. 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. What makes deadlocks especially interesting is the fact that the verification of a safety property can often be reduced to deadlock detection. The considered methods utilize the independence of transitions to cut down on the number of states inspected during the search. These methods have been combined by Godefroid, Pirottin, and Wolper to further reduce the number of inspected states.
Petri nets are a widely used model for concurrent and distributed systems. This paper shows that the stubborn set method and the sleep set method can be combined without any of the assumptions previously placed on the stubborn sets as far as the detection of reachable terminal states in place/transition nets, a class of Petri nets, is concerned. The obtained result is actually more general and 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.
This paper emphasizes the value of dynamically stubborn sets as a useful generalization of stubborn sets and presents some results that improve the understanding of the stubborn set method.
Keywords: reachability analysis; Petri nets; deadlocks; stubborn set method; sleep set method.