Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics

1 Introduction

We are concerned with the following problem: given a formula Π of metric temporal logic MTL and an atomic proposition A, is it possible to construct a query Q(x) in some standard query language such that, for any data instance D of atoms timestamped with binary fractions and any timestamp t from D, we have Π, D |= A(t) iff Q(t) is true in D?

MTL was originally designed for modelling and reasoning about real-time systems [Koymans, 1990; Alur and Henzinger, 1993; Bouyer et al., 2018]. Recently, combinations of MTL with description logics have been suggested as temporal ontology languages [Gutiérrez-Basulto et al., 2016b; Baader et al., 2017]. Datalog with MTL-operators was used by [Brandt et al., 2018] for practical ontology-based access to log data aiming to facilitate detection of events in asynchronous systems based on sensor measurements. For example, a Siemens turbine has a coast down if the rotor speed was below 1500 in the previous 30 seconds, while no more than 2 minutes before that the speed was above 6600 for 30 seconds. The event 'coast down' can be encoded by the following MTL-formula, where diamondminus(r,s]ϕ (⊟(r,s]ϕ) is true at a timestamp t if ϕ holds at some (respectively, all) t′ with r < t - t′ ≤ s:

To find when a coast down occurred, a Siemens engineer can now simply execute the query cdown(x) mediated by this formula. Answering datalogMTL queries in the streaming setting was considered by [Wał˛ega et al., 2019].

The underpinning idea of classical ontology-based data access (OBDA) [Calvanese et al., 2007; Xiao et al., 2018] is a reduction of ontology-mediated query (OMQ) answering to standard database query evaluation. As known from descriptive complexity [Immerman, 1999], the existence of such reductions, or rewritings, is closely related to the data complexity of OMQ answering, which is by now well understood for atemporal OMQs both uniformly (for all OMQs in a given language) and non-uniformly (for individual OMQs) [Gottlob et al., 2014; Bienvenu and Ortiz, 2015; Bienvenu et al., 2014; Lutz and Sabellek, 2017].

Temporal ontology and query languages have attracted attention of datalog and description logic communities since the 1990s; see [Baudinet et al., 1993; Chomicki and Toman, 1998; Lutz et al., 2008; Artale et al., 2017] for surveys. In recent years, the proliferation of temporal data from various sources and its importance for analysing the behaviour of complex systems and decision making in all economic sectors have intensified research into formalisms that can be used for querying temporal databases and streaming data [Soylu et al., 2017; Beck et al., 2018; Ronca et al., 2018]. OBDA with atemporal ontologies and query languages with linear temporal logic LTL operators has been in use since [Baader et al., 2013; Özçep and Möller, 2014]. Rewritability and data complexity of OMQs in the description logics DL-Lite and EL extended with LTL operators were considered in [Artale et al., 2015; Gutiérrez-Basulto et al., 2016a].

Here, we investigate the (uniform) rewritability and data complexity problems for basic OMQs given in metric temporal logic MTL, assuming that data instances are finite sets of atoms timestamped by dyadic rationals and that MTL is interpreted under the event-based semantics where atoms refer to events (state changes) rather than to states themselves [Ouaknine and Worrell, 2008]. MTL is more succinct, expressive, and versatile compared to LTL, being able to model both synchronous (discrete) and asynchronous (real-time) settings.

First, we observe that answering arbitrary MTL-OMQs is CONP-complete for data complexity (in contrast to NC1 - completeness for LTL-OMQs). OMQs in the Horn fragment hornMTL are P-complete and rewritable to datalog(FO), which extends datalog with FO-formulas built from EDB predicates; in fact, we establish P-hardness already for the fragment coreMTL⊟ of hornMTL with binary rules (like in OWL2QL) and box operators only. OMQs in coreMTLdiamondminus turn out to be FO(TC)-rewritable (FO with transitive closure) and NL-hard. We then classify MTL-OMQs by the type of ranges ϱ constraining their temporal operators diamondminusϱ and ⊟ϱ: infinite (r,∞) and [r,∞), punctual [r, r], and arbitrary nonpunctual ϱ. We show that OMQs of the first type are FOrewritable and can be answered in AC0 . OMQs of the second type are FO(RPR)-rewritable (FO with relational primitive recursion) and NC1 -complete. For the third type, we obtain an NL upper bound with rewritability to FO(TC) and NC1 lower bound; for hornMTL-OMQs of this type, the results are improved to L with rewritability to FO(DTC) (FO with deterministic closure).

