Commodification of accelerations for the Karp and Miller Construction. - Université Paris-Saclay Accéder directement au contenu
Article Dans Une Revue Discrete Event Dynamic Systems Année : 2021

Commodification of accelerations for the Karp and Miller Construction.

Résumé

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 omega-markings representing (potentially infinite) coverability sets. This set of omega-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 omega-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.
Fichier principal
Vignette du fichier
JDEDS.pdf (421.93 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03137054 , version 1 (10-02-2021)

Identifiants

  • HAL Id : hal-03137054 , version 1

Citer

Alain Finkel, Serge Haddad, Igor Khmelnitsky. Commodification of accelerations for the Karp and Miller Construction.. Discrete Event Dynamic Systems, 2021, 31 (2), pp.251-270. ⟨hal-03137054⟩
151 Consultations
273 Téléchargements

Partager

Gmail Facebook X LinkedIn More