A Resolution Calculus for the Branching-Time Temporal Logic CTL



Zhang, Lan, Hustadt, Ullrich ORCID: 0000-0002-0455-0267 and Dixon, Clare ORCID: 0000-0002-4610-9533
(2014) A Resolution Calculus for the Branching-Time Temporal Logic CTL. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 15 (1). pp. 1-38.

[thumbnail of Zhang+Hustadt+Dixon@ToCL2013.pdf] PDF
Zhang+Hustadt+Dixon@ToCL2013.pdf - Author Accepted Manuscript

Download (527kB)

Abstract

<jats:p>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.</jats:p>

Item Type: Article
Additional Information: ## TULIP Type: Articles/Papers (Journal) ##
Uncontrolled Keywords: Theory, Algorithms, Verification, Temporal logic, automated theorem proving, resolution
Subjects: ?? QA75 ??
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 11 Oct 2013 10:57
Last Modified: 09 Jan 2023 22:04
DOI: 10.1145/2529993
Publisher's Statement : © ACM, 2014.This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Computational Logic VOL 15, ISS 1, February 2014 http://doi.acm.org/10.1145/2529993
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/13453