DL-Lite with Temporalised Concepts, Rigid Axioms and Roles

We investigate the temporal extension of the description logic DL-Lite(RN ) bool with the until operator on concepts, rigid (time-independent) and local (time-dependent) roles, and rigid TBox axioms. Using an embedding into the one-variable fragment of first-order temporal logic and the quasimodel technique, we prove that (i) the satisfiability problem for the resulting logic is PSpace-complete, and that (ii) by weakening until to sometime in the future we obtain an NP-complete logic, which matches the complexities of the propositional linear-time temporal logics with the corresponding temporal operators.

• Type: Conference
• Year: 2009
• Where: FROCOS
• Authors: Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev
• Keywords: Control Systems, FROCOS 2009, Rigid Tbox Axioms, Temporal Logics, first-order Temporal Logic