  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. We actually define three different versions, that
vary depending on the method used for abstracting possible witnesses, and that
are able to handle problems of increasing difficulty. We have implemented our
methods in a model-checker called SMPT and give empirical evidences that our
approach can handle problems that are difficult or impossible to check with
current state of the art tools.

Logic in Computer Science