Temporal Ontology-Mediated Queries and First-Order Rewritability: A Short Course

Abstract

We discuss recent attempts to extend the ontology-based data access (aka virtual knowledge graph) paradigm to the temporal setting. Our main aim is to understand when answering temporal ontology-mediated queries can be reduced to evaluating standard first-order queries over timestamped data and what numeric predicates and operators are required in such reductions. We consider two ways of introducing a temporal dimension in ontologies and queries: using linear temporal logic LTL over discrete time and using metric temporal logic MTL over dense time.

1 Introduction

Imagine that you are an engineer and that your task is to analyse the behaviour of some complex system (such as gas turbines or drilling rigs) in order to understand what kind of undesirable events have happened in it over the past few days and why. As many others in this weird time of Covid-19 pandemic, you are working from home and can only figure out what has been going on with the system by querying the data, which is automatically collected from the system’s sensors and stored in the company’s databases. Your intuition and experience suggest that first you should look for emergency stops and unusually high and low values of temperature, rotor speed and other parameters read by the sensors. Then you would investigate more complex events such as ‘purging is over’ that happens, according to the manual, when the main flame was on for the past 10 s and also, within the previous 10 min, there was a 30-s period when the rotor speed was above 1260 rpm and, at most 2 min before the start of that period, the rotor speed was below 1000 rpm for at least 1 min.

You might be a brilliant engineer with intimate knowledge of your equipment but alas, the odds are you have no clue where the data is stored and in which form. (Your IT expert, Joe, would have told you, if asked politely, that the equipment ID, timestamp and temperature are, respectively, in the first, tenth and fifth columns of a database table SENSOR_TEM_C, the rotor speed measurements are in a different table ROTOR_SP_RPM, and emergency stops are in a special spreadsheet—but who would you dare ask him in the time of self-isolation with three kids, a wife-mathematician and a grumpy granny in a one-bedroom flat?)

The ontology-based data access (OBDA)  [29, 73, 84]—recently rebranded as the virtual knowledge graph (VKG)  [85]—paradigm has been introduced in the mid 2000s to facilitate access to data, make it more user-friendly, and remove the dependency on IT experts as far as formalising user queries is concerned. Informally, an OBDA system such as Mastro¹ or Ontop² allows the users to think that the data is always at hand in the form of a ‘knowledge graph’ whose vertices are individuals in the database labelled by classes they belong to and whose directed edges are labelled by relationships between those individuals. For example, the database facts that t11 is a gas turbine having rotor r3 as its moving part can be thought of as a graph edge labelled by hasMovingPart and going from a vertex t11 with label GasTurbine to a vertex r3 with label Rotor.

As the names of classes and relationships are familiar to the users (taken from the user manual or a textbook on the relevant domain) and the structure of the data is transparent (directed graph), formulating queries in the OBDA system should be much easier than, say, in a relational database management system (RDBMS)—especially if a visual query interface such as OptiqueVQS  [77] is enabled. Moreover, the OBDA system has a secret weapon in the form of an ontology, which is supposed to capture the background knowledge about the domain. In particular, it can contain definitions and descriptions of complex classes and relationships in terms of primitive ones, which can also be utilised in user queries. Thus, the ontology provides the user with a high-level conceptual view of the data and fixes a convenient vocabulary for queries; it supports queries to multiple and possibly heterogeneous data sources, which are of no concern to the user; and it allows the system to enrich incomplete data with background knowledge, which involves reasoning.

Does it sound too good to be true? Let us make the OBDA fairy tale told above more formal and see what it amounts to computationally. Denote by $\mathcal {O}$ the ontology (designed by a domain expert). There exist dozens of ontology languages: description logics (DLs)  [12, 13] of different expressivity, the Web Ontology Language OWL³ and its profiles, logic programming and deductive database languages Prolog and datalog, the perennial first-order logic (FO), etc. Let $\mathcal {O}$ be formulated in one of those languages. The knowledge graph, which the user wants to query, is a set, $\mathcal {A}$, of ground atoms of the form A(a) and P(a, b), where A is a unary predicate (class or concept such as Rotor) and P a binary predicate (relationship or property such as hasMovingPart) in the vocabulary of $\mathcal {O}$. The trouble is that $\mathcal {A}$ does not exist, it is virtual. It can be defined by means of a set, $\mathcal {M}$, of mappings of the form $S(\textit{\textbf{x}}) \leftarrow \varPhi (\textit{\textbf{x}})$, where S is a unary or binary predicate from $\mathcal {O}$ and $\varPhi$ a query over one of the datasources, $\mathcal {D}$ (say, an SQL query to a relational database). Thus, $\mathcal {A}$ can be defined as $\mathcal {M}(\mathcal {D})$. The mappings $\mathcal {M}$ are written by an expert with detailed knowledge of both $\mathcal {O}$ and $\mathcal {D}$. The users do not need to know anything about them. The users’ only task is to formulate a query $\varphi (\textit{\textbf{x}})$ over (imaginary) $\mathcal {A}$ in a query language such as SPARQL⁴ and press the enter key. The pair ${\textit{\textbf{q}}}= (\mathcal {O},\varphi (\textit{\textbf{x}}))$ is called an ontology-mediated query, OMQ for short. The OBDA system is then supposed to find certain answers to ${\textit{\textbf{q}}}$ over $\mathcal {A}$—actually, over $\mathcal {D}$ as $\mathcal {A}$ does not exist—which are tuples $\textit{\textbf{a}}$ of individuals from $\mathcal {A}$ such that $\varphi (\textit{\textbf{a}})$ is a logical consequence of $\mathcal {O}$ and $\mathcal {A}$, in which case we write $\mathcal {O}, \mathcal {A}\models \varphi (\textit{\textbf{a}})$. Thus, the OBDA system has to somehow compute all tuples $\textit{\textbf{a}}$ for which $\mathcal {O}, \mathcal {M}(\mathcal {D}) \models \varphi (\textit{\textbf{a}})$ holds. Whether it is feasible or not depends on the ontology, mapping and query languages involved.

The crucial idea behind the OBDA paradigm is that these languages should be chosen in such a way that the OMQ answering problem—‘is it the case that $\mathcal {O}, \mathcal {M}(\mathcal {D}) \models \varphi (\textit{\textbf{a}})$?’—could be reduced to the evaluation problem for standard database queries directly over $\mathcal {D}$. When $\mathcal {D}$ is a relational database, it would be great if the problem of answering ${\textit{\textbf{q}}}$ could be somehow reformulated, or rewritten, by the OBDA system into an SQL query $\textit{\textbf{Q}}(\textit{\textbf{x}})$ with the answer variables $\textit{\textbf{x}}$, which is then executed over $\mathcal {D}$ by an RDBMS at hand. In our theoretical setting we might as well assume that $\textit{\textbf{Q}}(\textit{\textbf{x}})$ is an FO-formula  [1] and call an OMQ ${\textit{\textbf{q}}}= (\mathcal {O},\varphi (\textit{\textbf{x}}))$ FO-rewritable if there is an FO-formula $\textit{\textbf{Q}}(\textit{\textbf{x}})$, a rewriting of ${\textit{\textbf{q}}}$, such that, for any data instance $\mathcal {D}$ and any tuple $\textit{\textbf{a}}$ of individuals in $\mathcal {D}$, we have $\mathcal {O}, \mathcal {M}(\mathcal {D}) \models \varphi (\textit{\textbf{a}})$ iff $\mathcal {D} \models \textit{\textbf{Q}}(\textit{\textbf{a}})$. If the language for mappings $\mathcal {M}$ is sufficiently simple (say, R2RML⁵), then it actually suffices to find an FO-rewriting $\textit{\textbf{Q}}(\textit{\textbf{x}})$ of ${\textit{\textbf{q}}}$ over possible virtual knowledge graphs $\mathcal {A}$, which can be later transformed to a proper SQL query over $\mathcal {D}$ by the OBDA system using the mappings (for details on this, consult  [84] and references therein). Thus, we arrive to the main definition of this paper: $\textit{\textbf{Q}}(\textit{\textbf{x}})$ is an FO-rewriting of ${\textit{\textbf{q}}}= (\mathcal {O},\varphi (\textit{\textbf{x}}))$ just in case $\mathcal {O}, \mathcal {A} \models \varphi (\textit{\textbf{a}})$ iff $\mathcal {A}\models \textit{\textbf{Q}}(\textit{\textbf{a}})$, for every VKG $\mathcal {A}$ (in the language of $\mathcal {O}$) and every tuple $\textit{\textbf{a}}$ of individuals from $\mathcal {A}$.

FO-rewritability is a very strong requirement for ontology and query languages; far from all of them satisfy it. By now, description logics and other fragments of FO that guarantee FO-rewritability are well studied and understood  [84]. For example, the OWL 2 QL profile of the Web Ontology Language OWL 2⁶ (underpinned by the DL-Lite family of description logics  [6, 29]) is the W3C standard ontology language for OBDA, which ensures FO-rewritability of all OMQs with an OWL 2 QL ontology and a SPARQL or conjunctive query. It is supported by MASTRO and Ontop. So OBDA is not a fairy tale after all.

But can you use it to spot in the sensor data those nasty events that possibly happened in your equipment? Unfortunately, not yet. Because the OBDA framework we discussed above has only been developed and implemented for querying non-temporal data using atemporal ontologies. Temporal OBDA is still largely work in progress, and the aim of this paper is to present and discuss some of the existing approaches to temporalising ontology-mediated query answering (where the authors have particular research interests). A more comprehensive recent survey of temporal OBDA can be found in  [9], though the area is moving forward very fast.

2 One-Dimensional Temporal OBDA

We begin our discussion of temporal OBDA with a very simple case. Imagine that the system whose behaviour we need to analyse is equipped with a number of sensors, say $S_1,\dots ,S_n$. At certain moments of time, t, the system records in a database the current measurement of one or more sensors $S_i$. So we can assume that the database records take the form $S_i(t,v)$, where t is a moment of time, or a timestamp, and v a measurement value. When speaking of temporal events, we often classify those values into qualitative categories, which may vary from one context to another, such as high temperature (e.g., $v \ge 300 \,^\circ$C), low temperature (say, $v \le 30\,^{\circ }$C), etc. Thus, we may want to think of the record $S_3(t,350\,^\circ$C) as $\textit{High}(t)$: at moment t, the temperature was high. The conversion of the original quantitative 2D data $S_i(t,v)$ into qualitative 1D data of the form A(t) can easily be done by mappings, for example,

$$\begin{aligned}&\textit{High(t)} \leftarrow \mathtt {SELECT\ t\ FROM\ }S_3\ \mathtt {WHERE \ v \ >= \ 300}. \end{aligned}$$

To sum up, let $A_i$, for $i=1,2,\dots$, be a countably infinite list of unary (or monadic) predicate symbols representing such qualitative measurements. Then every data instance we want to query is simply a finite set of atoms of the form $A_i(t)$ with a timestamp t. But what is time?

In general, this is a very difficult question. Remember ‘There is a time for everything. [...] Whatever is has already been’ (Ecclesiastes) or ‘Time is an illusion. Lunchtime doubly so’ (Douglas Adams, The Hitchhiker’s Guide to the Galaxy)? Even Computer Science uses numerous models of time: linear and branching, discrete and dense, finite and infinite, etc.  [34, 36, 38, 40]. So, what can we say about our data instances?

One important property is clear: as we store data about events that have already happened, we may assume that, for any timestamps t and $t'$, either $t < t'$ or $t=t'$, or $t > t'$. In other words, our time is linear. Whether the time is discrete or continuous depends on the type of the system we are dealing with. If it is synchronous in the sense that all records can only be made at a central clock signal, then time can be thought of as discrete, and so the timestamps in each data instance form a finite subset of the natural numbers $\mathbb {N}$ or the integer numbers $\mathbb {Z}$. In this paper, we prefer the integers.

Thus, in the case of discrete time, a data instance, $\mathcal {A}$, is a finite set of ground atoms of the form $A_i(\ell )$, where $\ell \in \mathbb {Z}$. We denote by $\min \mathcal {A}$ and $\max \mathcal {A}$ the minimal and maximal integer numbers occurring in $\mathcal {A}$. The active temporal domain of a data instance $\mathcal {A}$ is the set $\mathsf {tem}(\mathcal {A}) = \bigl \{\,n \in \mathbb {Z}\mid \min \mathcal {A}\le n \le \max \mathcal {A}\,\bigr \}$. To simplify constructions and without much loss of generality, we assume that $\min \mathcal {A}= 0$ and $\max \mathcal {A}\ge 1$.

If our system is asynchronous, database records can be made spontaneously, for example, when the current measurement of sensor $S_i$ differs ‘substantially’ from the previously recorded measurement taken by $S_i$. In this case, we can model time by the real numbers $\mathbb {R}$ or the rational numbers $\mathbb {Q}$. Since computer words are binary and finite, we prefer to assume that every timestamp is a dyadic rational number of the form $n/2^m$, where $n \in \mathbb {Z}$ and $m \in \mathbb {N}$. The set of these numbers is denoted by $\mathbb {Q}_2$. Note that although rationals such as 1/3 are not dyadic, by Cantor’s theorem, the order $(\mathbb {Q}_2,<)$ is dense in the sense that

$$ \forall x,y\, \big ( (x<y) \rightarrow \exists z \, (x< z < y) \big ) $$

and isomorphic to the order $(\mathbb {Q},<)$. Hence, rationals can be approximated with any accuracy by dyadic rationals. In this case, a data instance $\mathcal {A}$ is a finite set of ground atoms of the form $A_i(\ell )$ with $\ell \in \mathbb {Q}_2$. The active temporal domain of $\mathcal {A}$ is the finite set $\mathsf {tem}(\mathcal {A}) = \{\ell \mid A_i(\ell ) \in \mathcal {A}\}$.

Suppose we are interested in finding certain events in a given data instance. An event can be classified as instantaneous if it makes sense to say that it happens at a time instant (for example, an emergency stop or a power trip happened at moment t) and extended that can happen over a temporal interval (for example, the temperature was rising between $t_1$ and $t_2$). In this paper, we mainly consider the former type of events.

A natural language for speaking about temporal instantaneous events over $\mathbb {Z}$ is MFO$(<)$, monadic first-order logic with built-in precedence relation < (cf.  [30, 52]). More precisely, MFO$(<)$-formulas are built from unary predicates $A_i(x)$ and binary predicates $x=y$, $x<y$ using the standard Boolean connectives ($\wedge$, $\vee$, $\rightarrow$, $\lnot$) and first-order quantifiers ($\forall$ and $\exists$). They are interpreted in the usual way in structures, called (temporal) interpretations, of the form

$$ \mathcal {I}~=~ (\mathbb {Z}, <, A_1^\mathcal {I}, A_2^\mathcal {I}, \dots ), $$

which have domain $(\mathbb {Z},<)$ and interpret every predicate $A_i$ as a subset $A_i^\mathcal {I}\subseteq \mathbb {Z}$. Let $\mathfrak a$ be an assignment of numbers from $\mathbb {Z}$ to individual variables in MFO$(<)$-formulas. Given an MFO$(<)$-formula $\varphi (\textit{\textbf{x}})$ with free variables $\textit{\textbf{x}} = (x_1,\dots ,x_n)$, we write $\mathcal {I}\models \varphi (\mathfrak a(\textit{\textbf{x}}))$ to say that $\varphi$ is true in $\mathcal {I}$ under the assignment $\mathfrak a$ (which replaces $\textit{\textbf{x}}$ with $\mathfrak a(\textit{\textbf{x}}) = (\mathfrak a (x_1),\dots , \mathfrak a (x_n))$).

