SAT-Based Control of Concurrent Software for Deadlock Avoidance
Jason Stanley, Hongwei Liao, Stéphane Lafortune · IEEE Transactions on Automatic Control · 2015
We present a highly efficient boolean satisfiability (SAT) formulation for deadlock detection and avoidance in concurrent programs modeled by Gadara nets, a class of Petri nets. The SAT formulation is used in an optimal control synthesis framework based on Discrete Control Theory. We compare our method with existing methods and show a significant increase in scalability. Stress tests show that our technique is capable of synthesizing deadlock avoidance control logic in programs modeled by Gadara nets with over 109unsafe states.