Name
Abstract | ||
|---|---|---|
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 109 unsafe states. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1109/TAC.2015.2426232 | Automatic Control, IEEE Transactions |
Keywords | Field | DocType |
System recovery,Monitoring,Mathematical model,Scalability,Petri nets,Computational modeling,Boolean functions | Boolean function,Petri net,Optimal control,Computer science,Supervisory control,Deadlock,Boolean satisfiability problem,Theoretical computer science,Control logic,Deadlock prevention algorithms | Journal |
Volume | Issue | ISSN |
PP | 99 | 0018-9286 |
Citations | PageRank | References |
3 | 0.46 | 15 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jason Stanley | 1 | 39 | 3.48 |
| Hongwei Liao | 2 | 115 | 9.58 |
| StéPhane Lafortune | 3 | 1738 | 181.23 |