LTL可满足性与模型检查：焦点博弈新视角

"这篇论文探讨了焦点博弈在解决线性时间时序逻辑（LTL）的可满足性和模型检查问题中的应用。焦点博弈提供了一种博弈论的框架，其中一个玩家，利用焦点策略，来展示时间算子的特性。文章介绍了满足LTL公式的焦点博弈的定义，这些博弈中的策略具有明确的位置性，且能产生更小的模型。此外，还讨论了焦点博弈在LTL模型检测中的应用。关键词包括验证、时态逻辑和工具支持。" 在计算机科学的验证领域，逻辑扮演着至关重要的角色，因为它可以用来表述系统的正确性属性。线性时间时序逻辑（LTL）是一种广泛应用的时态逻辑，用于描述系统的动态行为和时间相关的性质。LTL的满足性和模型检查问题是验证的关键组成部分，它们有助于确定给定的系统是否满足指定的LTL公式。 焦点博弈在此背景下提出，它是一种特殊类型的博弈，其中两个玩家（通常称为Player 0 和 Player 1）根据LTL公式的语义进行互动。Player 0（通常是验证者）试图证明公式是不可满足的，而Player 1（系统的行为）则尝试反驳。在焦点博弈中，Player 0 被赋予一种特殊策略——“焦点”，能够突出关键的时间算子。Player 0 的策略不再局限于位置性，而是基于优先级公式列表，这使得他们能够更有效地展示公式无法满足的原因。 这篇论文的贡献在于定义了LTL的焦点博弈，其中Player 0 的策略变得位置性微不足道，这意味着它们更容易理解并且能导致更小的反例模型。这简化了游戏结构，使得分析过程更为高效。同时，作者还介绍了如何使用焦点博弈进行LTL模型检测，即检查给定系统是否满足特定的LTL公式。 焦点博弈的这种特性对于验证工具来说非常有价值，因为它们不仅能够告知用户公式是否满足，还能提供解释为何不满足的详细策略。这种透明度有助于用户理解系统的缺陷，从而改进设计。论文引用了多种已有的LTL决策程序，如表格法、分辨率、约简、自动机理论和符号方法，表明焦点博弈是现有方法的一个补充。 这篇论文深入研究了焦点博弈在LTL可满足性和模型检查中的应用，为验证技术提供了新的视角，有助于提高验证效率和用户体验。通过将复杂的逻辑问题转化为直观的游戏形式，焦点博弈为理解和解决系统正确性问题提供了一个实用的工具。