Communication Dans Un Congrès
Année : 2020
Résumé
Downward closures of Petri net reachability sets can be finitely represented by their set of maximal elements called the minimal cover-ability set or Clover. Many properties (coverability, boundedness, ...) can be decided using Clover, in a time proportional to the size of Clover. So it is crucial to design algorithms that compute it efficiently. We present a simple modification of the original but incomplete Minimal Coverability Tree algorithm (MCT), computing Clover, which makes it complete: it memorizes accelerations and fires them as ordinary transitions. Contrary to the other alternative algorithms for which no bound on the size of the required additional memory is known, we establish that the additional space of our algorithm is at most doubly exponential. Furthermore we have implemented a prototype MinCov which is already very competitive: on benchmarks it uses less space than all the other tools and its execution time is close to the one of the fastest tool.
Origine | Fichiers produits par l'(les) auteur(s) |
---|
Loading...
igor khmelnitsky : Connectez-vous pour contacter le contributeur
https://inria.hal.science/hal-02479879
Soumis le : vendredi 14 février 2020-17:23:49
Dernière modification le : vendredi 17 mai 2024-16:22:03
Archivage à long terme le : vendredi 15 mai 2020-18:04:44
Dates et versions
- HAL Id : hal-02479879 , version 1
Citer
Alain Finkel, Serge Haddad, Igor Khmelnitsky. Minimal Coverability Tree Construction Made Complete and Efficient. FoSSaCS 2020 - 23rd International Conference on Foundations of Software Science and Computation Structures, Apr 2020, Dublin, Ireland. ⟨hal-02479879⟩
Collections
263
Consultations
357
Téléchargements