一句话：本文指出保持 stutter 的偏序归约早期 stubborn sets 条件存在错误，给出反例并提出更强条件与正确性证明。
偏序归约（POR）是模型检测中常用的状态空间约简技术，其中 stubborn sets 是一种通用变体。早期工作通过增强基本条件，声称可使 stubborn sets 保持 stutter-trace equivalence，从而适用于线性时序性质模型检测。本文重新审视该论证，指出其推理存在缺陷，并用反例表明原条件并不一定保持 stutter-trace equivalence。作者随后提出更强的归约条件，给出详尽的正确性证明以消除该问题，并分析该缺陷可能在哪些形式化框架中出现。最后讨论了实际实现的影响：由于现有实现通常计算的是理论条件的正确近似，因此对工具实践影响有限。
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.
@article{paperbot1295,
title = {A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction},
author = {Thomas Neele and Antti Valmari and Tim A. C. Willemse},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:8)2021}
}