Skip to Main content Skip to Navigation
Conference papers

Minimal Coverability Tree Construction Made Complete and Efficient

Alain Finkel 1 Serge Haddad 2, 1 Igor Khmelnitsky 2, 1
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Igor Khmelnitsky Connect in order to contact the contributor
Submitted on : Friday, February 14, 2020 - 5:23:49 PM
Last modification on : Tuesday, January 4, 2022 - 6:35:47 AM
Long-term archiving on: : Friday, May 15, 2020 - 6:04:44 PM


Files produced by the author(s)


  • HAL Id : hal-02479879, version 1


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⟩



Les métriques sont temporairement indisponibles