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.

翻译：我们提出了一种检验Petri网广义可达性属性的方法，该方法利用结构约简技术，并可作为现有模型检测器的透明预处理步骤。该方法的理论基础在于一种新型过程：它能将关于原始Petri网的属性投影为仅涉及约简后等价网路的公式。该投影过程被定义为线性整数算术中的变量消去程序，专门针对我们所处理的特定约束类型而设计。该方法具有线性复杂度，能保证返回可靠属性，并利用简单条件检测结果是否精确。实验结果表明，该方法在实践中表现优异，即便在约简程度有限的情况下仍具有实用价值。