The omitted proofs can be found in [Ryzhikov et al., 2019].

2 MTL Ontology-Mediated Queries

In the context of event monitoring, we consider a 'past' variant of MTL, which is a propositional modal logic with constrained operators diamondminusϱ 'sometime in the past within range ϱ' and ⊟ϱ 'always in the past within range ϱ,' interpreted over finite timed words under the event-based semantics. We assume that timestamps in timed words are given as nonnegative dyadic rational numbers (finite binary fractions), the set of which is denoted by Q≥0 2 . The ranges ϱ in diamondminusϱ and ⊟ϱ are non-empty intervals with end-points in Q≥0 2 ∪ {∞}.

An MTL-program, Π, is a finite set of rules of the form

where each ϑi takes the formA, diamondminusϱA, or ⊟ϱA, for an atomic proposition A. We denote the empty ∧ by ⊤ (truth) and empty ∨ by ⊥ (falsehood). Using fresh atoms, every MTL-formula can be transformed to an equivalent (in the sense of giving the same answers to queries) MTL-program.

An MTL-program is called a hornMTL-program if, in all of its rules (1), l ≤ 1 and ϑk+1 is an atom. As usual, ϑk+1 is called the head of the rule and ϑ1 ∧ · · · ∧ ϑk its body. A hornMTL-program is a coreMTL-program if k + l ≤ 2. An MTL- (hornMTL- or coreMTL-) ontology-mediated query (OMQ) takes the form q = (Π,A), where Π is an MTL(resp., hornMTL- or coreMTL-) program and A an atom.

Intuitively, a data instance, D, can be thought of as a word A0(¯0), . . . ,Ak(¯ k) with timestamps ¯0 < · · · < ¯ k, ¯i ∈ Q≥0 2 , where each Ai is the set of atoms that are true at ¯i. Formally, we represent D as the FO-structure

with domain ∆ = {0, . . . , ℓ} ordered by <, timestamps Θ = {0, . . . , k}, 1 ≤ k ≤ ℓ, and subsets ADi ⊆ Θ. The ternary predicates bitin and bitfr are such that, for any n ∈ Θ and i ∈ ∆, there are unique bi, ci ∈ {0, 1} with bitin(n, i, bi) and bitfr (n, i, ci). These predicates give the value ¯n ∈ Q≥0 2 of every timestamp n ∈ Θ: ¯n = bℓ . . . b0.cℓ . . . c0 iff bitin(n, i, bi) and bitfr (n, i, ci) hold for all i ≤ ℓ. We assume that ¯n < ¯m if n < m. For any r ∈ Q≥0 2 , we can define an FO-formula dist<r(x, y) that holds in D iff x, y ∈ Θ and 0 ≤ ¯x - ¯ y < r, its variants dist>r(x, y), dist=r(x, y), etc. Using these, we can further define FO-formulas inϱ(x, y) for ¯x - ¯ y ∈ ϱ, suc(x, y) for 'x is an immediate successor of y in D', and FO-expressible constants min = 0 and max = k.

An event-based interpretation over D is a structure

where the Boolean connectives are interpreted as usual and

An interpretation I over D is a model of an MTL-program Π and D if, for any rule (1) in Π and any t ∈ Θ, whenever t ∈ ϑIi for all i, 1 ≤ i ≤ k, then t ∈ ϑIk+j for some j, 1 ≤ j ≤ l. We call D and Π consistent if there is a model of Π and D.

