关于保留口吃的部分序约简中标记不一致问题的详细说明
摘要：模型检测中最常用的状态空间缩减技术之一是部分顺序缩减（Partial-Order Reduction, POR）。在众多不同的POR实现中，顽固集（stubborn sets）是一种非常多才多艺的变种，因此在过去32年中已经有许多不同的应用。早期的顽固集工作之一展示了如何通过扩展基本缩减条件来保持 stutter-trace 等价（stutter-trace equivalence），使得顽固集适用于线性时序性质的模型检测。本文中，我们确定了推理中的一个缺陷，并通过反例证明 stutter-trace 等价不一定得到保持。我们提出了一个更强的缩减条件，并提供了广泛的新正确性证明以确保问题得到解决。此外，我们分析了在哪些形式主义中可能出现该问题。对于实际实现的影响有限，因为它们都计算了该理论的正确近似。
作者：Thomas Neele, Antti Valmari, Tim A. C. Willemse
论文ID：2012.15704
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22