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
ACM Trans. Comput. Log., 13(3), 2012

Details
Bibtex

KurzfassungAbstract
Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can be applied to concepts, and sometimes additionally to TBox axioms and ABox assertions. The aim of this paper is to study temporalized DLs where temporal operators on TBox axioms and ABox assertions are available, but temporal operators on concepts are not. While the main application of existing temporalized DLs is the representation of conceptual models that explicitly incorporate temporal aspects, the family of DLs studied in this paper addresses applications that focus on the temporal evolution of data and of ontologies. Our results show that disallowing temporal operators on concepts can significantly decrease the complexity of reasoning. In particular, reasoning with rigid roles (whose interpretation does not change over time) is typically undecidable without such a syntactic restriction, whereas our logics are decidable in elementary time even in the presence of rigid roles. We analyze the effects on computational complexity of dropping rigid roles, dropping rigid concepts, replacing temporal TBoxes with global ones, and restricting the set of available temporal operators. In this way, we obtain a novel family of temporalized DLs whose complexity ranges from 2-ExpTime-complete via NExpTime-complete to ExpTime-complete.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ BaaderGL12,
  author = {Franz {Baader} and Silvio {Ghilardi} and Carsten {Lutz}},
  journal = {ACM Trans. Comput. Log.},
  number = {3},
  title = {{LTL} over Description Logic Axioms},
  volume = {13},
  year = {2012},
}