LTL over Description Logic Axioms

Franz BaaderFranz Baader, Silvio GhilardiSilvio Ghilardi, Carsten LutzCarsten Lutz

Download

Franz Baader, Silvio Ghilardi, Carsten Lutz
LTL over Description Logic Axioms
Proceedings of the 21st International Workshop on Description Lo gics (DL2008), volume 353 of CEUR-WS, 2008

Details
Bibtex

KurzfassungAbstract
Most of the research on temporalized Description Logics (DLs) has concentrated on the most general case where temporal operators can occur both within DL concepts and in front of DL axioms. In this setting, reasoning usually becomes quite hard. If rigid roles (i.e., roles whose interpretation does not vary over time) are allowed, then the interesting inference problems (such as satisfiability of concepts) become undecidable. Even if all symbols are interpreted as flexible (i.e., their interpretations can change arbitrarily from one time-point to the next), the complexity of reasoning is doubly exponential, i.e., one exponential higher than the complexity of reasoning in pure DLs such as ALC. In this paper, we consider the case where temporal operators are allowed to occur only in front of axioms (i.e., ABox assertions and general concept inclusion axioms (GCIs)), but not inside concepts. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider ALC. We show that reasoning becomes simpler in this setting.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ BaGhiLu-DL08,
  author = {Franz {Baader} and Silvio {Ghilardi} and Carsten {Lutz}},
  booktitle = {Proceedings of the 21st International Workshop on Description Lo\ \ gics ({DL2008})},
  series = {CEUR-WS},
  title = {LTL over Description Logic Axioms},
  volume = {353},
  year = {2008},
}