在LTL Tableau的深度优先搜索中处理冲突，以简化基于合规性的语言
Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages
摘要：
提供适当的工具来解决不一致的合规规则的问题是一个重要的研究课题。这个问题对于实现对早期声明式设计的自动支持以及支持基于契约或基于服务的系统中规则的演化至关重要。在本文中，我们研究的问题，提取时间不可满足的核心，以检测不一致的部分规范。我们扩展了冲突驱动的SAT求解器，为时序逻辑提供了一个新的冲突驱动的深度优先搜索求解器。我们使用此求解器来计算LTL不可满足的核心，而无需重新探索求解器的历史。
英文摘要：
Providing adequate tools to tackle the problem of inconsistent compliance rules is a critical research topic. This problem is of paramount importance to achieve automatic support for early declarative design and to support evolution of rules in contract-based or service-based systems. In this paper we investigate the problem of extracting temporal unsatisfiable cores in order to detect the inconsistent part of a specification. We extend conflict-driven SAT-solver to provide a new conflict-driven depth-first-search solver for temporal logic. We use this solver to compute LTL unsatisfiable cores without re-exploring the history of the solver.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
