Commodification of accelerations for the Karp and Miller Construction
- PDF / 1,720,992 Bytes
- 20 Pages / 439.642 x 666.49 pts Page_size
- 23 Downloads / 209 Views
Commodification of accelerations for the Karp and Miller Construction Alain Finkel1,2 · Serge Haddad3 · Igor Khmelnitsky3 Received: 2 March 2020 / Accepted: 12 October 2020 / © Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Karp and Miller’s algorithm is based on an exploration of the reachability tree of a Petri net where, the sequences of transitions with positive incidence are accelerated. The tree nodes of Karp and Miller are labeled with ω-markings representing (potentially infinite) coverability sets. This set of ω-markings allows us to decide several properties of the Petri net, such as whether a marking is coverable or whether the reachability set is finite. The edges of the Karp and Miller tree are labeled by transitions but the associated semantic is unclear which yields to a complex proof of the algorithm correctness. In this work we introduce three concepts: abstraction, acceleration and exploration sequence. In particular, we generalize the definition of transitions to ω-transitions in order to represent accelerations by such transitions. The notion of abstraction makes it possible to greatly simplify the proof of the correctness. On the other hand, for an additional cost in memory, which we theoretically evaluated, we propose an “accelerated” variant of the Karp and Miller algorithm with an expected gain in execution time. Based on a similar idea we have accelerated (and made complete) the minimal coverability graph construction, implemented it in a tool and performed numerous promising benchmarks issued from realistic case studies and from a random generator of Petri nets. Keywords Petri nets · Coverability · Verification tool
This article belongs to the Topical Collection: Topical Collection on Recent Trends in Reactive Systems Guest Editor: Sebastian Lahaye Igor Khmelnitsky
[email protected] Alain Finkel [email protected] Serge Haddad [email protected] 1
ENS Paris-Saclay, LSV, Universit´e Paris-Saclay, Cachan, France
2
Institut Universitaire de France, Paris, France
3
INRIA, ENS Paris-Saclay, LSV, Universit´e Paris-Saclay, Cachan, France
Discrete Event Dynamic Systems
1 Introduction Coverability and Karp and Miller’s algorithm The coverability set (also denoted as Cover) of a Petri net with an initial marking is the downward closure (for the usual order on integer vectors) of the set of reachable markings. An effective finite representation of the cover makes it possible to decide several problems such as: Can a given marking be covered by an reachable marking (the coverability problem)? Is the set of reachable markings finite? Which places are unbounded? In 1969, Karp and Miller showed that a finite representation of the coverability set of Petri nets and vector addition systems is computable by an algorithm constructing a finite tree (KMT) (Karp and Miller 1969) whose finite set of vertex labels (ω-markings) C represents the cover. Specifically, the downward closure (in NP ) of C, denoted ↓C, coincides with the cover. The set C is not unique because it depends on
Data Loading...
