We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space abstraction, called polyhedral abstraction, which involves a combination between structural reductions and sets of linear arithmetic constraints between the marking of places. We propose a new data-structure, called a Token Flow Graph (TFG), that captures the particular structure of constraints occurring in polyhedral abstractions. We leverage TFGs to efficiently solve two reachability problems: first to check the reachability of a given marking; then to compute the concurrency relation of a net, that is all pairs of places that can be marked together in some reachable marking. Our algorithms are implemented in a tool, called Kong, that we evaluate on a large collection of models used during the 2020 edition of the Model Checking Contest. Our experiments show that the approach works well, even when a moderate amount of reductions applies.

翻译：我们提出了一种新方法，利用结构归约加速Petri网可达性属性的验证。该方法依赖于一种称为多面体抽象的状态空间抽象技术，该技术结合了结构归约与库所标识间的线性算术约束集合。我们提出了一种名为令牌流图(TFG)的新型数据结构，用于捕获多面体抽象中约束的特定结构。我们利用TFG高效解决两个可达性问题：首先检查给定标识的可达性；其次计算网的并发关系，即所有可在某个可达标识中同时被标识的库所对。我们的算法在名为Kong的工具中实现，并在2020年模型检测竞赛中使用的大规模模型集合上进行了评估。实验表明，即使仅应用中等程度的归约，该方法仍能取得良好效果。