Bolotov, Alexander and Basukoski, Artie (2004) A clausal resolution method for branching-time logic ECTL+. In: Combi, Carlo, (ed.) 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
![[img]](http://westminsterresearch.wmin.ac.uk/style/images/fileicons/application_pdf.png)
| PDF 645Kb |
Official URL: http://dx.doi.org/10.1109/TIME.2004.1314431
Abstract
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 |
|---|---|
| Research Community: | University of Westminster > Electronics and Computer Science, School of |
| ID Code: | 1451 |
| Deposited On: | 04 May 2006 |
| Last Modified: | 11 Aug 2010 15:30 |
Repository Staff Only: item control page
