A Resolution Calculus for Branching-Time Temporal Logic CTL. Zhang, L., Hustadt, U., & Dixon, C. *ACM Transactions on Computational Logic*, 15(1):10:1-38, February, 2014. Paper abstract bibtex 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 trans- lation 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.

@article{Zhang+Hustadt+Dixon@ToCL2014,
author = {Lan Zhang and Ullrich Hustadt and Clare Dixon},
title = {A Resolution Calculus for Branching-Time Temporal Logic {CTL}},
journal = {ACM Transactions on Computational Logic},
year = {2014},
month = feb,
volume = {15},
number = {1},
pages = {10:1-38},
url = {http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf},
abstract = {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 trans- lation 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.}
}

Downloads: 0

{"_id":"bKLJZzhZeQcG9Cwgr","bibbaseid":"zhang-hustadt-dixon-aresolutioncalculusforbranchingtimetemporallogicctl-2014","author_short":["Zhang, L.","Hustadt, U.","Dixon, C."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Lan"],"propositions":[],"lastnames":["Zhang"],"suffixes":[]},{"firstnames":["Ullrich"],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]},{"firstnames":["Clare"],"propositions":[],"lastnames":["Dixon"],"suffixes":[]}],"title":"A Resolution Calculus for Branching-Time Temporal Logic CTL","journal":"ACM Transactions on Computational Logic","year":"2014","month":"February","volume":"15","number":"1","pages":"10:1-38","url":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf","abstract":"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 trans- lation 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.","bibtex":"@article{Zhang+Hustadt+Dixon@ToCL2014,\n author = {Lan Zhang and Ullrich Hustadt and Clare Dixon},\n title = {A Resolution Calculus for Branching-Time Temporal Logic {CTL}},\n journal = {ACM Transactions on Computational Logic},\n year = {2014},\n month = feb,\n volume = {15},\n number = {1},\n pages = {10:1-38},\n url = {http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf},\n abstract = {The branching-time temporal logic CTL is useful for\n specifying systems that change over time and involve quantification\n over possible futures. Here we present a resolution calculus for CTL\n that involves the trans- lation of formulae to a normal form and the\n application of a number of resolution rules. We use indices in the\n normal form to represent particular paths and the application of the\n resolution rules is restricted dependent on an ordering and selection\n function to reduce the search space. We show that the translation\n preserves satisfiability, the calculus is sound, complete and\n terminating and consider the complexity of the calculus.}\n}\n\n\n\n","author_short":["Zhang, L.","Hustadt, U.","Dixon, C."],"key":"Zhang+Hustadt+Dixon@ToCL2014","id":"Zhang+Hustadt+Dixon@ToCL2014","bibbaseid":"zhang-hustadt-dixon-aresolutioncalculusforbranchingtimetemporallogicctl-2014","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Zhang+Hustadt+Dixon@ToCL2014.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["resolution","calculus","branching","time","temporal","logic","ctl","zhang","hustadt","dixon"],"title":"A Resolution Calculus for Branching-Time Temporal Logic CTL","year":2014}