Deadlock Detection with Stubborn Unfoldings

H. Wang and U. Buy (USA)


Formal methods; Verification and validation; Petri nets; Deadlock detection; Stubborn sets; Unfolding.


Stubborn sets and model unfolding are two well-known methods for sidestepping the complexity of state-space ex ploration based on formal models of concurrent programs, such as Labeled Transition Systems and Petri nets. Here we define a deadlock detection strategy that combines these two methods. We also show that the resulting method, stub born unfoldings, can produce smaller state space represen tations than both previous methods.

Important Links:

Go Back