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.
Type de document :
Communication dans un congrès
LICS 2016, 2016, New York, United States. ACM Press, pp.467--476, <10.1145/2933575.2933593>
Liste complète des métadonnées


https://hal.inria.fr/hal-01265302
Contributeur : Sylvain Schmitz <>
Soumis le : jeudi 12 mai 2016 - 10:35:37
Dernière modification le : samedi 18 février 2017 - 01:14:36
Document(s) archivé(s) le : mercredi 16 novembre 2016 - 02:27:36

Fichier

sigplanconf.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

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

Partager

Métriques

Consultations de
la notice

228

Téléchargements du document

87