CTL-RP: A computation tree logic resolution prover

Issue title: Practical Aspects of Automated Reasoning

Article type: Research Article

Authors: Zhang, Lan | Hustadt, Ullrich | Dixon, Clare

Affiliations: Department of Computer Science, University of Liverpool, Liverpool, UK. E-mails: {Lan.Zhang, U.Hustadt, CLDixon}@liverpool.ac.uk

Abstract: In this paper, we present a resolution-based calculus RCTL>,S for Computation Tree Logic (CTL) as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus RCTL>,S requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal semantics for the clausal normal form, provide proof sketches for the soundness and completeness of the resolution rules, discuss the complexity of the decision procedure based on RCTL>,S, and present an approach to implementing the calculus RCTL>,S using first-order techniques. Finally, we give a comparison between CTL-RP and a tableau theorem prover for CTL.

Keywords: Branching-time temporal logics, resolution theorem proving

DOI: 10.3233/AIC-2010-0463

Journal: AI Communications, vol. 23, no. 2-3, pp. 111-136, 2010