We study branching-time temporal description logics (TDLs) based on the DLs ALC and ℇL and the temporal logics CTL and CTL*. The main contributions are algorithms for satisfiability that are more direct than existing approaches, and (mostly) tight elementary complexity bounds that range from PTIME to 2EXPTIME and 3EXPTIME. A careful use of tree automata techniques allows us to obtain transparent and uniform algorithms, avoiding to deal directly with the intricacies of CTL*.
Paper
Full text
Complexity of Branching Temporal Description Logics
Semantic Scholar · Computer Science · 2012
Abstract
We study branching-time temporal description logics (TDLs) based on the DLs ALC and ℇL and the temporal logics CTL and CTL*. The main contributions are algorithms for satisfiability that are more direct than existing approaches, and (mostly) tight elementary complexity bounds that range from PTIME to 2EXPTIME and 3EXPTIME. A careful use of tree automata techniques allows us to obtain transparent and uniform algorithms, avoiding to deal directly with the intricacies of CTL*.
References (23)
Scroll for more · 11 remaining