The Complexity of Coverability in ν-Petri Nets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

The Complexity of Coverability in ν-Petri Nets

Résumé

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.
Fichier principal
Vignette du fichier
sigplanconf.pdf (530.38 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01265302 , version 1 (31-01-2016)
hal-01265302 , version 2 (12-05-2016)

Identifiants

Citer

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⟩
249 Consultations
295 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More