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.
|Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Friday, 07-Nov-2014 11:55:44 GMT © 1998-2004 by Ullrich Hustadt.|