29 citations · 81 across the 19 of their papers we have counts for
13 papers · 1 filter
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-proce…
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
Nicolas Amat, Silvano Dal Zilio
SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checki…
Property Directed Reachability for Generalized Petri Nets
Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa
We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method.…
Accelerating the Computation of Dead and Concurrent Places using Reductions
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
We propose a new method for accelerating the computation of a concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on a…
Checking marking reachability with the state equation in Petri net subclasses
Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio +1
Although decidable, the marking reachability problem for Petri nets is well-known to be intractable in general, and a non-elementary lower bound has been recently uncovered. In ord…
MCC: a Tool for Unfolding Colored Petri Nets in PNML Format
Silvano Dal Zilio
MCC is a tool designed for a very specific task: to transform the models of High-Level Petri nets, given in the PNML syntax, into equivalent Place/Transition nets. The name of the…