Henceforth, we write ts(D) for the set Θ of timestamps in (2) and often informally identify t ∈ ts(D) with its value ¯ t. We call t ∈ ts(D) (and so ¯ t) a certain answer to q = (Π,A) over D if t ∈ AI for every model I of D and Π. The OMQ answering problem for q is to decide, given D and t ∈ ts(D), whether t is a certain answer to q over D. To illustrate, consider Π = {⊟[0,2)B → B′ , diamondminus[1,1]B′ → A}, D1 = {B(0), B(1/2), C(3/2)} and D2 = {B(0), C(3/2)}. Then 3/2 is a certain answer to (Π, A) over D1, but there are no certain answers to (Π, A) over D2:

We are interested in the data complexity of OMQ answering, that is, regard D as the only input to the problem and assume q to be fixed.

Let L be a query language over FO-structures (2). An OMQ q is said to be L-rewritable if there is an L-query Q(x), called an L-rewriting of q, such that, for any data instance D, a timestamp t ∈ ts(D) is a certain answer to q over D iff D |= Q(t). Our target query languages L include:

• FO(<) and its extension FO(<,+) with the predicate PLUS (e.g., ∃xPLUS(x, x,max) says that |Θ| is odd); evaluating such queries is in AC0 for data complexity;
• FO(RPR), i.e., FO(<) with relational primitive recursion, which is in NC1 [Compton and Laflamme, 1990];
• FO(TC) and FO(DTC), i.e., FO(<) with transitive and deterministic transitive closure, which are in NL and L, respectively [Immerman, 1999];
• datalog(FO), i.e., datalog queries with additional FOformulas built from EDB predicates in their rule bodies, which are in P [Grädel, 1991].

All of them save datalog(FO) can be implemented in SQL. Lrewritability of an OMQ q means that answering q is in the same data-complexity class as evaluation of L-queries.

Given a hornMTL-program Π and a data instance D, we define a set CΠ,D of pairs of the form (ϑ, t) that contains all answers to OMQs with Π over D. We start by setting C = D and denote by cl(C) the result of applying exhaustively and non-recursively the following rules to C:

• if ϑ1 ∧ · · · ∧ ϑk → ϑ is in Π and (ϑi, t) ∈ C, for all i, 1 ≤ i ≤ k, then we add (ϑ, t) to C;
• if diamondminusϱB occurs in Π, (B, t′ ) ∈ C, and inϱ(t, t′ ) holds for some t ∈ ts(D), then we add (diamondminusϱB, t) to C;

• if ⊟ϱB occurs in Π, t ∈ ts(D) and (B, t′ ) ∈ C for all t′ ∈ ts(D) with inϱ(t, t′ ), then we add (⊟ϱB, t) to C.

It should be clear that there is some N < ω polynomially depending on Π and D such that clN (C) = clN+1 (C). We then set CΠ,D = clN (D). We can regard CΠ,D as a (minimal) model of Π and D with domain ts(D) in which t ∈ BCΠ,D iff (B, t) ∈ CΠ,D The proof of the following is standard:

Theorem 1. For a hornMTL-OMQ (Π, A), (i) Π is inconsistent with D iff (⊥, t) ∈ CΠ,D; (ii) a timestamp t ∈ ts(D) is a certain answer to a hornMTL-OMQ (Π, A) over D iff either CΠ,D |= A[t] or Π is inconsistent with D.

Note in passing that, as a consequence, we obtain the following reduction of L-rewritability of more general hornMTL-OMQs (Π, ϕ) with positive FO-queries ϕ (built from atoms, ∧, ∨, ∀, and ∃) to L-rewritability of atomic OMQs we deal with in this paper:

Corollary 2. Let (Π, ϕ) be a hornMTL-OMQ with a positive FO-query ϕ. If (Π,A) has an L-rewriting QA(x), for every atom A in ϕ, then the result of simultaneous replacing every A(x) in ϕ with QA(x) is an L-rewriting of (Π, ϕ).

3 OMQs with Arbitrary Ranges

We begin by establishing (non-)rewritability and data complexity of answering OMQs in various classes where arbitrary ranges in temporal operators are allowed. We denote by coreMTL⊟ (coreMTLdiamondminus) the restriction of coreMTL to the language with operators ⊟ϱ (respectively, diamondminusϱ) only.

