WestminsterResearch

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: 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]
Preview
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