@phdthesis{
    Vrp93a,
    author = "Varpaaniemi, Kimmo",
    ps = "lic.ps",
    school = "Department of Computer Science, Helsinki University of Technology",
    title = "{E}fficient Detection of Deadlocks in {P}etri Nets",
    abstract = "Reachability analysis (exhaustive simulation, state space generation) 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 even if finite. This thesis 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. All of these methods guarantee that all reachable terminal states are found if the complete state space is finite. \par Petri nets are a widely used model for concurrent and distributed systems. This thesis 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. \par 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. \par This thesis 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.",
    address = "Espoo, Finland",
    month = "September",
    flags = "public,copy,LICTHESIS",
    year = "1993",
    keywords = "reachability analysis, Petri nets, deadlocks, stubborn set method, sleep set method",
    pdf = "lic.pdf",
    type = "{L}icentiate's thesis",
    pages = "63"
}