Theorem 3. (i) Answering MTL-OMQs is CONP-complete for data complexity; (ii) hornMTL-OMQs are datalog(FO)- rewritable, with coreMTL⊟-OMQs being P-hard; (iii) coreMTLdiamondminus-OMQs are FO(TC)-rewritable and NL-hard.

Proof sketch. (i) The membership in CONP is trivial. We establish CONP-hardness by reduction of NP-complete circuit satisfiability [Arora and Barak, 2009]. Let C be a Boolean circuit with N0-many (two-input) AND, OR and (one-input) NOT gates enumerated by consecutive numbers starting from 0 so that if there is an edge from n to m, then n < m. Take the minimal N = 2k ≥ N0 and a data instance DC with the facts

• A(2n + i/N), if n is a gate and 0 ≤ i < N0;
• X(2n+n/N), if n is an input gate;
• N(2n+n/N), if n is a NOT gate;
• D(2n+n/N), if n is an OR gate;
• C(2n+n/N), if n is an AND gate;
• I0(2n +m/N), if n is a NOT gate with input gate m;
• I1(2n+m/N) and I2(2n+k/N), if n is anOR or AND gate with input gates m and k.

Let ΠC be an MTL-program with the following rules:

Then C is satisfiable iff the maximal number in ts(D) is not a certain answer to (ΠC, F) over DC. An example of C and an initial part of a model of ΠC, DC is shown below:

2

and similarly for other types of ranges ϱ in diamondminusϱB. Intuitively, Π′ ,D |= B′ (x, y) iff (B, t) ∈ CΠ,D, for each t ∈ [x, y] from ts(D). We replace every ⊟[r,s]B in the body of a rule with

and similarly for other types of ranges. Finally, we add the following rules to the resulting program:

Note that the obtained datalog program Π′ contains FOdefinable EDB predicates such as dist≥r(x, w) and suc(y, z) in rule bodies. Clearly, t is a certain answer to q over any given data instance D iff t is an answer to (Π′ , G(x)) over D. The proof of hardness via PSA is similar to that in (iii).

(iii) The upper bound can be shown by reduction to FO(TC) via linear datalog(FO). We prove NL-hardness by reduction of the reachability problem in acyclic digraphs. Let G be such a digraph with N0 vertices enumerated by consecutive natural numbers starting from 0 so that, if there is an edge from n to m, then n < m. Let e0, . . . , ek-1 be the lexicographical order of edges. Take the minimal N = 2i ≥ N0 for i ∈ N. Suppose we want to check whether a vertex t is accessible from s. Let DG consist of the atoms A(4i+n/N), for 0 ≤ i ≤ k and a vertex n; A(2+4i+n/N), A(2+4i+m/N), for every edge ei = (n, m); R(4i + s/N), for 0 ≤ i ≤ k. An example of G and an initial part of DG is shown below:

Let Π be a coreMTLdiamondminus program with the following rules:

Then 4k + t/N is a certain answer to (Π, R) over DG iff t is reachable from s in G. q

To obtain finer complexity results, we classify MTLOMQs by the type of ranges ϱ in their operators diamondminusϱ and ⊟ϱ: infinite, punctual, and non-punctual. Let 〈 be one of ( or [.

4 OMQs with Ranges 〈r,∞)

First, consider OMQs with diamondminus〈r,∞) and ⊟〈r,∞), which resemble LTL-operators 'sometime' and 'always in the past'. Using partially-ordered automata, [Artale et al., 2015] showed that LTL-OMQs with these operators are FO-rewritable. Although such automata are not applicable now, we establish the same complexity by characterising the structure of models. In the constructions below, it will be convenient to regard ⊟ϱ as an abbreviation for ¬diamondminusϱ¬ with Boolean negation ¬ and only consider w.l.o.g. OMQs (Π, A) with A occurring in Π.

Theorem 4. MTL-OMQs with temporal operators of the form diamondminus〈r,∞) and ⊟〈r,∞) only are FO(<)-rewritable.

