DocumentCode :
3193835
Title :
A clausal resolution method for branching-time logic ECTL
Author :
Bolotov, Alexander ; Basukoski, Artie
Author_Institution :
Harrow Sch. of Comput. Sci., Westminster Univ., UK
fYear :
2004
fDate :
1-3 July 2004
Firstpage :
140
Lastpage :
147
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.
Keywords :
formal specification; formal verification; temporal logic; theorem proving; trees (mathematics); Boolean combinations; ECTL+; branching-time logic; clausal resolution method; extended computation tree logic; temporal logic; temporal operators; Boolean functions; Bridges; Computer science; DH-HEMTs; Logic;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Temporal Representation and Reasoning, 2004. TIME 2004. Proceedings. 11th International Symposium on
ISSN :
1550-1311
Print_ISBN :
0-7695-2155-X
Type :
conf
DOI :
10.1109/TIME.2004.1314431
Filename :
1314431
Link To Document :
بازگشت