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

https://hal.inria.fr/hal-02479879
Contributor : Igor Khmelnitsky <>
Submitted on : Friday, February 14, 2020 - 5:23:49 PM
Last modification on : Friday, April 30, 2021 - 10:05:17 AM
Long-term archiving on: : Friday, May 15, 2020 - 6:04:44 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02479879, version 1

Citation

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⟩

Share

Metrics

Record views

195

Files downloads

727