Proof sketch. Let q = (Π, A) be an MTL-OMQ as specified above. A simple literal, σ, for Π takes the form P or ¬P, where P is an atom in Π; a temporal literal, τ , for Π is of the form diamondminusϱσ or ¬diamondminusϱσ provided that diamondminusϱP or ⊟ϱP occurs in Π and P is the atom in σ. Let ΣΠ and ΞΠ be the sets of simple and temporal literals for Π, respectively. A type for Π is any maximal set t ⊆ ΣΠ ∪ ΞΠ consistent with Π. The number of different types is NΠ = 2O(|Π|) .

Given a model I of Π and some D with s ∈ ts(D), denote by t(s) the type of s in I. As the ranges in Π are of the form 〈r,∞), the model I has the following monotonicity property:

We call t(s) in I an osteo-type if there is λ ∈ t(s) such that λ /∈ t(s′ ), for all s′ < s. Thus, if diamondminusϱσ ∈ t(s′ ) in I, there is an osteo-type t(s) ∋ σ with inϱ(s′ , s). All osteo-types in I are pairwise distinct, so the number of them does not exceed NΠ. Non-osteo-types are called fluff-types. By monotonicity, any fluff-type t(s′ ) has the same temporal literals as its nearest osteo-type t(s), for s < s′ . For example, in the model of the program Π = {⊟ϱP ∧ diamondminusϱP ∧ P → ⊥}, ϱ = [1,∞), shown below, there are three fluff-types: t(3/4), t(9/8), and t(5/4).

We now define an FO-sentence ΦΠ such that any given data instance D is consistent with Π iff ΦΠ holds in the FOstructure D. Let OΠ be the set of sequences ¯t = (t1, . . . , tn), 1 ≤ n ≤ NΠ, of distinct types for Π that satisfy the monotonicity property and such that diamondminusϱσ ∈ ti implies σ ∈ tj for some j ≤ i; for minimal such j, we write wit(ti, tj, ϱ). We write wit(ti, tj, ϱ) if j ≤ i, ¬diamondminusϱσ ∈ t(si) and σ ∈ t(sj), for some diamondminusϱσ. Denote by Fi¯t the set of types t for Π sharing the same temporal literals with ti and such that, for every σ ∈ t, there is tj ∋ σ with j ≤ i. Finally, for any type t, let

δt(x) = ∧¬P∈t ¬P(x) (which is true at t in D iff, for every P in Π, whenever P(t) ∈ D then P(t) ∈ t). Now, we set

where xi ≺ y says that xi is the nearest predecessor of y, which is different from x1, . . . , xn. An FO(<)-rewriting of q is the FO formula ¬Φ¬A(x), where Φ¬A(x) is obtained from ΦΠ by replacing δt(z) with δt(z, x), which is δt(z) if ¬A ∈ t and δt(z) ∧ (x ̸= z) otherwise. Clearly, Φ¬A(x) holds in D iff there is a model of Π and D satisfying ¬A in x. q

We also mention in passing one more FO-rewritability result (which does not fit our classification). Call an MTLprogram range-uniform if all of its temporal operators have the same constraining range. Let 〉 be one of ) or ].

Theorem 5. Range-uniform coreMTLdiamondminus-OMQs with ranges of the formdiamondminus〈0,r〉 are FO(<,+)-rewritable.

The proof uses automata with metric constraints that can be viewed as a primitive version of standard timed automata for MTL [Alur and Dill, 1994] as they only have one clock c, the clock reset c := 0 happens at every transition, and clock constraints are of the form c ∈ ϱ.

5 OMQs with Punctual Ranges [r, r]

Operators of the formdiamondminus[r,r] resemble the LTL previous time operator ⊖. To illustrate an essential difference, consider the program Π = {diamondminus[1,1]P → Q, diamondminus[1.5,1.5]P ∧ Q → P } and the data instance D below. In LTL, we always derive ⊖P at n+1

