We propose an automated procedure to prove polyhedral abstractions for Petri nets. Polyhedral abstraction is a new type of state-space equivalence based on the use of linear integer constraints. Our approach relies on an encoding 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 that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.

翻译：我们提出了一种自动化的过程，用于证明佩特里网的多面体抽象。多面体抽象是一种基于线性整数约束的新型状态空间等价关系。我们的方法依赖于将问题编码为一组SMT公式，这些公式的可满足性即蕴含等价关系成立。在此背景下，难点在于需要处理无限状态系统。为完备性起见，我们利用了与一类具有Presburger可定义可达集佩特里网的关联性。我们已实现了该过程，并通过多个示例展示了其应用。