关于保持停顿的偏序归约中不一致标记问题的详细说明
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
AI总结：
本文指出保持停顿的偏序归约中一个不一致标记问题，通过反例证明原有条件不充分，提出更强归约条件并给出新正确性证明，分析问题出现的形式化体系。
摘要：
模型检查中最流行的状态空间归约技术之一是偏序归约（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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