if P holds at n. In our example, P at 3/4 implies Q at 7/4, which together with P at 1/4 imply P at 7/4, and eventually the latter P with Q at 13/4 implies P at 13/4; independently, P at 7/8 implies Q at 15/8.

Theorem 6. MTL-OMQs with temporal operators of the form diamondminus[r,r] and ⊟[r,r] only are FO(RPR)-rewritable; answering such OMQs is NC1 -complete for data complexity.

Proof sketch. NC1 -hardness is proved by reduction of hornMTL-OMQs with rules of the form ⊖P ∧P ′ →Q, answering which is NC1 -complete [Artale et al., 2015].

To show FO(RPR)-rewritability of a given OMQ q = (Π,A), we assume w.l.o.g. that Π does not contain ranges [0, 0]. Let RΠ be the set of numbers occurring as endpoints of ranges in Π. We set 1 = gcd(RΠ), n = 1 · n, for n ∈ N, m = max(RΠ). Thus, in our example above, 1 = 1/2, 2 = 1, 3 = 3/2. We define cl (Π) to be the set of simple and temporal literals with atoms from Π and operators diamondminusi such that i ∈ {1, . . . , n} and diamondminusn occurs in Π. By a type s for Π we now mean any maximal subset of cl(Π) consistent with Π. For types s, s′ and i ∈ {1, . . . ,m}, we write s →i s′ if

• σ ∈ s iff diamondminusiσ ∈ s′ , for any diamondminusiσ ∈ cl (Π);

We say that (s0, t0), . . . , (sn, tn) is a run from t0 to tn on a data instance D of the form (2) if ti ∈ ts(D), for i ≤ n, and

• ¬diamondminusjσ ∈ s0 for all diamondminusjσ ∈ cl(Π);
• ¯ ti+1-¯ ti ∈ {1, . . . ,m} and if ti+1 > t > ti then ¯ t-¯ ti ̸∈ {1, . . . ,m}, for any t ∈ ts(D);

- si →(¯ ti+1-¯ ti) si+1 and {P ∈ΣΠ | ti+1 ∈ P D } ⊆ si+1. Call t ∈ ts(D) initial if ¯ t - ¯ t′ ̸∈ {1, . . . ,m}, for all

t′ ∈ ts(D). The next lemma follows directly from the given definitions:

Lemma 7. (i) (Π,D) is consistent iff, for every t ∈ ts(D), there exists a run on D from some initial t′ ≤ t to t; (ii) A timestamp t ∈ ts(D) is not a certain answer to q over D iff (Π,D) is consistent and there is a run (s0, t0), . . . , (sn, tn) from initial t0 to t = tn on D and ¬A ∈ sn.

We first show how to express the existence of a run from x to y specified in (ii) by an FO(RPR)-formula runq(x, y) over D. First, as divisibility of binary integers by a given number is recognisable by a finite automaton, we can define an FO(RPR)-formula div1(u, v) that is true iff ¯u - ¯ v = n1, for some n ∈ N. We also have an FO-formula lasti(u) saying that i is minimal among {1, . . . ,m} with ¯u - i = ¯ v, for some v ∈ ts(D). Let Q = {s1, . . . , sn} be the set of all types for Π, and let Q0 ⊆ Q comprise s with ¬diamondminusjσ ∈ s, for all diamondminusjσ ∈ cl (Π). We define runq(x, y) as the FO(RPR)-formula

where Rs(x, z), for s ∈ Q, is a relation variable and the formula ϑs(x, z, Rs1 (x, z -1), . . . , Rsn (x, z -1)) is a disjunction of the three formulas below if s ∈ Q0 and a disjunction of the last two of them if s /∈ Q0:

where z - 1 is the immediate predecessor of z in ts(D).

To illustrate, in the context of the example above, the formulas Rs ≡ ϑs say that Rs(1/4, 1/4) holds for the types

Then Rs(1/4, 3/4) holds for

Rs(1/4, 7/8) for the same s as Rs(1/4, 3/4), Rs(1/4, 7/4) for s = {¬diamondminus1P, diamondminus2P, diamondminus3P, P, Q}, and so on.