Example 1

We illustrate what can be said in MFO$(<)$ by a few examples. Suppose $\varphi (t,t') = (t< t') \wedge \lnot \exists t''\,(t< t'' < t')$, where $t< t'' < t'$ abbreviates the formula $(t< t'') \wedge (t'' < t')$. Then, for any interpretation $\mathcal {I}$ and any $m,n \in \mathbb {Z}$, we have $\mathcal {I}\models \varphi (m,n)$ iff $n = m+1$. It follows that, in MFO$(<)$-formulas, we can freely use the ‘functions’ $t+n$ and $t-n$, for every fixed $n \in \mathbb {Z}$. This allows us to capture events such as purging is over from the introduction. For instance, assuming that the clock ticks every second, the following FO-formula $\varphi (t)$ says that the main flame was on for the past 10 s and that within the previous 10 min, there was a 30-s period when the rotor speed was above 1260 rpm:

We invite the reader to extend this $\varphi (t)$ to a formula $\psi (t)$ that expresses the event purging is over described in the introduction. Then the sentence

$$\begin{aligned} \forall t\, \big [ \textit{PurgingIsOver}(t) \leftrightarrow \psi (t) \big ] \end{aligned}$$

(1)

defines a predicate $\textit{PurgingIsOver}(t)$ that can be used in queries.

By an MFO$(<)$-ontology we mean any finite set, $\mathcal {O}$, of MFO$(<)$-sentences. An interpretation $\mathcal {I}$ is a model of $\mathcal {O}$ if $\mathcal {I}\models \varphi$, for every sentence $\varphi \in \mathcal {O}$, in which case we write $\mathcal {I}\models \mathcal {O}$; $\mathcal {I}$ is a model of a data instance $\mathcal {A}$ if $\ell \in A^\mathcal {I}$ whenever $A(\ell ) \in \mathcal {A}$. We write $\mathcal {O}\models \varphi$ to say that $\mathcal {I}\models \varphi$, for every model $\mathcal {I}$ of $\mathcal {O}$.

MFO$(<)$-formulas $\psi (\textit{\textbf{t}})$ with free variables $\textit{\textbf{t}} = (t_1,\dots ,t_m)$ can also be used as queries asking for assignments of timestamps to the answer variables $\textit{\textbf{t}}$ under which the query holds true in relevant interpretations. An ontology-mediated query (OMQ) in MFO$(<)$ is a pair ${\textit{\textbf{q}}}= (\mathcal {O}, \psi (\textit{\textbf{t}}))$, where $\mathcal {O}$ is an ontology and $\psi (\textit{\textbf{t}})$ a query, both given in MFO$(<)$. If $\textit{\textbf{t}}$ is empty ($m=0$), then ${\textit{\textbf{q}}}$ is called a Boolean OMQ.

A certain answer to an OMQ ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ over a data instance $\mathcal {A}$ is any tuple $\varvec{\ell } = (\ell _1, \dots , \ell _m)$ such that $\ell _i\in \mathsf {tem}(\mathcal {A})$, for $1 \le i \le m$, and

$$\begin{aligned} \mathcal {I}\models \psi (\varvec{\ell }), \qquad \text { for every model }\mathcal {I}\text { of }(\mathcal {O}, \mathcal {A}). \end{aligned}$$

(2)

For a Boolean OMQ ${\textit{\textbf{q}}}$, a certain answer over $\mathcal {A}$ is ‘yes’ if $\mathcal {I}\models \psi$, for every model $\mathcal {I}$ of $\mathcal {O}$ and $\mathcal {A}$, and ‘no’ otherwise. The set of all certain answers to ${\textit{\textbf{q}}}$ over $\mathcal {A}$ is denoted by $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$. As a technical tool in our constructions, we also consider ‘certain answers’ that range over the whole of $\mathbb {Z}$ rather than only the active temporal domain $\mathsf {tem}(\mathcal {A})$; we denote the set of such certain answers over $\mathcal {A}$ and $\mathbb {Z}$ by $\mathsf {ans}^{\mathbb {Z}}({\textit{\textbf{q}}},\mathcal {A})$.

Example 2

Suppose $\mathcal {O}= \{\,\forall t\,(A(t) \rightarrow B(t+1)), \ \forall t\, (B(t) \rightarrow A(t+1))\,\}$ and $\mathcal {A}= \{\,A(0),\, C(1)\,\}$. Then $2n+1\in B^\mathcal {I}$, for any $n \ge 0$ and any model $\mathcal {I}$ of $(\mathcal {O},\mathcal {A})$. It follows that, for the OMQ ${\textit{\textbf{q}}}= (\mathcal {O}, \exists t'\, ((t' = t+2) \wedge B(t')))$, we have $\mathsf {ans}^{\mathbb {Z}}({\textit{\textbf{q}}},\mathcal {A}) = \{\,2n+1 \mid n\ge -1\,\}$, while $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}) = \{1\}$ because $\mathsf {tem}(\mathcal {A})=\{0,1\}$.

We are now in a position to introduce the central notion of the paper that reduces answering OMQs over data instances $\mathcal {A}$ to evaluation of first-order queries over a finite first-order structure $\mathfrak S_\mathcal {A}$ with domain $\mathsf {tem}(\mathcal {A})$ ordered by <, in which

$$\begin{aligned} \mathfrak S_\mathcal {A}\models A(\ell ) \quad \text {iff} \quad A(\ell )\in \mathcal {A}, \end{aligned}$$

for any predicate A and any $\ell \in \mathsf {tem}(\mathcal {A})$.

Definition 3

(FO-rewritability). Let $\mathcal {L}$ be a class of FO-formulas that can be interpreted over structures $\mathfrak S_\mathcal {A}$. (For example, $\mathcal {L}$ may coincide with $FO (<)$ or extend it with some standard numeric predicates such as $\textsc {plus}(x,y,z)$, which is true iff $x+y=z$, or even with some operators such as transitive closure or relational primitive recursion.) Let ${\textit{\textbf{q}}}=(\mathcal {O}, \psi (\textit{\textbf{t}}))$ be an OMQ and $\textit{\textbf{Q}}(\textit{\textbf{t}})$ a constant-free $\mathcal {L}$-formula with free variables $\textit{\textbf{t}}$. We call $\textit{\textbf{Q}}(\textit{\textbf{t}})$ an $\mathcal {L}$-rewriting of ${\textit{\textbf{q}}}$ if, for any data instance $\mathcal {A}$, we have $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}) = \{ \varvec{\ell } \subseteq \mathsf {tem}(\mathcal {A}) \mid \mathfrak S_\mathcal {A}\models \textit{\textbf{Q}}(\varvec{\ell })\}$.⁷ We say that ${\textit{\textbf{q}}}$ is $\mathcal {L}$-rewritable if it has an $\mathcal {L}$-rewriting.

Additionally, as a technical tool to construct $\mathcal {L}$-rewritings, we require the following notion of phantom. Given an OMQ ${\textit{\textbf{q}}}= (\mathcal {O},\psi (t))$ with one answer variable t and any integer number $k \in \mathbb {Z}$, by a k-phantom we understand an $\mathcal {L}$-sentence $\varPhi _{{\textit{\textbf{q}}}}^k$ such that $\mathfrak S_\mathcal {A}\models \varPhi _{{\textit{\textbf{q}}}}^k$ iff $\max \mathcal {A}+ k \in \mathsf {ans}^{\mathbb {Z}}({\textit{\textbf{q}}},\mathcal {A})$, for $k > 0$, and $\mathfrak S_\mathcal {A}\models \varPhi _{{\textit{\textbf{q}}}}^k$ iff $k \in \mathsf {ans}^{\mathbb {Z}}({\textit{\textbf{q}}},\mathcal {A})$, for $k < 0$.

We discuss the relevant classes $\mathcal {L}$ of FO-formulas in the Sects. 3 and 5.

Remark 4

In the definition above, we did not allow any constants (numbers) from $\mathbb {Z}$ in rewritings. Note, however, that the MFO$(<)$-formulas $\lnot \exists t'\, (t'< t)$ and $\lnot \exists t'\, (t'>t)$ define the minimal and maximal numbers that occur in any given data instance. In view of this, we can use the constants $\min$ and $\max$ in FO$(<)$-rewritings as syntactic sugar.

Example 5

Consider the OMQ ${\textit{\textbf{q}}}= (\mathcal {O},A(t))$, where $\mathcal {O}$ is the same as in Example 2. It is not hard to see that

$$\begin{aligned} \textit{\textbf{Q}}(t) ~=~ \exists s\,\bigl (A(s) \wedge P(t,s)\bigr )\ \vee \ \exists s\,\bigl (B(s) \wedge Q(t,s)\bigr ) \end{aligned}$$

is a rewriting of ${\textit{\textbf{q}}}$ in MFO$(<)$ extended with the predicates P(t, s) saying that $t - s = 2n$ for some $n \in \mathbb {N}$, and Q(t, s) saying that $t - s = 2n + 1$ for some $n \in \mathbb {N}$. Note that the quantified variable s ranges between $\min \mathcal {A}$ and $\max \mathcal {A}$ in any $\mathfrak S_\mathcal {A}$; in particular, $t \ge s$. Finally, observe that ${\textit{\textbf{q}}}$ is not FO$(<)$-rewritable since properties such as ‘t is even’ are not definable by FO$(<)$-formulas  [64, 79].

FO-rewritability of an OMQ ${\textit{\textbf{q}}}=(\mathcal {O}, \psi (\textit{\textbf{t}}))$ defined above is closely related to the data complexity of the OMQ answering problem for ${\textit{\textbf{q}}}$: given a data instance $\mathcal {A}$ and a tuple $\varvec{\ell }$ of elements from $\mathsf {tem}(\mathcal {A})$, decide whether $\varvec{\ell } \in \mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$. If ${\textit{\textbf{q}}}$ is regarded to be fixed and only $\mathcal {A}$ is the input, we speak of the data complexity of this problem; if both ${\textit{\textbf{q}}}$ and $\mathcal {A}$ are regarded as input, then we speak about the combined complexity. For example, evaluating standard FO-queries (without an ontology) over FO-structures—in other words, the model checking problem—is PSpace-complete for combined complexity and in the class ${\textsc {AC}^0}$ for data complexity⁸ (which is one of the smallest classes in the complexity hierarchy); see, e.g.,  [64, Chapter 6]. It is to be noted that, to measure the data complexity, we should assume that our data instances $\mathcal {A}$ are encoded as strings that can be given as inputs to computational devices such as Turing machines; see  [56, 64] for details. Now, if the OMQ ${\textit{\textbf{q}}}$ is FO$(<)$-rewritable (over data instances represented as such strings), then the OMQ answering problem for ${\textit{\textbf{q}}}$ is in LogTime-uniform ${\textsc {AC}^0}$. In what follows, when discussing various types of FO-rewritablity and the corresponding complexity classes, we do not want to go into the technical details of the string representation of data instances.

For events in asynchronous systems, we need interpretations with a dense order (in this paper, we use $\mathbb {Q}_2$), where FO$(<)$ is not able to express the function $t + a$, for a fixed number $a \in \mathbb {Q}_2$, which is obviously needed in our purging example. To make FO$(<)$ more expressive, we extend it with built-in binary predicates $\delta _{<a}(x,y)$ and $\delta _{= a}(x,y)$, for $a \in \mathbb {Q}^+_2$ (non-negative dyadic numbers), where the former stands for $0 \le x-y < a$ and the latter for $x-y = a$. This language is denoted by $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$ and interpreted in structures of the form

$$\begin{aligned} \mathcal {I}~=~ (\mathbb {T},<, \{\delta _{<a} \mid a \in \mathbb {Q}^+_2\}, \{\delta _{= a}\mid a \in \mathbb {Q}^+_2\}, A_1^\mathcal {I}, A_2^\mathcal {I}, \dots ) \end{aligned}$$

(3)

with a temporal domain $\mathbb {T} \subseteq \mathbb {Q}_2$. In fact, there are two types of semantics for $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$-formulas; cf.  [72]. In one of them, known as the continuous semantics, the temporal domain of $\mathcal {I}$ is always set to $\mathbb {T} = \mathbb {Q}_2$ in the definition (2) of the set of certain answers $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$ to an OMQ ${\textit{\textbf{q}}}$ over a data instance $\mathcal {A}$. In the alternative pointwise (or event) semantics, for each data instance $\mathcal {A}$, we only consider those models of $(\mathcal {O},\mathcal {A})$ in (2) that have the domain $\mathbb {T} = \mathsf {tem}(\mathcal {A})$. We illustrate the difference between these two semantics by an example.

Example 6

Consider the OMQ ${\textit{\textbf{q}}}=(\mathcal {O}, A(t))$ with

Suppose first that $\mathcal {A}_1 = \{B(0),B(1/2), C(3/2)\}$ and the semantics is pointwise. In this case, possible models of $(\mathcal {O},\mathcal {A}_1)$ have domain $\{0,1/2,3/2\}$, and so we obtain $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}_1) = \{3/2\}$ because the first axiom gives $B'$ at 0 and then at 1/2, from which we derive A at 3/2 by the second axiom.

Note that $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}_2) = \emptyset$ for $\mathcal {A}_2 = \{B(0),C(3/2)\}$. Under the continuous semantics, we cannot derive $B'$ at 0 and 1/2 because there exist time instants before 0 and between 0 and 1/2 where $B'$ can be false. Thus, in this case, $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}_1) = \emptyset$.

3 Ontology-Mediated Queries with LTL-Ontologies

In the previous section, we argued that monadic first-order logic MFO$(<)$ provides a natural formalism for ontology-mediated queries in the synchronous case, where the time flow is discrete $(\mathbb {Z},<)$. Temporal instantaneous events can be described then by MFO$(<)$-formulas with one free variable. We recall now that, by the celebrated Kamp Theorem  [57, 74], those formulas have exactly the same expressive power as the formulas of (propositional) linear temporal logic LTL, which are built from propositional variables using the Booleans and the temporal operators (at the next moment of time), $\Diamond _{\!\scriptscriptstyle F}$ (eventually), (always in the future), $\mathcal {U}$ (until), and their past-time counterparts (at the previous moment), $\Diamond _{\!\scriptscriptstyle P}$ (some time in the past), (always in the past) and $\mathcal {S}$ (since); see  [34, 40, 68] and further references therein.

We give the semantics of LTL-formulas via their standard MFO$(<)$-translation $^\dag$ defined inductively as follows. For an atomic proposition A, we set $A^\dag = A(t)$. The translation $^\dag$ commutes with the Booleans in the sense that $(\varkappa _1 \wedge \varkappa _2)^\dag = \varkappa _1^\dag \wedge \varkappa _2^\dag$, $(\lnot \varkappa )^\dag = \lnot (\varkappa ^\dag )$, etc. Finally, for the temporal operators, we set:

