关于保持 stutter 的部分序归约中不一致标记问题的详细剖析
计算机科学中的逻辑
2023-06-22 v3
摘要
模型检测中最流行的状态空间归约技术之一是部分序归约（POR）。在众多不同的 POR 实现中，顽固集是一种非常通用的变体，因此在过去 32 年中看到了许多不同的应用。早期顽固集工作之一展示了如何增强基本的归约条件以保留 stutter-trace 等价性，使顽固集适用于线性时间性质的模型检测。在本文中，我们指出了推理中的一个缺陷，并通过反例表明 stutter-trace 等价性不一定被保留。我们提出了一个更强的归约条件，并提供了广泛的新正确性证明以确保该问题得到解决。此外，我们分析了该问题可能在哪些形式化中出现。对实际实现的影响有限，因为它们都计算了该理论的一个正确近似。
引用
@article{arxiv.2012.15704,
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= {arXiv preprint arXiv:2012.15704},
year = {2023}
}
备注
arXiv admin note: substantial text overlap with arXiv:1910.09829