The Complexity of Coverability in nu-Petri Nets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2016

The Complexity of Coverability in nu-Petri Nets

Résumé

We show that the coverability problem in nu-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 nu-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 (527.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : hal-01265302 , version 1

Citer

Ranko Lazić, Sylvain Schmitz. The Complexity of Coverability in nu-Petri Nets. 2016. ⟨hal-01265302v1⟩
249 Consultations
297 Téléchargements

Partager

Gmail Facebook X LinkedIn More