A Hybrid Approach to Detecting Deadlock in STGs Unfoldings Using SAT

Abstract

Deadlock problem is often seen as one which consists of two parts: the detection, and the elimination of them. A number of techniques for solving the deadlock problem exist. Some of these methods operate directly on the STG level, but they restrict the class of the underlying Petri nets to only, marked graphs. While this purely state-based approach is relatively simple and well-studied, the issue of computational complexity for highly concurrent STGs is a serious one due to the state space explosion problem. To alleviate this problem, we chose to use methods that do not explicitly enumerate the input sequences, thus avoiding the state space explosion. Using a novel formulation of deadlock with some problem-specific optimization rules on Petri net unfoldings, we proposed a hybrid approach to detecting deadlock in asynchronous circuits. Experiment shows that the technique seems quite competitive on the example benchmark models available to us.