Abstract | ||
---|---|---|
The siphon-trap property, also known as Commoner-Hack property, establishes a relation between structural entities within a Petri net – the eponymous siphons and traps. The property is linked to the behavior of a Petri net, for instance to deadlock freedom and liveness of the net. It is nevertheless nontrivial to decide the property as a net can have exponentially many siphons and traps even if only minimal siphons are considered. Consequently, the value of the property depends on the availability of powerful decision procedures. We contribute to this issue by proposing two new methods for deciding the siphon-trap property. One is a plain translation of the property into a Boolean satisfiability (SAT) problem, which exploits the fact that incredibly powerful SAT solvers are available. The second procedure has a divide-and-conquer nature which builds upon a decomposition of a Petri net into open nets and projects information about siphons and traps onto the interfaces of the components. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1007/978-3-642-13675-7_16 | Petri Nets |
Keywords | Field | DocType |
powerful sat solvers,powerful decision procedure,boolean satisfiability,siphon-trap property,commoner-hack property,minimal siphon,new algorithm,new method,divide-and-conquer nature,open net,eponymous siphon,petri net,sat solver,divide and conquer | Discrete mathematics,Petri net,Siphon,Computer science,Boolean satisfiability problem,Deadlock,Algorithm,Exploit,Theoretical computer science,Divide and conquer algorithms,Liveness | Conference |
Volume | ISSN | ISBN |
6128 | 0302-9743 | 3-642-13674-5 |
Citations | PageRank | References |
8 | 0.47 | 3 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Olivia Oanea | 1 | 84 | 6.87 |
Harro Wimmel | 2 | 114 | 11.56 |
Karsten Wolf | 3 | 757 | 42.53 |