Selected publications at LSV

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.

   address = {New York City, USA},
   author = {Ranko Lazi{\'c} and Sylvain Schmitz},
   booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
   DOI = {10.1145/2933575.2933593},
   editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
   month = jul,
   pages = {467-476},
   publisher = {ACM Press},
   title = {The Complexity of Coverability in {{\(\nu\)}}-{P}etri Nets},
   url = {},
   year = {2016},

About LSV

Select by Year