Thus, we obtain the following FO(RPR)-rewriting of q

where ΦΠ checks the consistency condition of Lemma 7 (i) and can be constructed similarly to runq. q

6 OMQs with Non-Punctual Ranges

Unlike the proof of Theorem 6, where the derived facts at t were determined by the data D at t and the derived facts at the nearest t′ ∈ ts(D) with ¯ t′ = ¯ t - i, for non-punctual ranges the derived facts at t depend on an unbounded number of timestamps t′ < t. In the proof of Theorem 8 below, we show that to construct derivations in this case, we can actually keep track of a fixed number (depending only on the given OMQ) of moments t′P < t where each P was derived.

Theorem 8. (i) MTL-OMQs whose operators diamondminusϱ and ⊟ϱ have non-punctual ϱ are FO(TC)-rewritable; answering them is in NL and NC1 -hard; (ii) hornMTL-OMQs of this kind are FO(DTC)-rewritable; answering them is in L and NC1 -hard.

Proof sketch. In both cases, NC1 -hardness can be established as in the proof of Theorem 6 by encoding ⊖ with diamondminus(0,1].

(i) Let q = (Π, A) be the given OMQ. For ϱ = 〈r, q〉 with q ̸= ∞, let ϱ- = 〈0, q - r〉 and ϱ+ = 〈0, q〉; if q = ∞, ϱand ϱ+ are undefined. Let ΣΠ be the set of all σ with diamondminusϱσ in Π, for some ϱ. For σ ∈ ΣΠ, let ϱ-σ (ϱ+σ ) be the intersection (union) of the defined ϱ- (ϱ+) with diamondminusϱσ in Π; if there are no such diamondminusϱσ, ϱ-σ and ϱ+σ are undefined. To illustrate, consider the hornMTL-program Π with the rules

For a data instance D, a trace of length ℓ for t ∈ ts(D) is a sequence of intervals [u0, s0], . . . , [uℓ, sℓ] where either [ui, si] = [∗, ∗] (meaning that this interval is undefined) or ui, si ∈ ts(D), u0 = s0, and u1 ≤ s1 < u2 ≤ s2 < · · · < uℓ ≤ sℓ ≤ t, assuming that ∗ < u, for any u. Thus, for the data instance D below,

([ 1 2 , 12 ], [∗, ∗], [∗, ∗], [ 12 , 54 ], [ 52 , 52 ]) is a trace for t = 5/2. Intuitively, such a trace stores the most recent ℓ intervals preceding t where a simple literal holds at some point, with [u0, s0] storing the very first point where the literal holds. A tuple (t, (trσ)σ∈ΣΠ , t) is an extended type for t ∈ ts(D) if

• t is a type for Π (as in the proof of Theorem 4);
• trσ is a trace for t of length ℓσ = ⌈|ϱ+σ |/|ϱ-σ |⌉, where |ϱ+σ | and |ϱ-σ | denote the end-points of these intervals; if one of the intervals is undefined, ℓσ = 0;

- diamondminusϱσ ∈ t iff intϱ(t, ui, si), for some [ui, si] in trσ, where intϱ(t, u, s) is true iff {¯ t - k | k ∈ ϱ} ∩ [¯u, ¯ s] ̸= ∅ and u, s ̸= ∗. In our example, ℓP = 4, ℓQ = 0, and the following triples (ti, (triσ )σ∈ΣΠ , ti) are extended types for ti:

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

Intuitively, an extended type records the simple and temporal literals that hold at t (the type t) and also some history of the validity of σ (the traces) justifying the presence of diamondminusϱσ in t. As follows from Lemma 9 below, to make correct derivations, this history should keep ℓσ +1 intervals. Note that this bound does not apply if punctual intervals are present in Π, which explains the increase of complexity in Theorem 3.

Lemma 9. Let t0 < · · · < tm be all the timestamps in D. Then Π and D are consistent iff there exists a sequence (ti, (triσ )σ∈ΣΠ , ti) of extended types for ti, 0 ≤ i ≤ m, satisfying the following conditions for σ ∈ ΣΠ:

