论文标题
详细说明了放置局部订购的标签问题不一致的问题
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
论文作者
论文摘要
模型检查最流行的状态空间降低技术之一是部分订购（POR）。在许多不同的POR实施中，顽固的集合是一种非常通用的变体，因此在过去的32年中已经看到了许多不同的应用。早期顽固的套件作品之一表明，如何增加减少基本条件以保持口吃 - 跟踪等效性，使顽固的集合适合于模型检查线性时间属性。在本文中，我们确定了推理中的缺陷，并以反示例表明口吃 - 迹象等效性不一定得到保留。我们提出更强的减少条件，并提供广泛的新正确性证明，以确保解决问题。此外，我们分析可能出现形式主义的形式主义。对实际实施的影响是有限的，因为它们都计算出理论的正确近似值。
One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many different applications over the past 32 years. One of the early stubborn sets works shows how the basic conditions for reduction can be augmented to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a stronger reduction condition and provide extensive new correctness proofs to ensure the issue is resolved. Furthermore, we analyse in which formalisms the problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory.
