DocumentCode
3386201
Title
Search strategies for resolution in CTL-type logics: extension and complexity
Author
Basukoski, Artie ; Bolotov, Alexander
Author_Institution
Harrow Sch. of Comput. Sci., Westminster Univ., UK
fYear
2005
fDate
23-25 June 2005
Firstpage
195
Lastpage
197
Abstract
A clausal resolution approach originally developed for the branching logic CTL has recently been extended to the logics ECTL and ECTL+. In the application of the resolution rules searching for a loop is essential. In this paper, we define a depth-first technique to complement the existing breadth-first search and provide the complexity analysis of the developed methods. Additionally, it contains a correction in our previous presentation of loops.
Keywords
computational complexity; formal logic; tree searching; breadth-first search; complexity analysis; concurrent tree logic; depth-first technique; logic CTL; search strategy; Application software; Bismuth; Computer science; Logic; Search methods;
fLanguage
English
Publisher
ieee
Conference_Titel
Temporal Representation and Reasoning, 2005. TIME 2005. 12th International Symposium on
ISSN
1530-1311
Print_ISBN
0-7695-2370-6
Type
conf
DOI
10.1109/TIME.2005.32
Filename
1443371
Link To Document