  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-processing step of existing model-checkers. Our
approach is based on a new procedure that can project a property, about an
initial Petri net, into an equivalent formula that only refers to the reduced
version of this net. Our projection is defined as a variable elimination
procedure for linear integer arithmetic tailored to the specific kind of
constraints we handle. It has linear complexity, is guaranteed to return a
sound property, and makes use of a simple condition to detect when the result
is exact. Experimental results show that our approach works well in practice
and that it can be useful even when there is only a limited amount of
reductions.
