Skip to Main content Skip to Navigation
New interface
Conference papers

The Complexity of Coverability in ν-Petri Nets

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 metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Sylvain Schmitz Connect in order to contact the contributor
Submitted on : Thursday, May 12, 2016 - 10:35:37 AM
Last modification on : Saturday, June 25, 2022 - 7:44:58 PM
Long-term archiving on: : Wednesday, November 16, 2016 - 2:27:36 AM


Files produced by the author(s)



Ranko Lazić, Sylvain Schmitz. The Complexity of Coverability in ν-Petri Nets. LICS 2016 - 31th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2016, New York, United States. pp.467--476, ⟨10.1145/2933575.2933593⟩. ⟨hal-01265302v2⟩



Record views


Files downloads