Efficient Detection of Deadlocks in Petri Nets

摘要

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. The 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. 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. 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.