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.

翻译：本文提出了一种自动化证明Petri网多面体抽象（亦称多面体归约）的方法。多面体抽象是一种基于位置标识间线性整数约束的新型Petri网状态空间等价关系。除定义自动化证明方法外，本文旨在更精确刻画多面体归约的特征，并综述其在可达性问题中的应用。我们的方法将等价性问题编码为一组SMT公式，其可满足性意味着等价关系成立。此处的难点在于需要处理无限状态系统。为达成完备性，我们利用了一类具有Presburger可定义可达集的Petri网（称为平坦网）的性质。我们已实现该自动化流程，并通过多个案例演示其应用。