A Clausal Resolution Method for Branching-Time Logic ECTL+ Alexander Bolotov and Artie Basukoski   View Paper (PDF)   Return to Research Papers 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. BIBTEX @inproceedings{DBLP:conf/time/BolotovB04,    author    = {Alexander Bolotov and                 Artie Basukoski},    title     = {A Clausal Resolution Method for Branching-Time Logic ECTL+.},    booktitle = {TIME},    year      = {2004},    pages     = {140-147},    ee        = {http://csdl.computer.org/comp/proceedings/time/2004/2155/00/21550140abs.htm},    crossref  = {conf/time/2004},    bibsource = {DBLP, http://dblp.uni-trier.de}  }  @proceedings{DBLP:conf/time/2004,    title     = {11th International Symposium on Temporal Representation                 and Reasoning (TIME 2004), 1-3 July 2004, Tatihou Island,                 Normandie, France},    booktitle = {TIME},    publisher = {IEEE Computer Society},    year      = {2004},    isbn      = {0-7695-2155-X},    bibsource = {DBLP, http://dblp.uni-trier.de}  } }, ©2005 Association for Computing Machinery