TCS / Research / Publications / Efficient Detection of Deadlocks in Petri Nets
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Efficient Detection of Deadlocks in Petri Nets


Kimmo Varpaaniemi. Efficient detection of deadlocks in Petri nets. Research Report A26, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, October 1993.


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.


reachability analysis, Petri nets, deadlocks, stubborn set method, sleep set method

Suggested BibTeX entry:

    address = {Espoo, Finland},
    author = {Kimmo Varpaaniemi},
    institution = {Helsinki University of Technology, Digital Systems Laboratory},
    month = {October},
    number = {A26},
    pages = {56},
    title = {Efficient Detection of Deadlocks in {P}etri Nets},
    type = {Research Report},
    year = {1993},

NOTE: Reprint of Licentiate's thesis; see URL below.
PostScript (624 kB)
GZipped PostScript (164 kB)
PDF (546 kB)
See ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.