Helsinki University of Technology, Digital Systems Laboratory, Research Report A26, 56 pages, October 1993.
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 report 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 report 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.
The number of enabled transitions in a stubborn set can drastically affect the number of states inspected by the stubborn set method during the search for reachable terminal states. This work presents some heuristics for relieving the problem.
This report emphasizes the value of dynamically stubborn sets as a useful generalization of stubborn sets and shows some results that improve the understanding of the stubborn set method.
Keywords: reachability analysis; Petri nets; deadlocks; stubbornset method; sleep set method.