We propose an automated procedure to prove polyhedral abstractions 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可定义的可达性集合。我们实现了该流程，并通过多个示例展示了其应用。