We design a logic in the temporal DL-Lite family (with non-Horn role inclusions and restricted temporalised roles), for which answering ontology-mediated atomic queries (OMAQs) can be done in ExpSpace and even in PSpace for ontologies without existential quantification in the rule heads but determining FO-rewritability or (linear) Datalog-rewritability of OMAQs is undecidable. On the other hand, we show (by reduction to monadic disjunctive Datalog) that deciding FO-rewritability of OMAQs in the non-temporal fragment of our logic can be done in 3NExpTime.
Temporal description logics are used to reason about relational data that evolves in time. Along
with the standard DL constructs on concepts and roles they admit temporal operators such
as ○ (at the next moment), □ (always in the future), ♢ (sometime later) and their
pasttime counterparts, which give rise to temporalised concepts and roles. Being non-monodic [
The proliferation of ontology-based data access [
Example 1. Imagine that we are modelling the European transport network. Some passengers may like to go by plane in one direction but return by train (say, to safely bring back a selection of wines, cheeses and fine teas). To highlight such routes, one could use the following RI: lfight ⊓ ♢ train−
⊑ safeFlightConnection, where train− denotes the inverse of the role train (connection) from one city to another. (In our modelling, we do not regard the roles flight and train as ‘global’ because they depend on the season, day of a week, etc.) We may further partition the connections into certain classes, e.g., national and international, and infer properties of connected cities based on this classification. This is achieved by means of non-Horn RIs and CIs: safeFlightConnection ⊑ national ⊔ international, ∃international ⊑ InternationalAirport.
Axiom (1) is an example of a guarded ♢ -RI, where the temporalised role ♢ train− is ‘guarded’ by the role name flight . Thus, safeFlightConnection may be inferred at a time instant only when there exists a flight from one city to another and, sometime later, there is a return train.
The temporal description logic TDL-Liteb[♢oo]l we introduce in this paper admits arbitrary
Boolean CIs with temporalised concepts, and only guarded ♢ -RIs with temporalised roles that
take the form
1 ⊓ · · · ⊓
⊓ ♢ +1+1 ⊓ . . . ♢ ⊑ +1 ⊔ · · · ⊔
,
(3)
where the are role names or their inverses, the ♢ are sequences of ♢ and ♢ , and ≥ 1. We
prove that answering ontology-mediated atomic queries (OMAQs) in TDL-Liteb[♢oo]l can be done in
ExpSpace for combined complexity, and in PSpace for the flat fragment of TDL-Liteb[♢oo]l, which
disallows positive occurrences of ∃ in ontology axioms (Th. 1). However, determining whether
such a query can be rewritten into an FO- or a (linear) Datalog query is algorithmically
undecidable (Th. 2). On the other hand, we observe that FO-rewritability of OMAQs in DL-Litebool, i.e. in
TDL-Liteb[♢oo]l without temporalised concepts and roles, becomes decidable in 3NExpTime (Th. 3).
For the proofs consult the full version of the paper at https://eprints.bbk.ac.uk/id/eprint/51763.
2. OMAQ Answering and FO-rewritability in TDL-Liteb[♢ o]ol
The logic TDL-Liteb[♢oo]l is a member of the TDL-Lite family [
A TBox, , is a finite set of CIs, and an RBox, ℛ, is a finite set of guarded ♢ -RIs. Taken [♢ ] together, they form an ontology, , in TDL-Litebool. An ABox signature, Σ, is a set of concept and role names. An ABox, , over Σ is a finite set of facts of the form (, ℓ) and (, , ℓ), where , ∈ Σ and ℓ ∈ Z is a timestamp. We denote by ind () the set of individual names in , by min() and max() the minimal and maximal timestamps in , respectively, and by tem() the closed interval [min(), max()].
An ontology-mediated atomic query (OMAQ) is a triple (, ) = (, Σ, (, )), where
[♢ ]
is an ontology in TDL-Litebool, Σ is an ABox signature, a concept name, ranges over
ind (), and over tem(). (Note that the symbols in and do not have to be in Σ.) A pair
(, ℓ) ∈ ind () × tem() is a certain answer to (, ) over a Σ-ABox if (, ℓ) is true in
every model ℳ of (, ); for a detailed definition of a model the reader is referred to [
With an ABox we associate a temporal FO-structure S with domain ind () × tem(), over which we can evaluate FO(<)- and Datalog-queries with atoms of the form (, ), (, , ), (1 < 2). Let ℒ be any relevant query language: FO(<), linear or arbitrary Datalog queries. An OMAQ (, ) = (, Σ, (, )) is ℒ-rewritable if there exists an ℒ-query (, ), such that ans() = { (, ℓ) ∈ ind () × tem() | S |= (, ℓ) }, for every Σ-ABox . An OMBAQ is ℒ-rewritable if there is an ℒ-query without answer variables such that S |= if the certain answer to over is ‘yes’. It is known that FO(<)-, linear Datalog-, and Datalog-rewritability guarantee answering OMAQs/OMBAQs in AC0 [14], NL [15], and [♢ ] PTime [16] for data complexity, respectively. For the non-temporal fragment of TDL-Litebool, i.e. DL-Litebool, answering OMAQs/OMBAQs is ExpTime-complete for combined complexity [17]. We establish an ExpSpace upper bound for answering OMAQs/OMBAQs in full TDL-Liteb[♢oo]l. We also consider the flat TDL-Liteb[♢oo]l that disallows concepts ∃ on the right-hand side of CIs. This restriction reduces the complexity of answering OMAQs/OMBAQs to PSpace. Theorem 1. Answering TDL-Liteb[♢oo]l OMAQs/OMBAQs is in ExpSpace and ExpTime-hard for combined complexity. Answering flat TDL-Liteb[♢oo]l OMAQs/OMBAQs is PSpace-complete for combined complexity.
However, checking whether a query is rewritable into FO(<) or (linear) Datalog turns out to be undecidable even for flat ontologies.
Theorem 2. FO(<)-rewritability, linear Datalog-rewritability (if NL ̸= coNP ), and Datalogrewritability (if PTime ̸= coNP ) are undecidable for flat TDL-Lite b[♢oo]l OMAQs/OMBAQs.
The proof of Th. 2 makes use of the interaction between non-Horn RIs and temporal axioms.
FO-rewritability of OMAQs/OMBAQs becomes decidable in the case when ontologies do not
contain temporal operators. We obtain a positive result for the language DL-Litebool that
disallows temporalised concepts and temporalised roles in TDL-Liteb[♢oo]l. The proof is via a translation
to monadic disjunctive Datalog, adapting a similar technique for ℒℐ [
Theorem 3. Checking FO-rewritability of DL-Litebool OMAQs/OMBAQs is in 3NExpTime.
The problem of deciding if a given OMQ is rewritable into a conventional query language ℒ
has been investigated for several important description logics. Bienvenu et al. [
In this paper, we take a first step towards understanding (temporal) DL-Lite with guarded non-Horn role inclusions by establishing two results: a decision procedure for FO-rewritability of OMQs in DL-Litebool, and an undecidability result for FO(<)- and Datalog-rewritability of [♢ ] OMQs in TDL-Litebool, i.e., DL-Litebool with temporalised concepts and (guarded) roles. An open question is if rewritability is decidable for DL-Litebool with temporalised concepts only.
FO-rewritability (aka boundedness) has been studied for Datalog itself. Predicate boundedness is undecidable for binary programs [19], and even for linear programs with one binary IDB relation [20], while for linear monadic programs, it is in PSpace [21]. Uniform boundedness is undecidable for ternary programs [19], even if they are linear [22] (consult the latter for an explanation on diferent forms of Datalog boundedness). Temporalised RIs in TDL-Liteb[♢oo]l can be viewed from the Datalog perspective as using binary, or even ternary IDBs. However, the undecidability proofs of [19], [20] and [22] make use of chains, i.e., Datalog rules where the right-hand part contains constructs like (1, 2) ∧ (2, 3), which is inexpressible in DL-Lite. Compared to ℒℱ , DL-Lite lacks negation and qualified existential restrictions.
Journal of Artificial Intelligence Research 36 (2009) 1–69. doi: 10.1613/jair.2820. [14] N. Immerman, Descriptive Complexity, Springer Verlag, 1998. [15] E. Grädel, Capturing complexity classes by fragments of second-order logic, Theoretical Computer Science 101 (1992) 35 – 57. doi:10.1016/0304-3975(92)90149-A, cited by: 64. [16] E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov, Complexity and expressive power of logic programming, ACM Comput. Surv. 33 (2001) 374–425. doi:10.1145/502807.502810. [17] R. Kontchakov, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Boolean Role Inclusions in DL-Lite With and Without Time, in: Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020, pp. 582–591. doi:10.24963/ kr.2020/58. [18] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Firstorder rewritability of ontology-mediated queries in linear temporal logic, Artificial Intelligence 299 (2021) 103536. doi:https://doi.org/10.1016/j.artint.2021.103536. [19] G. G. Hillebrand, P. C. Kanellakis, H. G. Mairson, M. Y. Vardi, Undecidable boundedness problems for datalog programs, The Journal of Logic Programming 25 (1995) 163–190. doi:https://doi.org/10.1016/0743-1066(95)00051-K. [20] M. Y. Vardi, Decidability and undecidability results for boundedness of linear recursive queries, PODS ’88, Association for Computing Machinery, New York, NY, USA, 1988, p. 341–351. doi:10.1145/308386.308470. [21] R. v. d. Meyden, Predicate boundedness of linear monadic datalog is in pspace, International Journal of Foundations of Computer Science 11 (2000) 591–612. doi:10.1142/ S0129054100000351. [22] J. Marcinkowski, Achilles, turtle, and undecidable boundedness problems for small datalog programs, SIAM Journal on Computing 29 (1999) 231–257. doi:10.1137/ S0097539797322140.