and symmetric ally for the ‘past’ operators, for instance, , $(\Diamond _{\!\scriptscriptstyle P}\varkappa )^\dag = \exists t'\, \big ( (t > t') \wedge \varkappa ^\dag \{t'/t\}\big )$, etc. In the translation above, $t'$ and $t''$ are fresh variables and $\{t'/t\}$ means a substitution that replaces t with $t'$. Given a temporal interpretation $\mathcal {I}$ and an LTL-formula $\varkappa$, we define the extension $\varkappa ^\mathcal {I}$ of $\varkappa$ in $\mathcal {I}$ as the set of integers $\varkappa ^\mathcal {I}= \{n \in \mathbb {Z} \mid \mathcal {I}\models \varkappa ^\dag (n)\}$.

In this section, we introduce a number of fragments of LTL as possible temporal ontology languages and discuss FO-rewritability of various types of OMQs with ontologies in those fragments. Having in mind the OBDA application area for these languages, we somewhat modify the standard LTL terminology. For instance, instead of propositional variables, we prefer to speak about atomic concepts (similarly to concept names in Description Logic).

Thus, in this paper, we think of the alphabet of LTL as a countably infinite set of atomic concepts $A_i$, for $i < \omega$. Basic temporal concepts, C, are defined by the grammar

(4)

An $\textit{LTL}$-ontology, $\mathcal {O}$, is a finite set of clauses of the form

$$\begin{aligned} C_1 \wedge \dots \wedge C_k ~\rightarrow ~ C_{k+1} \vee \dots \vee C_{k+m}, \end{aligned}$$

(5)

where $k,m \ge 0$ and the $C_i$ are basic temporal concepts. As usual, we denote the empty conjunction ($k=0$) by $\top$ and the empty disjunction ($m=0$) by $\bot$. We often refer to the clauses in $\mathcal {O}$ as (ontology) axioms. Intuitively, the axioms are supposed to hold at every moment of time. In other words, (5) is just a shortcut for the MFO$(<)$-sentence

$$\begin{aligned} \forall t \, ( C_1^\dag \wedge \dots \wedge C_k^\dag ~\rightarrow ~ C_{k+1}^\dag \vee \dots \vee C_{k+m}^\dag ). \end{aligned}$$

(6)

It is true in an interpretation $\mathcal {I}$ iff

$$ C_1^\mathcal {I}\cap \dots \cap C_k^\mathcal {I}~\subseteq ~ C_{k+1}^\mathcal {I}\cup \dots \cup C_{k+m}^\mathcal {I}. $$

An ontology $\mathcal {O}$ entails a clause (5) if this clause is true in every model $\mathcal {I}$ of $\mathcal {O}$.

We classify ontologies by the shape of their axioms⁹ and the temporal operators that occur in them. Let and . By an $\textit{LTL}_{\textit{\textbf{c}}}^{{\textit{\textbf{o}}}}$-ontology we mean any LTL-ontology whose clauses satisfy the following restrictions on k and m in (5) indicated by ${\textit{\textbf{c}}}$:

• horn: $m\le 1$,

• krom: $k + m\le 2$,

• core: $k + m\le 2$ and $m \le 1$,

• bool: any $k,m \ge 0$,

and may only contain occurrences of the (future and past) temporal operators indicated in ${\textit{\textbf{o}}}$ (for example, ${\textit{\textbf{o}}}= \Box$ means that only and may occur in the temporal concepts). Note that an $\textit{LTL}_{\textit{\textbf{c}}}^{{\textit{\textbf{o}}}}$-ontology of any type may contain disjointness axioms of the form $C_1 \wedge C_2 \rightarrow \bot$. Although both $\textit{LTL}_\textit{krom}^{{\textit{\textbf{o}}}}$- and $\textit{LTL}_\textit{core}^{{\textit{\textbf{o}}}}$-ontologies may only have binary clauses as axioms (with at most two concepts), only the former are allowed to contain universal covering axioms such as $\top \rightarrow C_1 \vee C_2$; in other words, $\textit{core}= \textit{krom}\cap \textit{horn}$.

The definition above identifies a seemingly very restricted set of LTL-formulas as possible ontology axioms. For example, it completely disallows the use of the standard temporal operators $\Diamond _{\!\scriptscriptstyle F}$ (sometime in the future), $\Diamond _{\!\scriptscriptstyle P}$ (sometime in the past), $\mathcal {U}$ (until) and $\mathbin {\mathcal {S}}$ (since). Whether or not these operators can be somehow expressed in a given fragment $\textit{LTL}_{\textit{\textbf{c}}}^{{\textit{\textbf{o}}}}$ (in the context of OMQ answering) depends on ${\textit{\textbf{c}}}$ and ${\textit{\textbf{o}}}$. The following example clarifies the picture.

Example 7

Observe first that the clause $\Diamond _{\!\scriptscriptstyle P}A \rightarrow B$ is equivalent to the clause . Also, the former clause can be expressed in by three clauses: , and $X \rightarrow B$, for a fresh atomic concept X that is not supposed to occur in any data instances.

To see why, we need a few definitions. By the signature of an ontology we mean the set of atomic concepts that occur in it. An ontology $\mathcal {O}'$ is called a model conservative extension of an ontology $\mathcal {O}$ if $\mathcal {O}'\models \mathcal {O}$, the signature of $\mathcal {O}$ is contained in the signature of $\mathcal {O}'$, and every model of $\mathcal {O}$ can be expanded to a model of $\mathcal {O}'$ by providing interpretations of the fresh symbols of $\mathcal {O}'$ and leaving the domain and the interpretation of the symbols in $\mathcal {O}$ unchanged. Observe that if ${\textit{\textbf{q}}}= (\mathcal {O}, \varkappa )$ is an OMQ and $\mathcal {O}'$ a model conservative extension of $\mathcal {O}$, then the certain answers to ${\textit{\textbf{q}}}$ over a data instance $\mathcal {A}$ in the signature of $\mathcal {O}$ coincide with the certain answers to ${\textit{\textbf{q}}}' = (\mathcal {O}',\varkappa )$ over $\mathcal {A}$. Thus, any FO-rewriting of ${\textit{\textbf{q}}}'$ is also an FO-rewriting of ${\textit{\textbf{q}}}$.

The ontology $\mathcal {O}'$ obtained from $\mathcal {O}$ by replacing $\Diamond _{\!\scriptscriptstyle P}A \rightarrow B$ with , and $X \rightarrow B$ is a model conservative extension of $\mathcal {O}$, and so we can use it for OBDA in place of $\mathcal {O}$.

The clause $A \rightarrow \Diamond _{\!\scriptscriptstyle P}B$ cannot be expressed in any of the $\textit{LTL}^{\textit{\textbf{o}}}_\textit{core}$ fragments but can be expressed in by and $\top \rightarrow X \vee B$. The clauses of the form $A \wedge B \rightarrow C$ are in the $\textit{LTL}^{\textit{\textbf{o}}}_\textit{horn}$ fragments but not in $\textit{LTL}^{\textit{\textbf{o}}}_\textit{core}$ or $\textit{LTL}^{\textit{\textbf{o}}}_\textit{krom}$. The clause $A\, \mathcal {U}B \rightarrow C$ can be expressed in by and and $X \rightarrow C$, also for a fresh X. The clause $A \rightarrow B\, \mathcal {U}C$ can be expressed in using the well-known fixed-point unfolding of $B\mathcal {U}C$ as , which gives rise to 4 clauses $A \rightarrow X$, , and $A \rightarrow \Diamond _{\!\scriptscriptstyle F}C$ (the $\Diamond _{\!\scriptscriptstyle F}$ in the last clause can be replaced with as described above).

Exercise 8

Imagine that we would like to query the data about the status of a research article submitted to a certain journal. We are interested in temporal events such as $\textit{Submission}$, $\textit{Notification}$, $\textit{Accept}$, $\textit{Reject}$, $\textit{Revise}$, $\textit{Publication}$. Our background knowledge about these events can be formulated as an LTL-ontology $\mathcal {O}$ with the axioms below. We invite the reader to transform those axioms to the required form (5) using common sense and the previous example.

$$\begin{aligned}&\textit{Notification} \leftrightarrow \textit{Reject} \vee \textit{Accept} \vee \textit{Revise},\end{aligned}$$

(7)

$$\begin{aligned}&\textit{Reject}\wedge \textit{Accept} \rightarrow \bot , \quad \textit{Revise}\wedge \textit{Accept} \rightarrow \bot , \quad \textit{Reject}\wedge \textit{Revise} \rightarrow \bot \end{aligned}$$

(8)

(at any moment of time, every notification is either a reject, accept, or revision notification, and it can only be one of them)

$$\begin{aligned} P \rightarrow \lnot \Diamond _{\!\scriptscriptstyle P}P \wedge \lnot \Diamond _{\!\scriptscriptstyle F}P \end{aligned}$$

(9)

(for every event P we are interested in except $\textit{Notification}$ and $\textit{Revise}$, P can happen only once for any article)

$$\begin{aligned}&\textit{Publication} \rightarrow \Diamond _{\!\scriptscriptstyle P}\textit{Accept}, \quad \textit{Notification} \rightarrow \Diamond _{\!\scriptscriptstyle P}\textit{Submission},\end{aligned}$$

(10)

$$\begin{aligned}&\textit{Accept} \rightarrow \Diamond _{\!\scriptscriptstyle F}\textit{Publication}, \quad \textit{Submission} \rightarrow \Diamond _{\!\scriptscriptstyle F}\textit{Notification},\end{aligned}$$

(11)

$$\begin{aligned}&\textit{Revise} \rightarrow \Diamond _{\!\scriptscriptstyle F}\textit{Notification} \end{aligned}$$

(12)

(obvious necessary pre-conditions for publication and notification and also the post-conditions—eventual consequences—of acceptance, submission and a revision notification; for simplicity, we assume that after a revision notification the authors always eventually receive a notification regarding a revised version)

$$\begin{aligned} \textit{Accept} \vee \textit{Reject} \rightarrow \lnot \Diamond _{\!\scriptscriptstyle F}\textit{Notification} \end{aligned}$$

(13)

(acceptance and rejection notifications are final).

We distinguish between three types of ontology-mediated queries (OMQs) with LTL-ontologies:

• Atomic OMQs (or OMAQs, for short) take the form ${\textit{\textbf{q}}}= (\mathcal {O}, A(t))$ with an atomic concept A.

• A positive ontology-mediated instance query (OMPIQ) $(\mathcal {O}, \varkappa (t))$ with a positive LTL-formula $\varkappa$, which is constructed from atoms in the standard way but using $\wedge$ and $\vee$ only (or an equivalent MFO$(<)$-formula with one free variable t, which will be discussed below).

• Quasi-positive OMQs (or OMQPQs) ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ have a quasi-positive MFO(<)-formula $\psi (\textit{\textbf{t}})$, which is recursively constructed using $\wedge$, $\vee$, $\forall$, $\exists$, as well as the guarded universal quantification of the form

  $$\begin{aligned} \forall y \, \big ( (x< y< z) \rightarrow \varphi \big ),\qquad \forall y \, \big ( (x< y) \rightarrow \varphi \big ), \qquad \forall y \, \big ( (y < z) \rightarrow \varphi \big ), \end{aligned}$$

  (14)

  where $\varphi$ is a quasi-positive MFO$(<)$-formula.

• Finally, general OMQs ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ may have arbitrary MFO(<)-formulas $\psi (\textit{\textbf{t}})$.

Example 9

Consider $\mathcal {O}$ from Exercise 8. Then $(\mathcal {O}, \textit{Revise}(t))$ is an OMAQ asking when the paper was sent back for revision. As an example of OMPIQ, consider $(\mathcal {O}, (\Diamond _{\!\scriptscriptstyle P}\textit{Revise}\wedge \textit{Accept})(t))$ asking when (and whether) the paper was accepted after revision. As an example of OMQPQ, consider $(\mathcal {O}, \psi (t,t'))$, where

$$\begin{aligned} \psi (t,t') ~=~ \exists x \, \big ( (t< x < t') \wedge \textit{Revise}(x)\big ) \wedge \textit{Submission}(t) \wedge \textit{Accept}(t'), \end{aligned}$$

looking for time intervals $[t,t']$ over which a submitted article underwent at least one revision before acceptance. Finally, an example of a (general) OMQ is $(\mathcal {O}, \psi (t))$ with

$$\begin{aligned} \psi (t)= \textit{Submission}(t) \wedge \lnot \exists t'\, ((t'>t) \wedge ( \textit{Accept} (t') \vee \textit{Reject}(t') ) ). \end{aligned}$$

that checks if and when the article was submitted without accept or reject decision so far.

OMAQs are the simplest and arguably most convenient queries from the user’s point of view as they presuppose that definitions of relevant events should be provided by the ontology. However, they are not suitable in situations when more than one answer variable is needed as, for example, in the query ‘find all timestamps $t_1$ and $t_3$ with $t_1 < t_3$, for which there is $t_2$ such that $t_1< t_2 < t_3$ and some event (say, the temperature is lower than $50\,^\circ$C) happens everywhere in the interval $[t_1,t_2)$ and some other event (say, the temperature is higher than $90\,^\circ$C) happens everywhere in the interval $[t_2,t_3]$’. As we shall see below, arbitrary OMQs have worse computational properties compared to OMQPQs. In fact, one can show the following version of Kamp’s Theorem: every consistent quasi-positive MFO(<)-formula $\psi (t)$ with one free variable t is equivalent over $(\mathbb {Z},<)$ to a positive LTL-formula constructed using any temporal operators and the ‘positive’ Boolean connectives $\wedge$ and $\vee$ only  [10]. Another important semantic characterisation of quasi-positive formulas is as follows. Given temporal interpretations $\mathcal {I}_1$ and $\mathcal {I}_2$, we write $\mathcal {I}_1 \preceq \mathcal {I}_2$ if $A^{\mathcal {I}_1} \subseteq A^{\mathcal {I}_2}$, for every atomic concept A. An MFO$(<)$-formula $\psi (\textit{\textbf{t}})$ is called monotone if $\mathcal {I}_1 \models \psi (\textit{\textbf{n}})$ and $\mathcal {I}_1 \preceq \mathcal {I}_2$ imply $\mathcal {I}_2 \models \psi (\textit{\textbf{n}})$, for any tuple $\textit{\textbf{n}}$ in $\mathbb {Z}$. Now, one can show  [10] that an MFO$(<)$-formula is monotone iff it is equivalent over $(\mathbb {Z},<)$ to a quasi-positive MFO$(<)$-formula.

Let us now focus on rewritability of LTL OMQs. Is there a ‘standard’ query language into which any such OMQ can be rewritten? The following example shows that FO$(<)$, even extended with arbitrary arithmetic predicates, is not powerful enough for this purpose:

Example 10

Consider the OMAQ ${\textit{\textbf{q}}}= (\mathcal {O},B_0)$, where $\mathcal {O}$ consists of the axioms

For every binary word $\textit{\textbf{e}} = e_1\dots e_{n} \in \{0,1\}^n$, we take the data instance $\mathcal {A}_{\textit{\textbf{e}}} = \{\,B_0(0)\,\} \cup \{\, A_{e_i}(i) \mid 0 < i \le n\,\}$. It is not hard to check that n is a certain answer to ${\textit{\textbf{q}}}$ over $\mathcal {A}_{\textit{\textbf{e}}}$ iff the number of 1s in $\textit{\textbf{e}}$ is even (PARITY): intuitively, the word is processed starting from the minimal timestamp and moving towards the maximal one, and the first axiom preserves $B_i$ if the current symbol is 0, whereas the second axiom toggles $B_i$ if the current symbol is 1. As PARITY is not in ${\textsc {AC}^0}$  [39], it follows that ${\textit{\textbf{q}}}$ is not FO-rewritable even if arbitrary numeric predicates are allowed in rewritings.

A natural and more expressive target language for rewritings is FO(RPR) that extends FO with the successor relation and relational primitive recursion (RPR, for short). Evaluation of FO(RPR)-formulas is known to be $\textsc {NC}^1$-complete¹⁰ for data complexity  [32], with ${\textsc {AC}^0}\subsetneq {{\textsc {NC}^1}}\subseteq \textsc {L}$. We remind the reader that, using RPR, we can construct formulas such as

$$\begin{aligned} \varPhi ~=~ \left[ \begin{array}{l} Q_{1}(\textit{\textbf{z}}_1,t) \equiv \varTheta _1\big (\textit{\textbf{z}}_1,t,Q_1(\textit{\textbf{z}}_1,t-1),\dots ,Q_n(\textit{\textbf{z}}_n,t-1)\big )\\ \dots \\ Q_{n}(\textit{\textbf{z}}_n,t) \equiv \varTheta _n\big (\textit{\textbf{z}}_n,t,Q_1(\textit{\textbf{z}}_1,t-1),\dots ,Q_n(\textit{\textbf{z}}_n,t-1)\big ) \end{array}\right] \ \varPsi , \end{aligned}$$

where the part of $\varPhi$ within $[\dots ]$ defines recursively, via the FO(RPR)-formulas $\varTheta _i$, the interpretations of the predicates $Q_i$ in the FO(RPR)-formula $\varPsi$ (see Example 11 below). Note that the recursion starts at $t=0$ and assumes that $Q_{i}(z,-1)$ is false for all $Q_{i}$, $i=1,\dots ,n$, and all z. Thus, the truth value of $Q_{i}(z,0)$ is computed by substituting falsehood $\bot$ for all $Q_{i}(z,-1)$. For every $t=1,2,\dots$, the recursion is then applied in the obvious way.

We illustrate relational primitive recursion by a concrete example.

Example 11

The OMQ ${\textit{\textbf{q}}}= (\mathcal {O},B_0)$ from Example 10 can be rewritten to the following FO(RPR)-formula:

$$\begin{aligned} \textit{\textbf{Q}}(t) ~=~ \left[ \begin{array}{l} Q_{0}(t) \equiv \varTheta _0\\ Q_{1}(t) \equiv \varTheta _1 \end{array}\right] \ Q_0(t), \end{aligned}$$

where, for $k=0,1$,

$$\begin{aligned} \varTheta _k(t, Q_{0}(t-1), Q_{1}(t-1)) ~=~ B_k(t) \ \ \vee \ \bigl (Q_k(t-1)\,\wedge \, A_0(t)\bigr ) \ \ \vee \ \ \bigl (Q_{1-k}(t-1)\,\wedge \, A_1(t)\bigr ). \end{aligned}$$

As noted above, the recursion starts from the minimal timestamp 0 in the data instance (with $Q_i(-1)$ regarded as false) and proceeds to the maximal one.

The next theorem shows that all $\textit{LTL}$ OMQs can be rewritten into FO(RPR). As follows from  [32, Proposition 4.3], this means that we can also rewrite our OMQs into the language MSO$(<)$ of monadic second-order formulas that are built from atoms of the form A(t) and $t < t'$ using the Booleans, first-order quantifiers $\forall t$ and $\exists t$, and second-order quantifiers $\forall A$ and $\exists A$  [28].

Remark 12

It is worth reminding the reader (see  [33, 78, 79] for details) that, by the Büchi–Elgot–Trakhtenbrot Theorem  [28, 35, 81], $MSO (<)$-sentences define exactly the class of regular languages. FO(RPR), extended with the predicates $\textsc {plus}$ and $\textsc {times}$ or, equivalently, with one predicate bit  [56], captures exactly the languages in $\textsc {NC}^1$ (which are not necessarily regular)  [32].

Theorem 13

Every $\textit{LTL}$ OMQ is FO(RPR)- and MSO$(<)$-rewritable, and so can be answered in $\textsc {NC}^1$ for data complexity.

Note that the SQL:1999 ISO standard contains a WITH RECURSIVE construct that allows users to implement various FO-queries with relational primitive recursion such as the query in Example 11, which cannot be expressed in FO without recursion.

The next example shows that our OMQs can simulate arbitrary finite automata, and so FO(RPR) appears to be an optimal target language for rewritings in general (since there exist $\textsc {NC}^1$-complete regular languages).

Example 14

Let $\mathfrak A$ be a DFA with a tape alphabet $\Gamma$, a set of states Q, an initial state $q_0\in Q$, an accepting state $q_1\in Q$ and a transition function $\rightarrow$: we write $q \rightarrow _e q'$ if $\mathfrak {A}$ moves to a state $q'\in Q$ from a state $q\in Q$ while reading $e\in \Gamma$. (Without loss of generality we assume that $\mathfrak A$ has only one accepting state.) We take atomic concepts $A_e$ for tape symbols $e\in \Gamma$ and atomic concepts $B_q$ for states $q\in Q$, and consider the OMAQ ${\textit{\textbf{q}}}= (\mathcal {O},B_{q_0})$, where

For any input word $\textit{\textbf{e}}=(e_1\dots e_{n})\in \Gamma ^*$, we set

$$\begin{aligned} \mathcal {A}_{\textit{\textbf{e}}} \ \ = \ \ \bigl \{\,B_{q_0}(0)\,\bigr \} \ \ \cup \ \ \bigl \{\,A_{e_i}(i) \mid 0 < i \le n\,\bigr \}. \end{aligned}$$

It is easy to see that $\mathfrak A$ accepts $\textit{\textbf{e}}$ iff $\max (\mathcal {A}_{\textit{\textbf{e}}}) \in \mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}_{\textit{\textbf{e}}})$. We invite the reader to show that $\mathfrak A$ accepts $\textit{\textbf{e}}$ iff $0 \in \mathsf {ans}({\textit{\textbf{q}}}',\mathcal {A}_{\textit{\textbf{e}}})$, where ${\textit{\textbf{q}}}' = (\mathcal {O}',\psi (t))$,

$$\begin{aligned} \mathcal {O}' \ \&= \ \ \bigl \{ \, \overline{B}_q \wedge B_q \rightarrow \bot , \ \top \rightarrow B_q \vee \overline{B}_q \ \mid \ q \in Q \, \bigr \}, \end{aligned}$$

and $\psi (t)$ is the standard FO-translation of the LTL-formula

where $\Diamond _{\!\scriptscriptstyle P}^{\scriptscriptstyle +} C$ is an abbreviation for $C \vee \Diamond _{\!\scriptscriptstyle P}C$. (Hint: $\overline{B}_q$ represents the complement of $B_q$, and $\varkappa$ is equivalent to formula , where is an abbreviation for .)

Now we present classes of OMQs that are rewritable to FO-formulas without recursion. Namely, we have rewritings of two types. One type is the usual FO$(<)$-formulas. The other one comprises FO$(<,\equiv _{\mathbb {N}})$-formulas that can use numeric predicates $x \equiv 0\, (\text {mod}\ n)$, for any fixed $n \in \mathbb {N}$. (As shown in  [16], FO$(<,\equiv _{\mathbb {N}})$ is exactly the class of regular languages in ${\textsc {AC}^0}$.)

Exercise 15

Note that FO(RPR) does not contain $x < y$ or $x \equiv 0\, (\text {mod}\ n)$, for $n > 1$, as atoms. We invite the reader to show that both of them can be expressed in FO(RPR) in the sense that (i) there exists an FO(RPR)-formula $\varphi _<(x,y)$ such that $\mathfrak S \models \varphi _<(a,b)$ iff $\mathfrak S \models a < b$, for any FO-structure $\mathfrak S$ and a, b in its domain; and (ii) for any $n > 1$, there exists an FO(RPR)-formula $\varphi _n(x)$ such that $\mathfrak S \models \varphi _n(a)$ iff $\mathfrak S \models a \equiv 0\, (\text {mod}\ n)$, for any FO-structure $\mathfrak S$ and a in its domain. (A solution to (i) can be found in  [32] and a solution to (ii) in  [10].) As a consequence, we obtain that, for every FO$(<,\equiv _{\mathbb {N}})$-formula, there is an equivalent FO(RPR)-formula.

Theorem 16

Any OMAQ is FO$(<,\equiv _{\mathbb {N}})$-rewritable, and so can be answered in $\textsc {AC}^0$ for data complexity.

Proof

(Sketch). Suppose ${\textit{\textbf{q}}}= (\mathcal {O},A)$ is an OMAQ. By a literal, L, we mean an atomic concept in ${\textit{\textbf{q}}}$ or its negation. We use in place of if $n > 0$, L if $n = 0$, and if $n < 0$. We write if in every model $\mathcal {I}$ of $\mathcal {O}$. For any data instance $\mathcal {A}$ consistent with $\mathcal {O}$, we have:

Given literals L and $L'$, let $\mathfrak A_{L,L'}$ be an NFA whose tape alphabet is $\{0\}$, the states are the literals, with L initial and $L'$ accepting, and whose transitions are of the form $L_1 \rightarrow _0 L_2$, for (without loss of generality we assume that $\mathcal {O}$ does not contain nested ). It is easy to see that $\mathfrak A_{L,L'}$ accepts $0^k$ ($k > 0$) iff . By  [31, 80], there are $N = O(|\mathfrak A_{L,L'}|^2)$ arithmetic progressions $a_i + b_i\mathbb {N} = \{ a_i + b_i \cdot m \mid m\ge 0 \}$, $1 \le i \le N$, such that $0 \le a_i, b_i \le |\mathfrak A_{L,L'}|$ and $\mathfrak {A}_{L,L'}$ accepts $0^k$ iff $k \in a_i + b_i\mathbb {N}$ for some i, $1\le i \le N$. These progressions give rise to the FO-rewriting we need. To illustrate, suppose ${\textit{\textbf{q}}}= (\mathcal {O},A)$ and

The NFA $\mathfrak A_{B,A}$ (more precisely, the states reachable from B) is shown below,

and for $L \in \{ A, C, D, E\}$, $\mathfrak A_{L, A}$ is the same NFA but with the initial state L. It is readily seen that $\mathfrak A_{\smash {B,A}}$ accepts $0^k$ iff $k \in 3 + 2 \mathbb {N}$, which can be described by the formula

$$\begin{aligned} \varphi _{B,A}(t) = \exists s\, \bigl (B(s) \ \wedge \ \bigl (t - s \in a + b\mathbb {N}\bigr )\bigr ), \end{aligned}$$

where $a =3$, $b = 2$, and $\bigl (t - s \in 3 + 2\mathbb {N}\bigr )$ is an abbreviation for

$$\begin{aligned} \exists n \, [&(n = s+3) \wedge \bigl (((n \equiv 0\, (\text {mod}\ 2)) \wedge (t \equiv 0\, (\text {mod}\ 2)))\vee {}\\&\exists n', t'\, ( (n' = n+1) \wedge (t' = t+1) \wedge (n' \equiv 0\, (\text {mod}\ 2)) \wedge (t' \equiv 0\, (\text {mod}\ 2))) \bigr )] \end{aligned}$$

(the reader is invited to provide the definition of $\bigl (t - s \in a + b\mathbb {N}\bigr )$ for arbitrary a and b). Similarly, for $\mathfrak A_{E, A}$, we have $a = b =2$. (Note that in general more than one progression is needed to characterise automata $\mathfrak A_{L,A}$.) To obtain an FO$(<,\equiv _{\mathbb {N}})$-rewriting of ${\textit{\textbf{q}}}$, we take a disjunction of $\varphi _{L,A}(t)$, for all literals L. One can also construct any phantom $\varPhi _{(\mathcal {O}, A)}^k$ in FO$(<,\equiv _{\mathbb {N}})$.   $\square$

Theorem 17

Any $\textit{LTL}_\textit{bool}^\Box$ OMAQ is FO$(<)$-rewritable, and so can be answered in $\textsc {AC}^0$ for data complexity.

Proof

(Sketch). Given an $\textit{LTL}_\textit{bool}^\Box$-ontology $\mathcal {O}$, we construct an NFA $\mathfrak A$ that takes as input a data instance $\mathcal {A}$ written as the word $\mathcal {A}_0, \dots , \mathcal {A}_k$, where $k = \max \mathcal {A}$ and $\mathcal {A}_i = \{ A \mid A(i) \in \mathcal {A}\}$. Let $\Sigma$ be the set of temporal concepts in $\mathcal {O}$ and their negations. Each state of $\mathfrak A$ is a maximal set $S \subseteq \Sigma$ that is consistent with $\mathcal {O}$; let $\textit{\textbf{S}}$ be the set of all such states. For $S,S' \in \textit{\textbf{S}}$ and a tape symbol (set of concept names) X, we set $S \rightarrow _X S'$ just in case $X \subseteq S'$, iff , and iff . A state $S \in \textit{\textbf{S}}$ is accepting if $\mathfrak A$ has an infinite ‘ascending’ chain $S \rightarrow _\emptyset S_1 \rightarrow _\emptyset \dots$; S is initial if $\mathfrak A$ has an infinite ‘descending’ chain $\dots \rightarrow _\emptyset S_1 \rightarrow _\emptyset S$. The NFA $\mathfrak A$ simulates $\mathcal {O}$ in the following sense: for any ABox $\mathcal {A}$, concept name A and $\ell \in \mathbb {Z}$, we have $\ell \in \mathsf {ans}^{\mathbb {Z}}((\mathcal {O},A),\mathcal {A})$ iff $\mathfrak A$ does not contain an accepting path $S_0 \rightarrow _{X_1} \dots \rightarrow _{X_m} S_m$ ($S_0$ initial and $S_m$ accepting) such that $A \notin S_\ell$, $X_{i+j} = \mathcal {A}_j$ if $0 \le j \le k$, and $X_j = \emptyset$ otherwise, for some i, $0 < i \le m - k$.

Define an equivalence relation, $\sim$, on $\textit{\textbf{S}}$ by taking $S \sim S'$ iff $S = S'$ or $\mathfrak A$ has a cycle with both S and $S'$. Let [S] be the $\sim$-equivalence class of S. One can check that $S \rightarrow _X S'$ implies $S_1 \rightarrow _X S'$, for any $S_1 \in [S]$. Let $\mathfrak A'$ be the NFA with states [S], for $S \in \textit{\textbf{S}}$, and transitions $[S] \rightarrow _X [S']$ iff $S_1 \rightarrow _X S'_1$, for some $S_1 \in [S]$ and $S'_1 \in [S']$. The initial (accepting) states of $\mathfrak A'$ are all [S] with initial (accepting) S. The NFA $\mathfrak A'$ also simulates $\mathcal {O}$ and contains no cycles other than trivial loops, which makes it possible to express the simulation condition by an FO$(<)$-formula. For example, $\mathfrak A'$ for is shown below, where all states are initial and accepting, and negated concepts omitted:

Let ${\textit{\textbf{q}}}= (\mathcal {O},C)$. Take all accepting paths $\pi$ in $\mathfrak A'$ with pairwise distinct states at least one of which has a set without C. Thus, for $\pi = [S_1] \rightarrow _{\{A\}} [S_2] \rightarrow _{\emptyset } [S_3]$, a set in $[S_3]$ has no C, and the simulation condition for $\pi$, which makes sure that $\lnot C$ holds at t, can be written as

where $\mathsf {sym}_{\{A\}}(t) = A(t) \wedge \lnot B (t) \wedge \lnot C(t)$ and $\mathsf {sym}_{\emptyset } (t) = \lnot A(t) \wedge \lnot B (t) \wedge \lnot C(t)$ define transitions $\rightarrow _{\smash {\{A\}}}$ and $\rightarrow _{\smash {\emptyset }}$ in $\pi$, and $\mathsf {loop}_{[S_1]} = \top$, $\mathsf {loop}_{[S_3]} = \lnot A(t)$ and $\mathsf {loop}_{[S_2]} = \bot$ say that $[S_1]$ and $[S_3]$ have loop transitions with any input and any input but A, respectively, but $[S_2]$ has no loop. To obtain an FO$(<)$-rewriting of ${\textit{\textbf{q}}}$, we take a disjunction of such formulas for all accepting paths $\pi$ in $\mathfrak {A}'$ and negate it. It is also possible to construct any phantom $\varPhi _{(\mathcal {O}, A)}^k$ in FO$(<)$.   $\square$

Theorem 18

Any OMAQ is FO$(<,\equiv _{\mathbb {N}})$-rewritable, and so can be answered in $\textsc {AC}^0$ for data complexity.

Proof

(Sketch). The proof utilises the monotonicity of the $\Box$ operators, similarly to the proof of Theorem 17. However, the latter relies on partially-ordered NFAs accepting the models of $(\mathcal {O}, \mathcal {A})$, which do not work in the presence of . Our key observation here is that every model of $(\mathcal {O}, \mathcal {A})$ has at most $O(|\mathcal {O}|)$ timestamps such that the same $\Box$-concepts hold between any two nearest of them. The placement of these timestamps and their concept-types can be described by an FO$(<)$-formula. However, to check whether these types are compatible (i.e., satisfiable in some model), we require FO$(<,\equiv _{\mathbb {N}})$-formulas similar to those in the proof of Theorem 16.   $\square$

So far, we have considered the simplest class of OMQs with atomic queries. But what if we are interested in spotting complex events whose definitions are not provided by the available ontology? Or what if we need queries with multiple answer variables? Can we still rewrite some of the resulting OMQs into FO-queries without recursion? First, observe that we cannot use arbitrary MFO-formulas as queries if we want to achieve FO-rewritability without recursion. This is the case already for OMQs with empty ontologies as shown by Example 14. It also follows from the same example that OMQs ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ with monotone (quasi-positive) $\psi$ and $\mathcal {O}$ containing only binary disjunctions, can simulate an arbitrary DFA.

On the other hand, we show now how to obtain a strong positive rewritability result for OMQs with a Horn ontology and a monotone query. The key property of Horn ontologies required in the proof of this result is the following fact, which is well known and documented in the Prolog and datalog settings  [1, 4]. The intersection of two interpretations $\mathcal {I}_1$ and $\mathcal {I}_2$ is the interpretation $\mathcal {I}_3$ such that $A^{\mathcal {I}_3} = A^{\mathcal {I}_1} \cap A^{\mathcal {I}_2}$, for every atomic concept A.

Example 19

Consider $\mathcal {I}_1$ with $A^{\mathcal {I}_1} = \{0, 5\}$, $B^{\mathcal {I}_1} = \{n \in \mathbb {Z} \mid n > 0\}$ and $\mathcal {I}_2$ with $A^{\mathcal {I}_2} = \{-5, 0\}$, $B^{\mathcal {I}_2} = \mathbb {Z}$. Then the intersection of $\mathcal {I}_1$ and $\mathcal {I}_2$ is $\mathcal {I}_3$ with $A^{\mathcal {I}_3} = \{0\}$, $B^{\mathcal {I}_3} = \{n \in \mathbb {Z} \mid n > 0\}$.

In general, if we take a pair of models of $(\mathcal {O}, \mathcal {A})$, their intersection does not need to be a model of $(\mathcal {O}, \mathcal {A})$. The reader is invited to verify this on the simple KB $(\{A \rightarrow B \vee C\}, \{A(0)\})$. However, for $\mathcal {O}$ in , the intersection of models of $(\mathcal {O}, \mathcal {A})$ will be always a model of $(\mathcal {O}, \mathcal {A})$, too. Indeed, in Example 19 both $\mathcal {I}_1$ and $\mathcal {I}_2$ are models of and so is their intersection $\mathcal {I}_3$. The canonical (or minimal) model $\mathcal{C}_{\mathcal {O},\mathcal {A}}$ of $(\mathcal {O}, \mathcal {A})$, is the intersection of all the models of $(\mathcal {O}, \mathcal {A})$. For , the canonical model is $\mathcal {I}_3$ from Example 19.

Theorem 20

Let ${\textit{\textbf{q}}}= (\mathcal {O}, \psi (\textit{\textbf{t}}))$ be an OMQPQ with an -ontology $\mathcal {O}$ and let $\mathcal {L}$ be FO$(<)$ or FO$(<,\equiv _{\mathbb {N}})$. Suppose that, for each atomic A in $\psi$,

• every OMAQ $(\mathcal {O}, A)$ is $\mathcal {L}$-rewritable

• there exists a phantom $\varPhi _{(\mathcal {O}, A)}^k$ in $\mathcal {L}$, for every $k \in \mathbb {Z}$

Then, $(\mathcal {O}, \psi (\textit{\textbf{t}}))$ is $\mathcal {L}$-rewritable.

Proof

(Sketch). To simplify presentation, we assume that $\mathcal {O}$ does not contain $\bot$. The proof relies on the fact that, for any $\mathcal {A}$, there exists a canonical model $\mathcal{C}_{\mathcal {O},\mathcal {A}}$ of $(\mathcal {O},\mathcal {A})$. Then, using the monotonicy of $\psi$, one can establish the following property, for all $\varvec{\ell } \in \mathsf {tem}(\mathcal {A})$:

$$\begin{aligned} \varvec{\ell } \in \mathsf {ans}({\textit{\textbf{q}}},\mathcal {A}) \qquad \text { iff } \qquad \mathcal{C}_{\mathcal {O},\mathcal {A}} \models \psi (\varvec{\ell }). \end{aligned}$$

(15)

The second important component of the proof is the fact that every OMPIQ $(\mathcal {O}, \varkappa )$ is $\mathcal {L}$-rewritable and has phantoms $\varPhi _{(\mathcal {O}, \varkappa )}^k$ in $\mathcal {L}$ if every OMAQ $(\mathcal {O}, A)$ with A from $\varkappa$ is such. This fact is shown by induction on the construction of $\varkappa$ using (15). As an example, we show how to construct a rewriting $\varphi _{\varkappa }(t)$ for $\varkappa = \Diamond _{\!\scriptscriptstyle F}A$ from a rewriting $\varphi _{A}(t)$ for A and phantoms $\varPhi _{(\mathcal {O}, A)}^k$. By the semantics of $\Diamond _{\!\scriptscriptstyle F}$, we could take

$$ \varphi _{\varkappa }(t) = \exists t'\, \big ((t'> t) \wedge \varphi _A(t')\big ) \vee \bigvee _{k > 0}\varPhi _{(\mathcal {O}, A)}^k. $$

Indeed, provided that ‘infinite’ formulas are allowed in rewritings, it is not hard to check, using (15), that $\varphi _{\varkappa }(t)$ is a rewriting of $(\mathcal {O}, \varkappa )$. To avoid the ‘infinite’ disjunction, we need an additional periodicity property of the canonical models: for every ontology $\mathcal {O}$, there are positive integers $s_{\mathcal {O}}$ and $p_{\mathcal {O}}$ such that, for any data instance $\mathcal {A}$,

$$\begin{aligned} {\textit{\textbf{t}}}_{\mathcal {O}}(n) = {\textit{\textbf{t}}}_{\mathcal {O},\mathcal {A}}(n + p_{\mathcal {O}}), \text { for }n \ge \max \mathcal {A}+ s_{\mathcal {O}}. \end{aligned}$$

In view of this periodicity, we can finitise the ‘infinite’ rewriting of $(\mathcal {O}, \varkappa )$ by taking

$$ \varphi _{\varkappa }(t)= \exists t'\, \big ((t' > t) \wedge \varphi _A(t')\big ) \vee \bigvee _{0< k < s_{\mathcal {O}} + p_{\mathcal {O}}}\varPhi _{(\mathcal {O}, A)}^k. $$

The reader is invited to define phantoms $\varPhi _{(\mathcal {O}, \varkappa )}^k$ for $(\mathcal {O}, \varkappa )$ and $k > 0$ using the method above.

The third and last important component of this proof is that every monotone formula $\psi (\textit{\textbf{t}})$ is equivalent to a disjunction $\varphi (\textit{\textbf{t}}) = \bigvee _{l=1}^k \varphi _l(\textit{\textbf{t}})$ of formulas of the following form, for $l = 1,\dots , k$:

$$\begin{aligned} \varphi _l(\textit{\textbf{t}}) ~=~ \exists x_1,\dots ,x_n\, \Big [ \bigwedge _{i=1}^m (t_i = x_{j_i}) \wedge (x_1< \dots< x_n) \wedge \bigwedge _{i=1}^n \alpha _i(x_i) \wedge {}\\ \bigwedge _{i=1}^{n-1} \forall y\, \big ( (x_i< y < x_{i+1}) \rightarrow \beta _i(y) \big ) \Big ], \end{aligned}$$

(16)

where the first conjunction contains $(t_i = x_1)$ and $(t_j = x_n)$ with free variables $t_i,t_j \in \textit{\textbf{t}}$, and the $\alpha _i$ and $\beta _i$ are FO$(<)$-formulas with one free variable equivalent to some OMPIQs $(\mathcal {O}, \varkappa _i)$ and $(\mathcal {O}, \lambda _i)$ (respectively). This equivalence result is shown using Rabinovich’s proof of Kamp’s Theorem  [74]. Let us assume that $\psi (\textit{\textbf{t}})$ is a disjunction of formulas (16), and substitute in it each $\alpha _i(x_i)$ by $\varphi _{\varkappa _i}(x_i)$, where $\varphi _{\varkappa _i}(x_i)$ is a rewriting of $(\mathcal {O}, \varkappa _i)$, and similarly for $\beta _i(y)$. It is then straightforward to verify, relying on (15), that the result of this substitution is a rewriting of $(\mathcal {O}, \psi (\textit{\textbf{t}}))$.   $\square$

Corollary 21

All monotone OMQs are FO$(<,\equiv _{\mathbb {N}})$-rewritable, and all monotone OMQs are FO$(<)$-rewritable.

4 OBDA with Temporalised DL-Lite

The OMQs considered so far are one-dimensional. For example, the ontology from Exercise 8 captures background knowledge about temporal events that can happen with one article submitted to a journal. If we want to use OBDA in order to query data about other articles, authors, co-authors, editors, etc., we need a language that is capable of representing knowledge about a second dimension, a domain populated by those articles, authors, co-authors, editors, and relationships between them.

Description logics (DLs)  [12, 13] form a prominent family of knowledge representation formalisms designed specifically for atemporal domains of that sort. However, far from all of the existing DLs are suitable for OBDA because OMQs with DL ontologies are not necessarily rewritable to standard target query languages such as FO (which is essentially SQL) or datalog; for more details we refer the reader to the course  [61]. The DL-Lite family of DLs was developed for OBDA with relational databases and with the aim of guaranteeing FO-rewritability of all OMQs with conjunctive queries  [6, 29, 73, 84]. DL-Lite logics also underpin the OWL 2 QL profile of the Web Ontology Language OWL 2 standardised by the W3C.

We illustrate DL-Lite by a simple example (borrowed from  [21]); for a detailed introduction to OBDA with OWL 2 QL, we refer the reader to  [59, 61].

Example 22

Consider the following ontology $\mathcal {O}$ given in the DL syntax and, for the reader’s convenience, translated into first-order logic:

$$\begin{aligned}&\textit{ProjectManager} \sqsubseteq \exists \textit{isAssistedBy}. \textit{PA}\\&\qquad \qquad \qquad {\small \forall x \, \big (\textit{ProjectManager}(x) \rightarrow \exists y\, (\textit{isAssistedBy}(x,y) \wedge \textit{PA}(y))\big )}\\&\exists \textit{managesProject} \sqsubseteq \textit{ProjectManager}\\&\qquad \qquad \qquad {\small \forall x\, \big (\exists y\, \textit{managesProject}(x,y) \rightarrow \textit{ProjectManager}(x)\big )}\\&\textit{ProjectManager} \sqsubseteq \textit{Staff}\\&\qquad \qquad \qquad {\small \forall x \, \big (\textit{ProjectManager}(x) \rightarrow \textit{Staff}(x)\big )}\\&\textit{PA} \sqsubseteq \textit{Secretary}\\&\qquad \qquad \qquad {\small \forall x \, \big (\textit{PA}(x) \rightarrow \textit{Secretary}(x)\big )} \end{aligned}$$

Here, ProjectManager, PA, Staff, and Secretary are concept names (corresponding to the unary predicates in the FO-translations), while isAssistedBy as well as managesProject are role names (corresponding to the binary predicates). The conjunctive query

$$\begin{aligned} \psi (x) \ = \ \exists y \, \bigl (\textit{Staff}(x) \wedge \textit{isAssistedBy}(x,y) \wedge \textit{Secretary}(y)\bigr ) \end{aligned}$$

asks for the members of staff that are assisted by secretaries. We invite the reader to verify that the following FO-query

is an FO-rewriting of the OMQ ${\textit{\textbf{Q}}}(x) = (\mathcal {O},\psi (x))$ in the sense that, for any data instance $\mathcal {A}$ (which contains ground atoms such as $\textit{ProjectManager}({ bob})$, $\textit{PA}({ joe})$ and $\textit{isAssistedBy}({ bob},{ sam})$) and any individual name a from $\mathcal {A}$, we have $\mathcal {O},\mathcal {A}\models \psi (a)$ iff $\textit{\textbf{Q}}(a)$ is true when evaluated directly over $\mathcal {A}$.

Being able to speak about domain concepts and roles, DL cannot say anything about their evolution in time. Following  [8], we next introduce two-dimensional combinations of the LTL ontology languages from the previous section and various species of DL-Lite. The 2D language now contains individual names $a_0,a_1,\dots$, concept names $A_0,A_1,\dots$, and role names $P_0,P_1,\dots$. Roles S, temporalised roles R, basic concepts B, and temporalised concepts C are defined by the following grammars:

A concept or role inclusion takes the form

$$\begin{aligned} \vartheta _1 \sqcap \dots \sqcap \vartheta _k ~\sqsubseteq ~ \vartheta _{k+1} \sqcup \dots \sqcup \vartheta _{k+m}, \end{aligned}$$

(17)

where the $\vartheta _i$ are all temporalised concepts of the form C or, respectively, temporalised roles of the form R. When it does not matter whether we talk about concepts or roles, we refer to the $\vartheta _i$ as terms. A TBox $\mathcal {T}$ and an RBox $\mathcal {R}$ are finite sets of concept inclusions (CIs, for short) and, respectively, role inclusions (RIs, for short); their union $\mathcal {O}= \mathcal {T}\cup \mathcal {R}$ is called an ontology.

As before, we classify ontologies by the form of their inclusions and the temporal operators that occur in them. Let ${\textit{\textbf{c}}},{\textit{\textbf{r}}}\in \{\textit{bool}, \textit{horn}, \textit{krom},\textit{core}\}$ and . We denote by the temporal description logic whose TBoxes and RBoxes contain concept and role inclusions (17) satisfying ${\textit{\textbf{c}}}$ and ${\textit{\textbf{r}}}$, respectively, and the only temporal operators that occur in them are indicated in ${\textit{\textbf{o}}}$. Whenever ${\textit{\textbf{c}}}= {\textit{\textbf{r}}}$, we use a single subscript, that is, $\textit{DL-Lite}^{\textit{\textbf{o}}}_{{\textit{\textbf{c}}}} = \textit{DL-Lite}^{\textit{\textbf{o}}}_{{\textit{\textbf{c}}}/{\textit{\textbf{c}}}}$.

Note that, unlike the standard atemporal DL-Lite logics  [6, 29], which can have various types of CIs but allow only core RIs (of the form $S_1 \sqsubseteq S_2$ and $S_1 \sqcap S_2 \sqsubseteq \bot$), here we treat CIs and RIs in a uniform way and impose restrictions on the clausal structure of CIs and RIs separately.

An ABox (data instance, in DL parlance), $\mathcal {A}$, is a finite set of atoms of the form $A_i(a,\ell )$ and $P_i(a,b,\ell )$, where a and b are individual names and $\ell \in \mathbb {Z}$. We denote by the set of individual names in $\mathcal {A}$; as before, we also set . A knowledge base (KB) is a pair $(\mathcal {O},\mathcal {A})$, where $\mathcal {O}$ is a ontology and $\mathcal {A}$ an ABox. The size $|\mathcal {O}|$ of an ontology $\mathcal {O}$ is the number of occurrences of symbols in $\mathcal {O}$; the size of a TBox, RBox, ABox, and knowledge base is defined analogously.

A (temporal) interpretation is a pair $\mathcal {I}= (\Delta ^\mathcal {I},\cdot ^{\mathcal {I}(n)})$, where $\Delta ^\mathcal {I}\ne \emptyset$ and, for each $n \in \mathbb {Z}$,

$$\begin{aligned} \mathcal {I}(n)=(\Delta ^\mathcal {I}, a_0^\mathcal {I},\dots ,A_0^{\smash {\mathcal {I}(n)}}, \dots ,P_0^{\smash {\mathcal {I}(n)}},\dots ) \end{aligned}$$

(18)

is a standard (atemporal) DL interpretation with $a_i^{\mathcal {I}}\in \Delta ^\mathcal {I}$, $A_i^{\smash {\mathcal {I}(n)}}\subseteq \Delta ^\mathcal {I}$ and $P_i^{\smash {\mathcal {I}(n)}}\subseteq \Delta ^\mathcal {I}\times \Delta ^\mathcal {I}$. Thus, we assume that the domain $\Delta ^\mathcal {I}$ and the interpretations $a_i^\mathcal {I}\in \Delta ^\mathcal {I}$ of the individual names are the same for all $n\in \mathbb {Z}$. (However, we do not adopt the unique name assumption.) The description logic and temporal constructs are interpreted in $\mathcal {I}(n)$ as follows:

As usual, $\bot$ is interpreted by $\emptyset$, and $\top$ by $\Delta ^{\smash {\mathcal {I}}}$ for concepts and by $\Delta ^{\smash {\mathcal {I}}}\times \Delta ^{\smash {\mathcal {I}}}$ for roles. CIs and RIs are interpreted in $\mathcal {I}$ globally, i.e., (17) holds in $\mathcal {I}$ if

Given an inclusion $\alpha$, we write $\mathcal {I}\models \alpha$ if $\alpha$ holds in $\mathcal {I}$. We call $\mathcal {I}$ a model of $(\mathcal {O},\mathcal {A})$ and write $\mathcal {I}\models (\mathcal {O},\mathcal {A})$ if

We say that $\mathcal {O}$ is consistent if there is an interpretation $\mathcal {I}$, a model of $\mathcal {O}$, such that $\mathcal {I}\models \alpha$, for all $\alpha \in \mathcal {O}$; we also say and that $\mathcal {A}$ is consistent with $\mathcal {O}$ if there is a model of $(\mathcal {O},\mathcal {A})$. For an inclusion $\alpha$, we write $\mathcal {O}\models \alpha$ if $\mathcal {I}\models \alpha$ for every model $\mathcal {I}$ of $\mathcal {O}$. A concept C is consistent with $\mathcal {O}$ if there is a model $\mathcal {I}$ of $\mathcal {O}$ and $n\in \mathbb {Z}$ such that $C^{\mathcal {I}(n)}\ne \emptyset$; consistency of roles with $\mathcal {O}$ is defined analogously.

We now define a language for querying temporal knowledge bases, which was inspired by the SPARQL 1.1 entailment regimes  [44]; see also  [46, 69]. The main ingredients of the language are positive temporal concepts $\varkappa$ and positive temporal roles $\varrho$ given by the following grammars:

where and $\textit{\textbf{op}}_2\in \{\mathcal {U}, \mathbin {\mathcal {S}}\}$. Let $\mathcal {I}= (\Delta ^\mathcal {I},\cdot ^{\mathcal {I}(n)})$ be an interpretation. The extensions $\varkappa ^{\mathcal {I}(n)}$ of $\varkappa$ in $\mathcal {I}$, for $n \in \mathbb {Z}$, are computed using the definition above and the following items:

$$\begin{aligned}&(\exists S.\varkappa )^{\mathcal {I}(n)} = \bigl \{\, u \in \Delta ^\mathcal {I}\mid (u,v) \in S^{\mathcal {I}(n)}, \text { for some } v\in \varkappa ^{\mathcal {I}(n)} \,\bigr \},\\&(\varkappa _1 \sqcap \varkappa _2)^{\mathcal {I}(n)} = \varkappa _1^{\mathcal {I}(n)} \cap \varkappa _2^{\mathcal {I}(n)}, \qquad (\varkappa _1 \sqcup \varkappa _2)^{\mathcal {I}(n)} = \varkappa _1^{\mathcal {I}(n)} \cup \varkappa _2^{\mathcal {I}(n)},\\&(\Diamond _{\!\scriptscriptstyle F}\varkappa )^{\mathcal {I}(n)} = \bigcup _{k>n} \varkappa ^{\mathcal {I}(k)}, (\Diamond _{\!\scriptscriptstyle P}\varkappa )^{\mathcal {I}(n)} = \bigcup _{k<n} \varkappa ^{\mathcal {I}(k)},\\&(\varkappa _1 \mathcal {U}\varkappa _2)^{\mathcal {I}(n)} = \bigcup _{k>n}\,\bigl (\varkappa _2^{\mathcal {I}(k)} \cap \bigcap _{n< m< k} \varkappa _1^{\mathcal {I}(m)}\bigr ), \\&(\varkappa _1 \mathbin {\mathcal {S}}\varkappa _2)^{\mathcal {I}(n)} = \bigcup _{k<n}\,\bigl (\varkappa _2^{\mathcal {I}(k)} \cap \bigcap _{k< m < n} \varkappa _1^{\mathcal {I}(m)}\bigr ). \end{aligned}$$

The definition of $\varrho ^{\mathcal {I}(n)}$ is analogous. Note that positive temporal concepts $\varkappa$ and roles $\varrho$ include all temporalised concepts C and roles R, respectively ($\exists S$ is a shortcut for $\exists S.\top$).

A $\textit{DL-Lite}^{{\textit{\textbf{o}}}}_{{\textit{\textbf{c}}}/{\textit{\textbf{r}}}}$ ontology-mediated instance query (OMIQ) is a pair of the form ${\textit{\textbf{q}}}= (\mathcal {O}, \varkappa )$ or ${\textit{\textbf{q}}}= (\mathcal {O}, \varrho )$, where $\mathcal {O}$ is a $\textit{DL-Lite}^{{\textit{\textbf{o}}}}_{{\textit{\textbf{c}}}/{\textit{\textbf{r}}}}$ ontology, $\varkappa$ is a positive temporal concept and $\varrho$ a positive temporal role (which can use all temporal operators, not necessarily only those in ${\textit{\textbf{o}}}$). If $\varkappa$ is a basic concept (i.e., A or $\exists S$) and $\varrho$ a role, then we refer to ${\textit{\textbf{q}}}$ as an ontology-mediated atomic query (OMAQ, as before). A certain answer to an OMIQ $(\mathcal {O},\varkappa )$ over an ABox $\mathcal {A}$ is a pair $(a,\ell )\in \mathsf {ind}(\mathcal {A})\times \mathsf {tem}(\mathcal {A})$ such that $a^{\mathcal {I}} \in \varkappa ^{\smash {\mathcal {I}(\ell )}}$ for every model $\mathcal {I}$ of $(\mathcal {O}, \mathcal {A})$. A certain answer to $(\mathcal {O},\varrho )$ over $\mathcal {A}$ is a triple $(a,b,\ell )\in \mathsf {ind}(\mathcal {A})\times \mathsf {ind}(\mathcal {A})\times \mathsf {tem}(\mathcal {A})$ such that $(a^{\mathcal {I}},b^{\mathcal {I}}) \in \varrho ^{\smash {\mathcal {I}(\ell )}}$ for every model $\mathcal {I}$ of $(\mathcal {O}, \mathcal {A})$. The set of all certain answers to ${\textit{\textbf{q}}}$ over $\mathcal {A}$ is denoted, as before, by $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$.

Let $\mathcal {A}$ be any given ABox with $\mathsf {ind}(\mathcal {A}) = \{a_1,\dots ,a_m\}$. We always assume, without much loss of generality, that $|\mathsf {tem}(\mathcal {A})| \ge |\mathsf {ind}(\mathcal {A})|$ (if this is not the case, we can simply add the required number of dummies with the missing time instances to $|\mathsf {tem}(\mathcal {A})|$). We represent $\mathcal {A}$ as a structure $\mathfrak S_\mathcal {A}$ with domain $\mathsf {tem}(\mathcal {A})$ ordered by < such that

$$\begin{aligned} \mathfrak S_\mathcal {A}\models A(k,\ell ) \quad \text {iff} \quad A(a_k,\ell )\in \mathcal {A}, \qquad \mathfrak S_\mathcal {A}\models P(k,k',\ell ) \quad \text {iff} \quad P(a_k,a_{k'},\ell )\in \mathcal {A}, \end{aligned}$$

for any concept and role names A, P and any $k,k',\ell \in \mathsf {tem}(\mathcal {A})$. To simplify notation, we often identify an individual name $a_k \in \mathsf {ind}(\mathcal {A})$ with its number representation $k \in \mathsf {tem}(\mathcal {A})$. The structure $\mathfrak S_\mathcal {A}$ represents a temporal database over which we can evaluate first-order formulas (queries) with predicates of the form A(x, t), P(x, y, t) and $t_1 < t_2$ as well as other standard numeric predicates and relational primitive recursion.

Definition 23

(FO-rewritability). Let $\mathcal {L}$ be one of the three languages FO$(<)$, FO$(<,\equiv _{\mathbb {N}})$ or FO(RPR). Let ${\textit{\textbf{q}}}=(\mathcal {O}, \varkappa )$ be an OMIQ and $\textit{\textbf{Q}}(x,t)$ a constant-free $\mathcal {L}$-formula with free variables x and t. We call $\textit{\textbf{Q}}(x,t)$ an $\mathcal {L}$-rewriting of ${\textit{\textbf{q}}}$ if, for any ABox $\mathcal {A}$, any $a \in \mathsf {ind}(\mathcal {A})$ and any $\ell \in \mathsf {tem}(\mathcal {A})$, we have $(a,\ell ) \in \mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$ iff $\mathfrak S_\mathcal {A}\models \textit{\textbf{Q}}(a,\ell )$. Similarly, a constant-free $\mathcal {L}$-formula $\textit{\textbf{Q}}(x,y,t)$ is an $\mathcal {L}$-rewriting of an OMIQ ${\textit{\textbf{q}}}= (\mathcal {O},\varrho )$ if, for any ABox $\mathcal {A}$, any $a,b \in \mathsf {ind}(\mathcal {A})$ and any $\ell \in \mathsf {tem}(\mathcal {A})$, we have $(a,b,\ell ) \in \mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$ iff $\mathfrak S_\mathcal {A}\models \textit{\textbf{Q}}(a,b,\ell )$.

Having all the definitions given, it is time to recall that two-dimensional combinations of knowledge representation formalisms can be computationally very complex if any non-trivial interaction between the dimensions is available; see, e.g.,  [41,42,43, 54, 65]. Our temporalised DL-Lite logics are not an exception as the following theorem demonstrates:

Theorem 24

(i) Consistency checking for KBs is undecidable.

(ii) There are OMAQs ${\textit{\textbf{q}}}_1 = (\mathcal {O}, A)$ and ${\textit{\textbf{q}}}_2 = (\mathcal {O}, S)$ such that the problems whether, for a given ABox $\mathcal {A}$, the pair (a, 0) is a certain answer to ${\textit{\textbf{q}}}_1$ over $\mathcal {A}$ and (a, b, 0) is a certain answer to ${\textit{\textbf{q}}}_2$ over $\mathcal {A}$ are undecidable.

Proof

(Sketch). (i) The proof is by reduction of the undecidable $\mathbb {N} \times \mathbb {N}$-tiling problem  [19]. Given a set $\mathfrak T = \{1,\dots ,k\}$ of tile types, we define a KB $(\mathcal {O}_{\mathfrak T},\{I(a,0)\})$ with the following ontology $\mathcal {O}_{\mathfrak T}$, where the $R_{i}$ are role names associated with the tile types $i \in \mathfrak T$ and $\textit{top}(i)$, $\textit{bot}(i)$, $\textit{right}(i)$, $\textit{left}(i)$ are the colours on the four edges of any tile type i:

It is readily checked that $\{I(a,0)\}$ is consistent with $\mathcal {O}_{\mathfrak T}$ iff $\mathfrak T$ can tile the $\mathbb {N} \times \mathbb {N}$ grid.

(ii) Using the representation of the universal Turing machine by means of tiles (see, e.g.,  [23]), we obtain a set $\mathfrak U$ of tile types for which the following problem is undecidable: given a finite sequence of tile types $i_0,\dots ,i_n$, decide whether $\mathfrak U$ can tile the $\mathbb {N} \times \mathbb {N}$ grid so that tiles of types $i_0,\dots ,i_n$ are placed on $(0,0),\dots ,(n,0)$, respectively. Given such $i_0,\dots ,i_n$, we take the ABox $\mathcal {A}= \{\,I(a,0), R_{i_0}(a,b,0),\dots ,R_{i_n}(a,b,n)\,\}$. Then $\mathfrak U$ can tile $\mathbb {N} \times \mathbb {N}$ with $i_0,\dots ,i_n$ on the first row iff $\mathcal {A}$ is consistent with $\mathcal {O}_{\mathfrak U}$ iff A(a, 0) is not a certain answer to OMAQ $(\mathcal {O}_{\mathfrak U},A)$ over $\mathcal {A}$, where A is a fresh concept name; similar considerations apply to the case of a fresh role S.   $\square$

We can obtain better-behaved logics by restricting the expressive power of role inclusions. The proof of the following result can be found in [60].

Theorem 25

Consistency checking for , and is ExpSpace-complete for combined complexity; for and , it is $\textsc {PSpace}$-complete.

Let us now consider FO-rewritability of OMQs with ontologies in temporalised DL-Lite. To avoid many a technical detail and concentrate on the main ideas, we only discuss here OMQs with atomic queries (that is, OMAQs) and ontologies without occurrences of $\bot$ (which, therefore, are always consistent). Let $\mathcal {L}$ be one of the target languages FO$(<)$, FO$(<,\equiv _{\mathbb {N}})$ or FO(RPR). We show that $\mathcal {L}$-rewritability of a $\bot$-free OMAQ with an ontology is reducible to $\mathcal {L}$-rewritability of a role-free OMAQ. Ontologies without roles are clearly a notational variant of LTL ontologies; hence, in this case we can write ‘ ontologies’. We explain the reduction by instructive examples. The first two of them illustrate the interaction between the DL and temporal dimensions in that we need to take into account when constructing the LTL OMAQs to which the rewritability of $\bot$-free OMAQs is reduced.

Example 26

Suppose $\mathcal {T}= \{ \, B \sqsubseteq \exists P, \ \exists Q \sqsubseteq A\,\}$ and . An obvious idea of constructing a rewriting for the OMAQ ${\textit{\textbf{q}}}= (\mathcal {T}\cup \mathcal {R},\, A)$ would be to find first a rewriting of the $\textit{LTL}$ OMAQ $(\mathcal {T}^\dagger ,A^\dagger )$ obtained from $(\mathcal {T}, A)$ by replacing the basic concepts $\exists P$ and $\exists Q$ with surrogate concept names $(\exists P)^\dagger = E_P$ and $(\exists Q)^\dagger = E_Q$, respectively. This would give us the FO-query $A(x,t) \vee E_Q(x,t)$. By restoring the intended meaning of $E_Q$, we would then obtain $A(x,t) \vee \exists y \, Q(x,y,t)$. The second step would be to rewrite, using the RBox $\mathcal {R}$, the atom Q(x, y, t) into $Q(x,y,t) \vee P(x,y,t-1)$. However, the resulting formula

$$\begin{aligned} A(x,t) \vee \exists y \, \bigl (Q(x,y,t) \vee P(x,y, t-1) \bigr ) \end{aligned}$$

is not a rewriting of ${\textit{\textbf{q}}}$ as it does not return the certain answer (a, 1) over the ABox $\mathcal {A}= \{B(a,0),C(a,1)\}$ because so far we have not taken into account the CI , which is a consequence of $\mathcal {R}$. If we now add the ‘connecting axiom’ to $\mathcal {T}^\dagger$, then in the first step we obtain $A(x,t) \vee E_Q(x,t) \vee E_P(x,t-1) \vee B(x,t-1)$, which gives us the correct FO$(<)$-rewriting of ${\textit{\textbf{q}}}$:

$$ A(x,t) \vee \exists y \, \big ( Q(x,y,t) \vee P(x,y, t-1)\big ) \vee {} \exists y \, P(x,y, t-1) \vee B(x, t-1). $$

Example 27

Let ${\textit{\textbf{q}}}= (\mathcal {T}\cup \mathcal {R},\, A)$ with and

The two-step construction outlined in Example 26 would give us first the formula

$$\begin{aligned} \varPhi (x,t) ~=~ A(x,t) \vee \exists t' \, \big ( (t < t') \wedge \exists y \, Q(x,y,t') \big ) \end{aligned}$$

as a rewriting of $(\mathcal {T},A)$. It is readily checked that the following formula $\varPsi (x,y,t')$ is a rewriting of $(\mathcal {R},Q)$:

However, the result of replacing $Q(x,y,t')$ in $\varPhi (x,t)$ with $\varPsi (x,y,t')$ is not an FO$(<)$-rewriting of $(\mathcal {O}, A)$: when evaluated over $\mathcal {A}= \{\, T(a,b,0),\ P(a,b,1)\,\}$, it does not return the certain answers (a, 0) and (a, 1); see the picture below:

(Note that these answers would be found had we evaluated the obtained ‘rewriting’ over $\mathbb {Z}$ rather than $\{0,1\}$.) This time, we miss the concept inclusion , which follows from $\mathcal {R}$ and $\mathcal {T}$. To fix the problem, we can take a fresh role name $G_\rho$, for , and add the ‘connecting axiom’ to $\mathcal {T}$. Then, in the first step, we rewrite the extended TBox and A to the formula

where we replace $Q(x,y,t')$ by $\varPsi (x,y,t')$ and restore the meaning of $G_\rho (x,y,t')$ by rewriting to $P(x,y,t') \wedge \bigl (T_1(x,y,t') \vee \exists t''\,\bigl ((t'' < t) \wedge T(x,y,t'')\bigr )\bigr )$ and substituting it for $G_\rho (x,y,t')$ in $\varPhi '(x,t)$.

We now formally define the connecting axioms for $\mathcal {O}$, assuming that $\mathcal {R}$ contains all role names in $\mathcal {T}$. Let $\rho$ be a set of (temporalised) roles from $\mathcal {R}$ consistent with $\mathcal {R}$. Let $\textit{\textbf{r}}_\rho$ be the $\mathcal {R}$-canonical rod for $\{ S(d,e,0) \mid S\in \rho \}$. Clearly, there are positive integers $s^{\,\rho } \le |\mathcal {R}|$ and $p^{\,\rho } \le 2^{2|\mathcal {R}|}$ with

$$\begin{aligned}&\textit{\textbf{r}}_\rho (n) = \textit{\textbf{r}}_\rho (n - p^{\,\rho }),&\text { for } n \le - s^{\,\rho },\\&\textit{\textbf{r}}_\rho (n) = \textit{\textbf{r}}_\rho (n + p^{\,\rho }),&\text { for } n \ge s^{\,\rho }. \end{aligned}$$

Then we take a fresh role name $G_{\rho }$ and fresh concept names $D^n_{\rho }$, for $- s^{\,\rho } - p^{\,\rho }< n < s^{\,\rho }+ p^{\,\rho }$, and construct the CIs

and symmetrical ones for $-s^{\,\rho } - p^{\,\rho } \le n \le 0$. Let (con) be the set of such CIs for all possible $\rho$. Set $\mathcal {T}_\mathcal {R}= \mathcal {T}\cup \mathbf (con)$.

Example 28

In Example 26, for , we have $s^{\,\rho } = 2$, $p^{\,\rho } = 1$, and so $\mathcal {T}_\mathcal {R}$ contains the CIs

which imply . In the context of Example 27, for , we have $s^{\,\rho } = 1$, $p^{\,\rho } = 1$, and so $\mathcal {T}_\mathcal {R}$ contains the following CIs:

We denote by $\mathcal {T}^\dagger _{\smash {\mathcal {R}}}$ the TBox obtained from $\mathcal {T}_\mathcal {R}$ by replacing every basic concept B with its surrogate $B^\dagger$.

Theorem 29

Let $\mathcal {L}$ be one of FO$(<)$, FO$(<,\equiv _{\mathbb {N}})$, FO$(RPR )$. A OMAQ $(\mathcal {O}, A)$ with a $\bot$-free $\mathcal {O}= \mathcal {T}\cup \mathcal {R}$ is $\mathcal {L}$-rewritable whenever

• the OMAQ $(\mathcal {T}_\mathcal {R}^{\smash {\dagger }}, A)$ is $\mathcal {L}$-rewritable and

• the OMAQ $(\mathcal {R}, R)$ is $\mathcal {L}$-rewritable, for every temporalised role in $\mathcal {R}$.

As a consequence of Theorems 13 and 29, we obtain:

Theorem 30

Every OMAQ is FO(RPR)-rewritable.

Moreover, we also have the following:

Corollary 31

(i) All OMAQs, and so all OMAQs are FO$(<,\equiv _{\mathbb {N}})$-rewritable.

(ii) All OMAQs are FO(RPR)-rewritable.

These results can be extended to OMQs with more complex queries:

Theorem 32

(i) All OMIQs are FO$(<)$-rewritable.

(ii) All OMIQs are FO$(<,\equiv _{\mathbb {N}})$-rewritable.

(iii) All OMIQs are FO(RPR)-rewritable.

It is to be noted that Theorem 32 holds for core and Horn DL-Lite logics only because even very simple disjunctive axioms lead to coNP-complete OMIQ answering problem. For example, as follows from  [76], answering the atemporal $\textit{DL-Lite}_\textit{krom}$ OMIQ

$$ \big ( \{\top \sqsubseteq A \sqcup B\}, \ \exists R. (\exists P_1.A \sqcap \exists P_2.A \sqcap \exists N_1.B \sqcap \exists N_2.B)\big ) $$

is $\textsc {coNP}$-complete for data complexity.

5 Ontology-Mediated Queries with MTL Ontologies

So far, we have discussed temporal ontologies with LTL-operators, which allowed us to naturally describe the behaviour of synchronous systems. Note, however, that LTL-representations of metric statements such as ‘high temperature will be reached in at most 100 s’ require long and unreadable disjunctions of the form

Moreover, such formulas become meaningless in the case of asynchronous systems where time is dense and there is no next or previous moment.

A more suitable temporal knowledge representation formalism in this case is metric temporal logic MTL, which was introduced for modelling and reasoning about real-time systems [3, 62]. Essentially, MTL-operators are obtained by indexing the LTL-operators with arbitrary intervals $\varrho$, which allow concise representation of metric information and which can be used over dense time. We denote the metric counterparts of the future LTL-operators $\Diamond _{\!\scriptscriptstyle F}$, , and $\mathcal {U}$ by , $\boxplus _\varrho$, and $\mathcal {U}_\varrho$, respectively; their past analogues are , $\boxminus _\varrho$, and $\mathbin {\mathcal {S}}_\varrho$. Recall from Sect. 2 that, in the case of dense time, we assume that timestamps are dyadic rational numbers (whose set is denoted by $\mathbb {Q}_2$). Each interval $\varrho$, indexing an MTL-operator and called its range, has non-negative end-points from $\mathbb {Q}_2^{\ge 0}$ or $\infty$.

Example 33

The formula is regarded to be true at a time instant $t \in \mathbb {Q}_2$ if $\textit{HighTemp}$ is true at some moment in the interval $(t,t+100]$; dually, the formula $\boxplus _{(0,100]} \textit{HighTemp}$ holds at t if $\textit{HighTemp}$ is true at every point of that interval. Note that the LTL-formula $\Diamond _{\!\scriptscriptstyle F}\textit{HighTemp}$ has the same meaning as the MTL-formula and as $\boxplus _{(0,\infty )} \textit{HighTemp}$.

Similarly to the case of LTL, we treat ontology axioms with $\textit{MTL}$-operators as (variable-free) abbreviations for monadic first-order formulas. However, since now time is dense, instead of MFO$(<)$-formulas, we use $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$-formulas, where $\delta _{<a}$ and $\delta _{= a}$, for $a \in \mathbb {Q}^+_2$, are additional built-in binary predicates allowing us to speak about the distance between moments of time. Recall that $\delta _{<a}(x,y)$ stands for $0 \le x-y < a$, and $\delta _{=a}(x,y)$ for $x-y = a$. Using these predicates, for every range $\varrho$, we can define a predicate $\delta _\varrho (x,y)$ saying that $x - y \in \varrho$; for example, we can set

$$ \delta _{[1,2)}(x,y) = \delta _{\ge 1}(x,y) \wedge \delta _{<2}(x,y) . $$

We can define the standard translation $^\ddag$ from MTL into $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$, similar to the translation $^\dag$ of LTL into MFO$(<)$, by taking, for example

As mentioned in Sect. 2, there are two semantics for $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$ and MTL. In the continuous semantics, the temporal domain in the definition (2) of $\mathsf {ans}({\textit{\textbf{q}}},\mathcal {A})$ is the whole of $\mathbb {Q}_2$; in the pointwise semantics, it coincides with the active domain $\mathsf {tem}(\mathcal {A})$. Under the former, $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$-formulas with one free variable have the same expressive power as MTL-formulas interpreted over the reals $\mathbb {R}$  [55]. On the other hand, the satisfiability and model checking problems turn out to be undecidable in this case  [50]. However, as shown in [71], both problems become decidable, albeit with non-primitive recursive complexity, if the pointwise semantics is adopted.

Let us now turn to OBDA with MTL-ontologies. Compared to the LTL OMQs, research of the MTL case has just begun, and very few results are known at the moment. In particular, FO-rewritability of MTL OMQs under the continuous semantics is practically terra incognita; we refer the reader to  [25, 26, 82, 83] and the survey  [9]. In the remainder of this section, we discuss what is known about FO-rewritability of MTL OMQs under the pointwise semantics following  [75]. We begin with an example.

Example 34

Consider the $\textit{MTL}$-ontology and the data instances $\mathcal {A}_1 = \{ B(0), B (1/2), C(3/2) \}$ and $\mathcal {A}_2 = \{ B(0),C(3/2) \}$. Then $\mathsf {tem}(\mathcal {A}_1)=\{0, 1/2, 3/2 \}$ and $\mathsf {tem}(\mathcal {A}_2)= \{0, 3/2 \}$. The minimal models $\mathcal {I}_1$ of $({\mathcal {O}},\mathcal {A}_1)$ and $\mathcal {I}_2$ of $({\mathcal {O}},\mathcal {A}_2)$ are shown in the picture below:

Hence, 3/2 is a certain answer to the OMAQ $({\mathcal {O}},A)$ over $\mathcal {A}_1$, but there is no certain answer to $({\mathcal {O}},A)$ over $\mathcal {A}_2$.

In what follows, we consider FO-rewritability of MTL OMAQs only. The following observation is simple and left to the reader.

Theorem 35

Answering $\textit{MTL}$ OMAQs is in coNP for data complexity.

The next theorem establishes some lower complexity bounds for answering MTL OMQs, which should be compared with the data complexity of LTL OMQs. In this theorem, $\textit{MTL}^-$ means MTL with past operators only, with $\textit{MTL}_{horn}^-$ and $\textit{MTL}_{core}^-$ being its Horn and core fragments, respectively.

Theorem 36

(i) Answering $\textit{MTL}$ OMAQs is coNP-hard for data complexity.

(ii) Answering OMAQs with an $\textit{MTL}_{core}^-$ ontology is P-hard for data complexity.

(iii) Answering OMAQs with an $\textit{MTL}_{core}^-$ ontology containing operators only is NL-hard for data complexity.

Proof

(Sketch). We show (i) by reduction of the complement of the NP-complete circuit satisfiability problem  [5]. Instead of presenting the details of the construction, we only consider the Boolean circuit below, which contains two input gates, one AND gate, one OR gate, and one NOT gate.

First, we enumerate the gates of the circuit with consecutive numbers starting from 0 so that if there is an edge from n to m, then $n < m$ (observe that such an enumeration always exists). Then we define a data instance $\mathcal {A}$ stating that A holds in 25 timestamps. These timestamps form 5 sections, each containing 5 timestamps (as there are 5 gates in the circuit) as depicted below:

The data instance $\mathcal {A}$ also contains facts about X (for the input gates), D (for the OR gate), C (for the AND gate), N (for the NOT gate), $I_0$ (for the input of the NOT gate), and $I_1$ and $I_2$ (for the first and the second inputs to the binary gates, i.e., OR and AND). The i-th section of $\mathcal {A}$ represents information about the i-th gate. For example, the left-most section of $\mathcal {A}$ describes the gate 0 by stating that X holds in the left-most timestamp in this section. On the other hand, the third section from the left describes the OR gate by stating that D holds in the third from the left timestamp in this section (which expresses that the gate number 2 is an OR gate), that $I_1$ holds in the first timestamp from the left in the section (which expresses that the gate number 0 is the first input to the OR gate), and that $I_2$ holds in the second timestamp from the left in the section (which expresses that the gate number 1 is the second input to the OR gate).

We can now construct an ontology that allows checking unsatisfiability of any circuit. The ontology uses two more atoms T and F, which stand for ‘true’ and ‘false’ and which allow us to simulate propagation of signals in the circuit:

A possible propagation of T and F enforced by the ontology is shown in the previous picture with T and F written in grey. A given circuit is unsatisfiable iff the right-most timestamp in $\mathcal {A}$ is a certain answer to an OMAQ consisting of the above ontology and the query F.

(ii) The proof is by reduction of path system accessibility (PSA) which consists of checking whether there exists a hyperpath between two nodes in a hypergraph (the problem is well-known to be $\textsc {P}$-complete). For example, assume that a hypergraph contains vertices 0, 1, 2, 3, and a single hyperedge (0, 1, 2). Suppose we want to check whether the vertex $t=3$ is accessible from the set of vertices $S=\{ 0,1 \}$, i.e., whether $t \in S$ or there are vertices u, w accessible from S and (u, w, t) is a hyperedge. For such an instance of PSA, we construct the following data instance $\mathcal {A}$:

We next define an $\textit{MTL}_{core}^-$-ontology $\mathcal {O}$ with the axioms:

Then $4k \! + \!t/N$ is a certain answer to $(\mathcal {O},R)$ over $\mathcal {A}$ iff t is accessible from S in G.

We prove (iii) by reduction of the NL-complete reachability problem in acyclic digraphs. As an example, assume that we want to check whether $t=3$ is accessible from $s=0$ in the following directed graph G:

To this end, we construct a data instance $\mathcal {A}_G$, whose initial segment (corresponding to the edge from 0 to 2) is depicted below:

Let $\mathcal {O}$ be a $\textit{MTL}_{core}^-$-ontology with the following rules:

Then $4k + t/N$ is a certain answer to $(\mathcal {O},R)$ over $\mathcal {A}$ iff t is reachable from s in G.   $\square$

In the next theorem, we show that, for each $\textit{MTL}_{horn}^-$-OMAQ, there is a rewriting to datalog queries with additional FO-formulas built from EDB predicates in their rule bodies, answering which is in P  [45].

Theorem 37

Every $\textit{MTL}_{horn}^-$-OMAQ is datalog(FO)-rewritable, and so can be answered in $\textsc {P}$ for data complexity.

Proof

(Sketch). To illustrate how one can construct a datalog(FO)-rewriting, we consider the $\textit{MTL}_{horn}^-$-OMAQ ${\textit{\textbf{q}}}= (\mathcal {O}, \textit{Alert})$, where $\mathcal {O}$ consists of the axiom:

We construct a datalog(FO)-rewriting $(\Pi ,G)$ of ${\textit{\textbf{q}}}$. We will use $\textit{suc} (x,y)$ stating that x is the immediate successor of the timestamp y.

The first block of $\Pi$ has the following rules for every atom B occurring in ${\textit{\textbf{q}}}$:

$$\begin{aligned}&B(x) \rightarrow B'(x,x),&B'(x,y) \wedge B'(z,z) \wedge \textit{suc}(y,z) \rightarrow B'(x,z). \end{aligned}$$

Intuitively, instead of unary predicates B(x) stating that B holds at a timestamp x, we want to obtain binary predicates $B'(x,y)$ stating that B holds in the interval [x, y] (i.e., in all timestamps from the temporal domain that belong to this interval). The first rule converts B(x) into $B'(x,x)$, while the second rule allows us to coalesce intervals by stating that if B holds in [x, y] and in z, and moreover, there is no timestamp between y and z, then B holds in [x, z].

The second block of $\Pi$ consists of rules obtained by modifying axioms in $\mathcal {O}$, where every atom B not in the scope of a metric operator is replaced by $B'(x,x)$, whereas atoms in the scope of metric operators are replaced by corresponding formulas using predicates such as $\delta _{< a}$ and $\delta _{> a}$. In particular, in our example the single rule in $\mathcal {O}$ would be replaced with:

Finally, the program $\Pi$ contains the rule

$$ \textit{Alert}'(x,x) \rightarrow G(x), $$

which states that if A holds at x, then G also holds at x.

Now, for every data instance $\mathcal {A}$, t is a certain answer to ${\textit{\textbf{q}}}$ over $\mathcal {A}$ iff t is an answer to $(\Pi , G)$ over $\mathcal {A}$. As a result, $(\Pi ,G)$ is a datalog(FO)-rewriting of ${\textit{\textbf{q}}}$.

Note that so far we have assumed that $\mathcal {A}$ is in the signature (3). However, this assumption does not differentiate between small (e.g., 0.01) and large (e.g., 1000.00000001) timestamps in $\mathcal {A}$. Instead, we can consider $\mathcal {A}$ in a different signature using binary predicates $\textit{bit}(i,j)$ indicating that the integer part of the timestamp i has bit j equal to 1, and analogous predicates for the fractional part. In this new representation of $\mathcal {A}$, we do not assume the predicates $\delta _{<a}(x,y)$ and $\delta _{=a}(x,y)$, however, we can express them as FO$(<)$-formulas $\varphi _{<a}(x,y)$ and $\varphi _{=a}(x,y)$ with the predicates $\textit{bit}$ (see  [75] for details). The predicate $\textit{suc} (x,y)$ is also expressible in the new representation as $(y< x) \wedge \lnot \exists z\,(y< z < x)$.   $\square$

The next theorem establishes rewritability into FO(TC) that extends FO$(<)$ with the transitive closure operator. In complexity-theoretic terms, FO(TC) corresponds to NL  [56].

Theorem 38

Every $\textit{MTL}_{core}^-$-OMAQ with an ontology containing operators only is FO(TC)-rewritable, and so can be answered in $\textsc {NL}$ for data complexity.

Proof

(Sketch). Let ${\textit{\textbf{q}}}= (\mathcal {O},A)$ be an $\textit{MTL}_{core}^-$-OMAQ with operators only. First, we delete all disjointness constraints of the form $C_1 \wedge C_2 \rightarrow \bot$ from $\mathcal {O}$ and we translate the query into datalog(FO) in the same way as we did in the proof of Theorem 37. Since ${\textit{\textbf{q}}}$ is core, by the form of this translation, we obtain a linear datalog(FO) program. It is well-known that such a program can be transformed into an FO(TC)-query $\varPsi _A(x)$  [45]. For every disjointness constraint $C_1 \wedge C_2 \rightarrow \bot$ in $\mathcal {O}$, we take the sentence $\exists x\, (\varPsi _{C_1}(x) \wedge \varPsi _{C_2}(x))$ and, finally, form a disjunction of $\varPsi _A(x)$ with those sentences, which is an FO(TC)-rewriting of ${\textit{\textbf{q}}}$.   $\square$

The rewritability results we are going to present next impose restrictions on the range of metric operators: in particular, we consider ontologies with unbounded ranges of the form $\langle r, \infty )$, for $r \in \mathbb {Q}_2^{\ge 0}$ and $\langle$ being ( or [, punctual ranges [r, r], for $r\in \mathbb {Q}_2^{\ge 0}$, and non-punctual ranges.

Theorem 39

Every $\textit{MTL}^-$-OMAQ ${\textit{\textbf{q}}}= (\mathcal {O}, A)$ with temporal operators in $\mathcal {O}$ of the form

• and $\boxminus _{\langle r, \infty )}$ only is $FO (<)$-rewritable, and so can be answered in $\textsc {AC}^0$;

• and $\boxminus _{[r,r]}$ only is FO(RPR)-rewritable, and answering such OMAQs is $\textsc {NC}^1$-complete for data complexity;

• and $\boxminus _\varrho$, for non-punctual $\varrho$, only is FO(TC)-rewritable; answering such OMAQs is in $\textsc {NL}$ and $\textsc {NC}^1$-hard for data complexity.

Moreover, $\textit{MTL}_{horn}^-$-OMAQs from the last item are also FO(DTC)-rewritable (FO with deterministic transitive closure), and so answering them is in L for data complexity. These rewritings heavily depend on the properties of the minimal models of OMAQs of a given type. For example, in the case of MTL-OMAQ with temporal operators of the forms and $\boxminus _{\langle r, \infty )}$ only, we can observe that the minimal model is monotonic in the sense that if holds in a timestamp t, then the same formula holds in all timestamps greater than t. Analogously, if does not hold in a timestamp t, then this formula holds in all timestamps smaller than t. It turns out that we can use this observation (and some additional properties of the minimal model) to construct an $FO (<)$-rewriting. For more details of the constructions we refer the reader to  [75].

So far in this section we discussed MTL-OMAQs. What do we know about wider classes of MTL OMQs (under the pointwise semantics)? First, we have:

Theorem 40

Every $\textit{MTL}$ OMQ ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ with an $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$-formula $\psi (\textit{\textbf{t}})$ is coNP-complete for data complexity.

Note that the counterpart of this result in LTL is Theorem 13. Furthermore, we say that $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$-formula is positive, if it is constructed using $\wedge$, $\vee$, $\forall$, $\exists$. We say that an $\textit{MTL}$-OMQ ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ is positive, if $\psi (\textit{\textbf{t}})$ is a positive $MFO (<,\delta _{\le \mathbb {Q}_2},\delta _{= \mathbb {Q}_2})$-formula. The following result follows from  [75]:

Theorem 41

Suppose ${\textit{\textbf{q}}}= (\mathcal {O},\psi (\textit{\textbf{t}}))$ is a positive $\textit{MTL}_{horn}$-OMQ and $\mathcal {L}$ a language containing FO$(<)$. Suppose also that, for each atomic A in $\psi$, the OMAQ $(\mathcal {O}, A)$ is $\mathcal {L}$-rewritable. Then, ${\textit{\textbf{q}}}$ is also $\mathcal {L}$-rewritable.

Therefore, by Theorems 37, 38, and 39, we obtain:

Corollary 42

(i) Every positive $\textit{MTL}_{horn}^-$-OMQ is datalog(FO)-rewritable.

(ii) Every positive $\textit{MTL}_{core}^-$-OMQ with an ontology containing operators only is FO(TC)-rewritable.

(iii) Every positive $\textit{MTL}^-$-OMQ with an ontology containing and $\boxminus _{\langle r, \infty )}$ operators only is $\text {FO}(<)$-rewritable.

(iv) Every positive $\textit{MTL}^-$-OMQ with an ontology containing and $\boxminus _{[r,r]}$ operators only is FO(RPR)-rewritable.

(v) Every positive $\textit{MTL}^-$-OMQ with an ontology containing and $\boxminus _\varrho$ for non-punctual $\varrho$ only is FO(TC)-rewritable.

It is of interest to compare the results above to the results in the $\textit{LTL}{}$ case given by Corollary 21. The latter results also hold for positive OMQs, since every positive OMQ is also monotone. The comparison shows that, even in the case of positive Horn OMQs, the complexity landscape is more diverse for $\textit{MTL}{}$ than for $\textit{LTL}{}$.

6 Future Research

In this paper, we have tried to overview recent developments in ontology-based access to temporal data, focusing primarily on the problem of rewriting temporal ontology-mediated queries into first-order queries over the data. For other aspects of temporal OBDA the reader is referred to the survey  [9]. Compared to the classical atemporal OBDA, its temporal counterpart is still an infant, from both theoretical and especially practical points of view. In the remainder of this concluding section, we briefly discuss a few open problems and directions for future research that are related to OBDA with LTL, MTL and temporal DL-Lite.

LTL. The classical OBDA theory has recently investigated the fine-grained combined and parameterised complexities of OMQ answering and the succinctness problem for FO-rewritings  [15, 20,21,22]. These problems are of great importance for the temporal case, too (in particular, because the rewritings discussed above are far from optimal). Another development in the classical OBDA theory is the classification of single ontologies and even OMQs according to their data complexity and rewritability  [51, 66, 67]. Extending this approach to temporal OMQs will most probably require totally different methods because of the linearly ordered temporal domain.

Temporal DL-Lite. The technique considered above does not seem to work for (two-sorted) conjunctive queries in place of instance queries; on the other hand, the methods of  [7] indicate a somewhat different approach to deal with not necessarily tree-shaped conjunctive queries having multiple answer variables. It is of interest what happens with OMAQs when we consider Krom role inclusions. There are two open questions: the upper bound for OMAQs and FO-rewritability of $\textit{DL-Lite}_{\textit{krom}}^\Box$ and OMAQs. We conjecture that $\textit{DL-Lite}_{\textit{krom}}^\Box$ OMAQs are FO$(<)$-rewritable and OMAQs are FO$(<,\equiv _{\mathbb {N}})$-rewritable. To show this, one may need a type-based technique similar to the approach in the proof of Theorem 18 as Theorem 29 is not applicable to Krom role inclusions. Another open question is the upper bound for OMAQs. On the practical side, more real-world use cases are needed to understand which temporal constructs are required to specify relevant temporal events and evaluate the performance of OMQ rewritings; for some activities in this direction we refer the reader to  [17, 24, 25, 58].

MTL. Much less is known about OMQs with $\textit{MTL}$-ontologies than about ontologies with LTL-operators. The results presented in this paper show that some MTL-ontologies can be rewritten to FO (and its extensions), which indicates that reasoning with such ontologies may be feasible in practise. However, the computational properties of MTL-ontologies heavily depend on many aspects, such as the form of available metric operators and the type of ranges they use. The results presented in the previous section are only preliminary observations, and we are clearly far from understanding well the complexity of answering MTL-OMQs and classifying them accordingly. Here we mention some interesting open problems. Observe that Theorem 39 about OMAQs with non-punctual ranges contains a gap between $\textsc {NL}$ and ${{\textsc {NC}^1}}$, and between $\textsc {L}$ and ${{\textsc {NC}^1}}$. It would be interesting to establish tight complexity bounds for such OMAQs, as non-punctuality of ranges is a standard approach in MTL, which often allows one to reduce significantly the computational costs  [2]. There are also many types of MTL-OMQs that have not been considered so far, for example, the ones with the ‘since’ and ‘until’ operators, as well as more complex queries, such as quasi-positive, or general (used in LTL-OMQs).

Another direction of future work concerns adopting the continuous semantics. Interestingly, such an approach has been already considered with respect to extensions of Datalog with $\textit{MTL}$-operators  [26, 82] and applied, for example, to stream reasoning  [48, 49, 63, 83]. It is also worth mentioning that there is work on combining DLs with MTL [11, 47]. As there is a big variety of potential applications of ontologies with MTL-operators, for instance, to image sequence evaluation [27], to ambient intelligence context [18, 70], or to online monitoring asynchronous systems  [14, 37, 53], among others, this direction of research looks very promising.