Name
Abstract | ||
|---|---|---|
Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We present a direct, DBM-based algorithm for forward reachability analysis of bounded TAPNs extended with transport arcs, inhibitor arcs and age invariants. We also give a complete proof of its correctness, including reduction techniques based on symmetries and extrapolation. Finally, we augment the algorithm with a novel state-space reduction technique introducing a monotonic ordering on markings and prove its soundness even in the presence of monotonicity-breaking features like age invariants and inhibitor arcs. We implement the algorithm within the model-checker TAPAAL and the experimental results document an encouraging performance compared to verification approaches that translate TAPN models to UPPAAL timed automata. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.4204/EPTCS.102.12 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
Keywords | Field | DocType |
reachability,model checking,verification | Discrete mathematics,Petri net,Model checking,Computer science,Automaton,Algorithm,Stochastic Petri net,Reachability,Invariant (mathematics),Soundness,Bounded function | Journal |
Issue | ISSN | Citations |
102 | 2075-2180 | 3 |
PageRank | References | Authors |
0.47 | 17 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexandre David | 1 | 1667 | 76.52 |
| Lasse Jacobsen | 2 | 31 | 2.99 |
| Morten Jacobsen | 3 | 31 | 2.99 |
| Jirí Srba | 4 | 252 | 28.68 |