We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.

翻译：我们提出了一种自动化的程序，用于证明佩特里网的多面体抽象（也称为多面体化简）。多面体抽象是一种基于位置标识间线性整数约束的新型佩特里网状态空间等价关系。除了定义自动化证明方法，本文旨在进一步刻画多面体化简的特征，并概述其在可达性问题中的应用。我们的方法将等价问题编码为一组满意性可证明等价成立的SMT公式。在此背景下，难点源于需要处理无限状态系统。为完备性起见，我们利用了与一类称为扁平网的佩特里网的联系，其可达集是Presburger可定义的。我们实现了该程序，并通过多个示例展示了其应用。