The Complexity of Coverability in ν-Petri Nets

Ranko Lazić 1, 2 Sylvain Schmitz 3, 4
3 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We show that the coverability problem in ν-Petri nets is complete for 'double Ackermann' time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes ν-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals.
Document type :
Conference papers
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-01265302
Contributor : Sylvain Schmitz <>
Submitted on : Thursday, May 12, 2016 - 10:35:37 AM
Last modification on : Thursday, February 7, 2019 - 5:29:22 PM
Long-term archiving on : Wednesday, November 16, 2016 - 2:27:36 AM

File

sigplanconf.pdf
Files produced by the author(s)

Identifiers

Citation

Ranko Lazić, Sylvain Schmitz. The Complexity of Coverability in ν-Petri Nets. LICS 2016, 2016, New York, United States. pp.467--476, ⟨10.1145/2933575.2933593⟩. ⟨hal-01265302v2⟩

Share

Metrics

Record views

371

Files downloads

237