A clausal resolution method for branching-time logic ECTL+

Bolotov, Alexander and Basukoski, Artie (2004) A clausal resolution method for branching-time logic ECTL+. In: 11th International Symposium on Temporal Representation and Reasoning: (TIME 2004), Tatihou, Normandie, France, 1-3 July 2004. IEEE Computer Society, pp. 140-147. ISBN 076952155X


Download (661kB)
Official URL: http://dx.doi.org/10.1109/TIME.2004.1314431


We expand the applicability of the clausal resolution technique to the branching-time temporal logic ECTL_. ECTL_ is strictly more expressive than the basic computation tree logic CTL and its extension, ECTL, as it allows Boolean combinations of fairness and single temporal operators. We show that any ECTL_ formula can be translated to a normal form the structure of which was initially defined for CTL and then applied to ECTL. This enables us to apply to ECTL_ a resolution technique defined over the set of clauses. Our correctness argument also bridges the gap in the correctness proof for ECTL: we show that the transformation procedure for ECTL preserves unsatisfiability.

Item Type: Book Section
Subjects: University of Westminster > Science and Technology > Electronics and Computer Science, School of (No longer in use)
Depositing User: Miss Nina Watts
Date Deposited: 04 May 2006
Last Modified: 11 Aug 2010 14:30
URI: http://westminsterresearch.wmin.ac.uk/id/eprint/1451

Actions (login required)

Edit Item (Repository staff only) Edit Item (Repository staff only)