• {P ∈ ΣΠ | ti ∈ P D } ⊆ ti;
• if σ /∈ t0, all [uj, sj] in tr0σ are [∗, ∗]; if σ ∈ t0, then [u0, s0] = [uℓσ , sℓσ ] = [t0, t0] and [uj, sj] = [∗, ∗] for 0 < j < ℓσ;
• if σ ̸∈ ti and i > 0, then triσ = tri-1 σ ; if σ ∈ ti, tri-1 σ = ([u0, s0], . . . , [uℓσ , sℓσ ]) and [u, s] = [u0, s0] when u0 ̸= ∗ and [u, s] = [ti, ti] otherwise, then triσ = ([u, s], [u1, s1], . . . , [uℓσ , ti]) if ¯ ti - ¯ sℓσ ∈ ϱ-σ , else triσ = ([u, s], [u2, s2], . . . , [uℓσ , sℓσ ], [ti, ti]).

We use the characterisation of Lemma 9 to construct an FO(TC)-sentence ΦΠ that is true in D iff Π and D are consistent, for any data instance D. ΦΠ contains tuples of variables x = xσ1 , . . . , xσn , for {σ1, . . . , σn} = ΣΠ, where xσ = x0σ, . . . , xℓσσ and xiσ = uiσ, siσ for intervals in traces trσ; x′ is the same as x but with primed variables:

Here, firstt(x) is an FO-formula saying that t holds in the first timestamp (min) of D and x represents tr0σ for all σ by encoding [∗, ∗] as the empty interval [max, min]. The formula ξ(t, x, t′ , x′ ) under the transitive closure TC says that there is an extended type for t with the trace given by x, that t′ is the immediate successor of t in ts(D), and there is an extended type for t′ whose trace is given by x′ . We define it as

with ξt′(t, x, t′ , x′ ) saying that if (t, (trσ)σ∈ΣΠ , t) is an extended type for t with (trσ)σ∈ΣΠ given by x, then (t′ , (tr′σ )σ∈ΣΠ , t′ ) can be the next extended type with (tr′σ )σ∈ΣΠ given by x′ :

The formula extt(t, x) defines an extended type for t in D:

Finally, firstt(x) is ⊥ if there is diamondminusϱσ ∈ t and otherwise it is

saying that the intervals in the initial extended type are set correctly. That ΦΠ is as required follows from Lemma 9. One can nowmodify ΦΠ to obtain an FO(TC)-rewriting of q. q

7 Conclusion

In this paper, we made a first step towards understanding the data complexity of answering queries mediated by ontologies with MTL operators and their rewritability into standard database query languages. By imposing natural restrictions on the ranges ϱ constraining the operators diamondminusϱ and ⊟ϱ, and by distinguishing between arbitrary, Horn and core ontologies, we identified classes of MTL-OMQs that are rewritable to FO(<), FO(<,+), FO(RPR), FO(DTC), FO(TC), and datalog(FO). Unrestricted MTL-OMQs were shown to be CONP-hard. The rewritability results look encouraging, though much remains to be done to make our rewritings practical, especially in the presence of more expressive atemporal (description logic or datalog) ontologies.

We can extend our language with constrained operators since Sϱ. In this case, hornMTL remains P-complete (but coreMTL becomes P-hard) and Theorem 8 holds, too. We believe that our hornMTL can also be extended with ⊟ϱ in the rule heads (cf. [Brzoska, 1998]): Theorems 3 (ii) and 8 (i) also hold in this case, but so far we have not managed to prove Theorem 8 (ii) for such rules. Extending MTL with future-time operators is also interesting, in which case Theorems 3 and 4 remain to hold. Finally, we are looking into MTL-OMQs under the continuous (state-based) semantics, where the techniques developed above do not apply directly.

Acknowledgements

This work was supported by EPSRC UK grant EP/S032282, NCN Poland grant 2016/23/N/HS1/ 02168, and the Foundation for Polish Science (FNP). We would like to thank Stanislav Kikot for his help with the proof of Theorem 5.