基于LTL求解器的合成规范分解再探讨
摘要：反应合成规范的分解问题已经提出了几种算法。受Antonio Iannopollo（2018）的方法启发，他设计了所谓的（DC）算法。我们在这里提出了我们的解决方案，进一步采用了他的思想，并提供了DC策略的数学形式化。我们对算法中涉及的主要概念进行严格定义，解释了技术，并通过示例演示其应用。DC的核心技术基于利用模型检查器的能力和效率来检测线性时态逻辑公式中的独立变量。尽管DC算法是正确的，但其作者已经指出它不完备。在本文中，我们提供了一个反例来证明这个事实，并提出相关变化来调整原始的DC策略以确保其正确性。DC的修改和其正确性的详细证明是本研究的主要贡献。
作者：Josu Oca and Montserrat Hermo and Alexander Bolotov
论文ID：2307.00540
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-09-01