A Resolution Calculus for the Branching-Time Temporal Logic CTL

作者：Zhang Lan; Hustadt Ullrich; Dixon Clare^*

来源：ACM Transactions on Computational Logic, 2014, 15(1): 10.

DOI：10.1145/2529993

• Theory
• Algorithms
• Verification
• Temporal logic
• automated theorem proving
• resolution

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.

• 出版日期2014-2
• 单位首都经济贸易大学