A resolution calculus for the branching-time temporal logic CTL
A resolution calculus for the branching-time temporal logic CTL
复制标题
DOI：
10.1145/2529993
复制
发表时间：
2014-02
期刊：
影响因子：
--
通讯作者：
Lan Zhang;U. Hustadt;C. Dixon
中科院分区：
文献类型：
--
作者：
Lan Zhang;U. Hustadt;C. Dixon
分支时间时序逻辑CTL用于指定随时间变化的系统，并涉及对可能的未来的量化。在这里，我们提出了一个决议演算CTL，涉及到翻译的公式，一个正常的形式和应用程序的一些决议规则。我们使用正常形式的索引来表示特定的路径和决议规则的应用受到限制，依赖于排序和选择功能，以减少搜索空间。我们表明，翻译保持可满足性，演算是健全的，完整的，和终止，并考虑复杂的演算。
The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the translation of formulae to a normal form and the application of a number of resolution rules. We use indices in the normal form to represent particular paths and the application of the resolution rules is restricted dependent on an ordering and selection function to reduce the search space. We show that the translation preserves satisfiability, the calculus is sound, complete, and terminating, and consider the complexity of the calculus.