Title
New algorithms for deciding the siphon-trap property
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 Oanea1846.87
Harro Wimmel211411.56
Karsten Wolf375742.53