Evènement pour le groupe Séminaire Méthodes Formelles

Date 2016-03-08  11:00-12:00
TitreThe 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. Joint work with Ranko Lazic, preprint available from https://hal.inria.fr/hal-01265302. 
OrateurSylvain Schmitz 
UrlLSV - ENS Cachan 

Aucun document lié à cet événement.

Retour à l'index