ω-正则模型检验：状态计算与循环检测的挑战与解决方案

"这篇论文探讨了ω-正则模型检验中的状态计算与循环检测问题，主要关注在有限或无限词上的活性属性验证。作者Ahmed Bouajjani、Axel Legay和Pierre Wolper讨论了如何在无界配置的无限计算中处理循环检测的挑战，同时提供实验结果证明了所提出方法的有效性。该研究强调了模型检查不仅是状态可达性的问题，还涉及到线性时间属性的验证，特别是那些涉及活性成分的属性。" 在ω-正则模型检验领域，传统的研究主要集中在状态可达性和安全性验证上。然而，对于那些涉及活性属性的验证，即需要检查系统是否可以反复进入某个状态或状态集合，情况则更为复杂。论文指出，尽管活性属性的检验也可以在这个框架内进行，但相关的方法细节和技术评估相对较少。 文章的核心在于如何在有限或无限词的背景下计算状态，并解决循环检测的问题。由于无界配置可能导致无限计算路径且不重复，这使得循环检测变得困难。作者提出了新的方法来精确计算在不同情况下的系统结构，并有效地处理由于配置无限性带来的挑战。 为了证明这种方法的实用性，作者进行了多个实验，结果显示这种方法能够成功应用于活性属性的模型检查。此外，他们还提到了常规模型检查的加速技术，这些技术虽然不能在所有情况下提供完全准确的结果，但在很多实际场景中可以得到正则表示或近似的可达状态，尤其是在处理无限状态系统时。 论文进一步指出，对于安全属性，模型检查可以直接转化为状态可达性问题。但对于包含活性属性的线性时间逻辑（如Büchi自动机），模型检查则需要检查重复可达性。作者引用了相关工作，如[3, 16]，这些工作展示了如何将模型检查问题转换为Büchi自动机的目标。 这篇论文为ω-正则模型检验提供了深入的理解，特别是在处理活性属性和循环检测方面，为无限状态系统的分析提供了新的见解和实用的技术。这些研究对于软件验证、形式化方法和并发系统分析等领域具有重要的理论和实践意义。