Tractable Fragments of Datalog with Metric Temporal Operators

1 Introduction

DatalogMTL [Brandt et al., 2017; Brandt et al., 2018; Wał˛ega et al., 2019b] is a temporal extension of the fundamental rule language Datalog [Abiteboul et al., 1995] in which atoms in rules may contain metric temporal logic (MTL) operators interpreted over a rational timeline [Ouaknine and Worrell, 2008; Hunter et al., 2013]. For instance, DatalogMTL rule (1) states that cooling measures should be activated on a device x at time t if the device surpasses a fixed temperature threshold at some point in the interval [t - 2.5, t]; in contrast, rule (2) captures a more conservative requirement, where cooling measures are activated if the aforementioned threshold is exceeded continuously within the given time interval:

MTL is equipped with two alternative semantics: pointwise and continuous; in this paper we consider the latter, which is the one typically adopted in works on DatalogMTL.

DatalogMTL is receiving increasing attention as a suitably expressive language for querying temporal data [Brandt et al., 2018; Artale et al., 2017; Ryzhikov et al., 2019] and reasoning over streams [Wał˛ega et al., 2019a]. The use of DatalogMTL in applications is, however, handicapped by its high data complexity of reasoning, namely PSPACE-complete for consistency checking [Wał˛ega et al., 2019b]. A known alternative to regain tractability while still allowing for temporal operators in rules is to preclude recursion altogether; Brandt et al. (2018) showed that, if timestamps and intervals are represented as dyadic rational numbers (rationals given as an integer fraction where the denominator is a power of 2), reasoning in nonrecursive DatalogMTL is first-order rewritable and hence AC0 in data complexity.

∗Contact Author

In this paper, we study the data complexity of recursive fragments of DatalogMTL under continuous semantics. Our aim is to identify natural fragments with good computational properties and sufficient expressive power for data-intensive applications, while gaining a deeper understanding of interactions between constructs leading to intractability.

We first study the core fragment DatalogMTL core , where each rule with the head different from ⊥ has a singleton body; clearly, rules (1) and (2) satisfy this condition. Plain core Datalog and its extension with existential quantification in the rule heads are prominent KR languages, which can capture standard KR languages for ontology-based data access (OBDA) [Xiao et al., 2018; Motik et al., 2012]; reasoning in such languages is first-order rewritable, thus ensuring AC0 data complexity [Calì et al., 2012]. In Section 3 we show that this does not apply to our setting, as DatalogMTL core remains PSPACE-hard in data complexity, even if the since operator S is the only temporal operator allowed in rules. Operator S fully expresses the past diamond operator diamondminus (but not viceversa), and hence the rule (1) can be written using only S as a temporal operator; in contrast, S does allow us to express ⊟. This prompts us to investigate both DatalogMTLdiamondminuscore - the core fragment where diamondminus is the only temporal operator allowed-and the fragment DatalogMTL⊟core . We show that reasoning in DatalogMTLdiamondminuscore is TC0 -complete, and hence both tractable and parallelisable; however, these favourable computational properties do not transfer to DatalogMTL⊟core , for which reasoning is P-hard.

In Section 4 we consider DatalogMTL lin -the linear fragment, where rule bodies must contain at most one IDB conjunct (i.e., a conjunct whose predicate occurs in the head of some rule of the program). For instance, the program consisting of rule (3), which requires cooling measures to continue being applied if a moderate temperature is detected after cooling measures were already in force, is linear as the conjunction in (3) involves a single conjunct over IDB predicate Cool:

DatalogMTL lin extends DatalogMTL core , and hence all lower bounds proved in Section 4 transfer. To regain favourable computational properties, we focus on DatalogMTLdiamondminuslin : the linear fragment where diamondminus is the only temporal operator allowed. We then show that reasoning in this fragment is NLcomplete, and hence no harder than in plain linear Datalog [Dantsin et al., 2001]. Linear Datalog provides the foundation for recursion in SQL, and hence our results open the door to efficient implementations of temporal recursive queries.

Our results are summarised in Figure 1 for reference (recall that TC0 ⊆ NL ⊆ P ⊆ PSPACE and NL ̸= PSPACE).

2 Preliminaries

In this section, we define DatalogMTL and its associated reasoning problems [Brandt et al., 2018]. We also recapitulate some important properties of DatalogMTL proven by Wał˛ega et al. (2019b), which we exploit in our technical results.

Intervals. We consider intervals over rationals Q. An interval is denoted by 〈x, y〉, where the left bracket 〈 is [ or (, the right bracket 〉 is ] or ), and x, y ∈ Q ∪ {-∞, +∞}. Hence,

An interval 〈x, y〉 is positive if x ≥ 0; it is bounded if x, y ∈ Q; and it is punctual if it is of the form [t, t], in which case we write {t} instead of [t, t]. Each number in Q is represented by an integer numerator and a positive integer denominator, both encoded in binary (we do not require rationals to be dyadic).

Syntax. Assume a function-free first-order vocabulary with constants and predicates equipped with a non-negative arity. An atom is of the form P (τ ), with P a predicate and τ a tuple of constants and variables of matching arity. Each predicate in the vocabulary is either extensional (EDB) or intensional

(IDB). A literal A is an expression given by the following grammar, with P (τ ) an atom and ϱ a positive interval:

A literal is EDB if it mentions only EDB predicates and IDB otherwise. A (DatalogMTL) rule is an expression of the form

where each Ai is a literal and B is a literal not mentioning the operators diamondminus, diamondplus, S, and U. The conjunction of the Ai is the rule body, whereas the literal B is the rule head. A rule is safe if each variable in its head occurs also in its body. A DatalogMTL program is a finite set of safe rules. The greatest common divisor gcd(Π) of a program Π is the largest rational number dividing all rationals which are endpoints of intervals in Π to integer values (if Π has no numbers, we take gcd(Π) = 1 for definiteness). A program is core if each of its rules is of the form B ← A or ⊥ ← A1 ∧ A2. A program is linear if each of its rules is either of form (4) with at most one Ai being an IDB literal, or of the form ⊥ ← A1 ∧ A2. We denote the core and linear fragments by DatalogMTL core and DatalogMTL lin , respectively. For X ∈ {diamondminus,⊟}, and Y ∈ {core, lin}, we denote by DatalogMTLXY the fragment of DatalogMTLY where X is the only temporal operator that may occur in literals. A program is propositional if all its predicates are nullary (i.e., propositions), and it is positive if it does not mention ⊥. An expression e (e.g., an atom or a literal) is ground if it mentions no variables. A ground expression e′ is a grounding of e if e′ = eν for an assignment ν of variables to constants. A fact is α@ϱ, where α is a ground atom and ϱ is a non-empty interval. A dataset is a finite set of facts mentioning only EDB predicates.

Semantics. An interpretationMspecifies, for each ground atom α and each time point t ∈ Q, whether α is true at t, in which case we write M, t |= α. This notion extends to ground literals with temporal operators as in Table 1, where r, s, t ∈ Q. An interpretation M is a model of a rule of form (4) if, for each grounding assignment ν and each t ∈ Q, we have M, t |= Bν whenever M, t |= Aiν for each i ∈ {1, . . . , n}. An interpretation M is a model of program Π, written M |= Π, if M is a model of all rules in Π. Interpretation M is a model of fact α@ϱ, written M |= α@ϱ, if M, t |= α for all time points t ∈ ϱ, and it is a model of dataset D, writtenM |= D, if it is a model of all facts in D. Program Π and dataset D are consistent if there is a model of both Π and D. Program Π and dataset D entail fact α@ϱ, written (Π, D) |= α@ϱ, if M |= α@ϱ for each model M of Π and D. For brevity, we write D |= α@ϱ instead of (∅, D) |= α@ϱ.

Reasoning Problems. We study the complexity of consistency checking for the linear and core fragments of DatalogMTL. We focus on data complexity-the standard measure of complexity in data-intensive applications, where programs are assumed to be fixed. All our complexity results are also applicable to the entailment of punctual facts of the form α@{t}, because such entailment and inconsistency checking problems are inter-reducible in all the fragments we consider. On the one hand, (Π,D) |= α@{t} if and only if Π ∪ {⊥ ← α ∧ P } and D ∪ {P@{t}} are inconsistent, with

Table 1: Semantics of DatalogMTL ground literals

P a fresh proposition; on the other hand, Π and D are inconsistent if and only if Π and D entail a fact with a proposition not mentioned in Π or D. In contrast, all known reductions of entailment of facts with arbitrary intervals to inconsistency checking require S or U, which are not always available in our fragments. We assume without loss of generality that the least number occurring explicitly in each dataset is 0 (for a fixed program, any dataset can be modified to satisfy this assumption while preserving consistency).

Rulers. If a DatalogMTL program Π and a dataset D are consistent, then they have a unique least model (i.e., the model assigning true as little as possible) [Brandt et al., 2017]. As shown by Wał˛ega et al. (2019b), such a least model can be divided into regularly distributed intervals whose time points satisfy the same ground atoms as follows. The (Π, D)- ruler is the set of time points of the form x + n · gcd(Π), for x a number in D and n ∈ Z. A (Π,D)-interval is either a punctual interval over a time point on the ruler, or an interval (t1, t2) with t1 and t2 consecutive time points on the ruler. For a sequence ϱi, ϱi+1, . . . , ϱj of successive (Π,D)- intervals (i.e., such that ⋃i ϱi is an interval), with i ≤ j, we define the (asymmetric) distances between ϱi and ϱj as dist(ϱi, ϱj) = j - i and dist(ϱj, ϱi) = -dist(ϱi, ϱj). As an example, we present below a fragment of the (Π, D)-ruler for Π = {β ← diamondminus[0,2.5)α, γ ← diamondminus{5}β} and D = {α@(0, 1.7)}, where gcd(Π) = 2.5 and dist({0}, (2.5, 4.2)) = 5.

The following lemma by Wał˛ega et al. (2019b) shows that points in a given ruler interval satisfy the same ground atoms.

Lemma 1. For every DatalogMTL program Π, dataset D, atom α, and t ∈ Q, if (Π, D) |= α@{t}, then (Π, D) |= α@ϱ, where ϱ is the (Π,D)-interval such that t ∈ ϱ.

The (Π,D)-ruler can be divided into segments of length gcd(Π) starting from 0, such that each segment contains the same number of (Π, D)-intervals and the corresponding intervals in different segments have the same lengths. The density d of Π and D is dist({0}, {gcd(Π)}); this induces an equivalence relation on (Π, D)-intervals with d equivalence classes, which we call (Π,D)-types and denote by natural numbers between 0 and d-1. The (Π, D)-type k consists of all (Π, D)- intervals ϱ such that dist({0}, ϱ) - k is a multiple of d.

3 Core Fragments

In this section, we study the data complexity of reasoning in the core DatalogMTL fragments. We first show that consistency checking in DatalogMTL core is PSPACE-hard, which matches the known PSPACE upper bound for the full DatalogMTL language [Wał˛ega et al., 2019b]. In particular, each problem in PSPACE reduces to checking inconsistency of a dataset and a propositional DatalogMTL core program where S is the only temporal operator.

Theorem 2. Consistency checking in DatalogMTL core is PSPACE-hard in data complexity. The result holds already for propositional programs using only S as a temporal operator.

Proof sketch. Let P be a problem in PSPACE. Then, there exists a deterministic Turing machine M and a polynomial p such that, for every input word w, M decides P for w using at most p(|w|) cells. We construct in logarithmic space a dataset Dw encoding the initial configuration of M on w and a propositional DatalogMTL core program ΠM simulating the computations of M (on any input word) such that M accepts w if and only if ΠM and Dw are inconsistent.

Each configuration of M in the run on w is encoded within a unit interval (i.e., of length 1) divided into p(|w|) subintervals, each describing a cell of the tape. Each subinterval is split into two (left-open and right-closed) halves indicated by propositions P and Q, which respectively hold in the first and second half of each subinterval. In addition, we use the following propositions to encode a configuration: Pa-for each alphabet symbol a-which holds in the first half of a subinterval if the corresponding cell contains a; Qq-for each state q-which holds in the second half of a subinterval if the head is over the corresponding cell and M is in q; and QL and QR, which hold in the second half of a subinterval if the corresponding cell is, respectively, somewhere to the left and to the right of the head's position.

Program ΠM has two main blocks. The first block consists of the following rules, for each symbol a and state q:

The first two rules propagate P and Q. The remaining rules copy the description of a configuration into the next unit interval using auxiliary propositions (note that there is a gap between the unit intervals encoding consecutive configurations). The rules ensure that, if Pa and Qq hold in the two halves of a subinterval, then Paq and Qaq hold in the two halves of the corresponding subinterval in the next unit interval. Moreover, if Paq and Qaq hold in the same subinterval, then QLaq and QRaq hold in the second halves of the subintervals that are adjacent, respectively, to the left and to the right.

The second block of ΠM encodes the transition function of M (and does not use temporal operators). Each left-moving transition (q, a) ↦→ (q′ , a′ , L) is encoded by the rules

Right-moving transitions are encoded analogously; similar rules are also needed to propagate QL, QR, and Pa, for cells without the head. Finally, ΠM contains the rule ⊥ ←Qq for each accepting state q, which ensures inconsistency of ΠM and Dw when M accepts w.

The since operator S is strictly more expressive than the past diamond operator diamondminus. Hence, to regain tractability, we consider the DatalogMTLdiamondminuscore fragment and show that, in this case, consistency checking is TC0 -complete. This suggests suitability of DatalogMTLdiamondminuscore for data-intensive applications.

We start by defining a normal form. A DatalogMTLdiamondminuscore program is normal if each of its rules has one of the following forms, where α, α1, α2, and β are atoms, and ϱ is a non-empty bounded positive interval:

Each DatalogMTLdiamondminuscore program can be normalised so that the resulting program is a conservative extension of the original one: rules with nested operators are flattened by introducing fresh predicates, rules α ← α′ without metric operators are rewritten as α ← diamondminus{0}α′ , and rules P (τ ) ← diamondminus[t,∞)P ′ (τ ′ ) with unbounded intervals are replaced with rules Q(τ) ← diamondminus{t}P ′ (τ ′ ), Q(τ ) ← diamondminus[0,1]Q(τ ), and P (τ ) ← diamondminus{0}Q(τ ), for Q a fresh predicate of the same arity as P. Hence, in this section, we concentrate on normal DatalogMTLdiamondminuscore programs.

Next, we provide a characterisation of fact entailment for ground normal DatalogMTLdiamondminuscore programs in terms of existence of a specific length path in a graph defined below.

Definition 3. Let Π be a ground normal DatalogMTLdiamondminuscore program and let d ∈ N. Then, GdΠ is the directed edge-weighted multigraph with a vertex vα k for each (ground) atom α in Π and each k ∈ {0, . . . , d - 1}; and an edge (vα k , vβ ℓ ) of weight n whenever ℓ = (k + n) mod d and Π has a rule β ← diamondminusϱα such that n · (gcd(Π)/d) ∈ ϱ.

The graph GdΠ is defined so that, if d is the density of Π and a dataset D, then every derivation from Π and D (i.e., a sequence of punctual facts) corresponds to a path in GdΠ such that a 1-step derivation of β@{t2} from α@{t1} corresponds to an edge (vα k , vβ ℓ ) of weight dist(ϱ1, ϱ2), where ϱ1 ∋ t1 and ϱ2 ∋ t2 are (Π,D)-intervals of (Π,D)-types k and ℓ, respectively. Indeed, the following result holds.

Lemma 4. Let Π be a ground and positive normal DatalogMTLdiamondminuscore program, D a dataset, and d the density of Π and D. Then, for each fact β@ϱ with a (Π,D)-interval ϱ, the following are equivalent:

1. (Π,D) |= β@ϱ;
2. there exist a fact α@ϱ′ with ϱ′ a (Π,D)-interval such that D |= α@ϱ′ (or Π contains a rule α ← ⊤) and a path in GdΠ of weight dist(ϱ′ , ϱ) from vα k to vβ ℓ , where k and ℓ are the (Π, D)-types of ϱ′ and ϱ, respectively.

We next show that, given two vertices v and v′ in a directed multigraph with weights of edges being non-negative integers (e.g., GdΠ), we can finitely represent the weights of all paths from v to v′ . This lemma relies on the normal form for unary non-deterministic finite automata (NFAs) by Chrobak (1986) and will be essential to prove the TC0 upper bound.

Lemma 5. Let G be a directed edge-weighted multigraph with non-negative integer weights and let v, v′ be vertices in G. Then, it is possible to construct a finite set S of pairs of non-negative integers such that there is a path in G of weight n from v to v′ if and only if n = a + i · b for a pair (a, b) ∈ S and a non-negative integer i.

Proof sketch. First, we replace each edge in G of weight n > 1 with a chain of n edges of weight 1 by introducing fresh nodes. Then, we construct an NFA A over a unary alphabet {σ}, where states correspond to vertices: the initial state corresponds to v and the final state to v′ , and we have a σ-transition for each edge of weight 1 and an ϵ-transition for each edge of weight 0. Then, the weights of paths in G from v to v′ are exactly the lengths of words accepted by A. After eliminating ϵ-transitions, we obtain a unary NFA, which we then transform to Chrobak normal form [Chrobak, 1986, Lemma 4.3], where the transitions form a path from the initial state followed by a single nondeterministic choice between several (disjoint) cycles. For every accepting state q in the resulting automaton A′ , there exist a, b ∈ N such that there is an accepting run of A′ on σn ending at q if and only if there is a number i with n = a+ i · b (where a and b are the lengths of the simple paths from the initial state to q and of the cycle through q, respectively).

Lemmas 4 and 5 suggest a TC0 algorithm for checking whether a fixed ground positive normal DatalogMTLdiamondminuscore program Π and a dataset D entail β@{t}. For this, it suffices to check if there is α@ϱ in D such that (Π, {α@ϱ}) |= β@{t}. These checks can be done in parallel for each fact α@ϱ in D and hence we prove that each of them is feasible in TC0 . Assume that D′ = {α@ϱ}; we want to check whether (Π, D′ ) |= β@{t}. First, we compute the density d of Π and D′ , which is at most 4 since D′ contains only one interval. Then, we compute the (Π,D′ )-interval ϱ′ containing t, and the (Π,D′ )-type ℓ of ϱ′ . We also compute the left-most, ϱL, and the right-most, ϱR, (Π,D′ )-intervals contained in ϱ, as well as the set K of (Π,D′ )-types of (Π,D′ )-intervals contained in ϱ. All these computations are feasible in TC0 . Now, by Lemma 4, it suffices to check whether there is a path of weight n from vα k to vβ ℓ in GdΠ such that dist(ϱR, ϱ′ ) ≤ n ≤ dist(ϱL, ϱ′ ) and k ∈ K (if Π contains rules of the form α′ ← ⊤, some additional but easy to handle checks are required), which by Lemma 5 can also be checked in TC0 .

To check consistency of a ground normal DatalogMTLdiamondminuscore program Π and a dataset D, we need to consider rules of the from ⊥ ← α1 ∧ α2, where α1 and α2 are ground atoms. In particular, inconsistency arises whenever there is a time point where both α1 and α2 hold together in the least model of D and the positive subset of Π. This leads to technical difficulties since there is an unbounded number of candidate time points. The following theorem shows that these difficulties can be overcome, and consistency checking is TC0 -complete, where the upper bound holds also for non-ground programs.

Theorem 6. Consistency checking for DatalogMTLdiamondminuscore is TC0 -complete in data complexity. The lower bound holds for propositional DatalogMTL core without metric operators.

Proof sketch. For the lower bound, there is a simple AC0 reduction of the integer multiplication problem [Hesse, 2001]: a · b = c for positive integers a, b, and c (encoded in binary) if and only if the program {⊥ ← A ∧ B}, for propositions A and B, and the dataset {A@{a}, B@{ cb }} are inconsistent.

For the upper bound, we first consider a ground normal DatalogMTLdiamondminuscore program Π, with Π+ its positive subset. Since rules in Π with ⊥ do not contain temporal operators, the (Π, D)- and (Π+, D)-rulers and the corresponding densities coincide, as well as GdΠ = GdΠ+, for each d ∈ N.

By linearity of derivations and by Lemma 1, Π and D are inconsistent if and only if there is a rule ⊥← β1 ∧ β2 in Π and a subset D′ of D with at most two facts such that (Π+,D′ ) |= βi@ϱ for both i and some (Π+,D′ )-interval ϱ. Consider such D′ = {α1@ϱ1, α2@ϱ2}. Moreover, for both i, let ϱLi and ϱRi be the left- and the right-most (Π+,D′ )- intervals in ϱi, respectively, let Ki be the sets of the (Π+, D′ )- types of all (Π+,D′ )-intervals in ϱi, and let d be the density of Π+ and D′ . Then, assuming for simplicity that Π does not have rules α ← ⊤, we use Lemma 4 to reduce existence of ϱ as above to existence of two paths in GdΠ+: one from vα1 k1 to vβ1 ℓ with weight n1 and another from vα2 k2 to vβ2 ℓ with weight n2, where ki ∈ Ki for both i, ℓ is a (Π+,D′ )-type, and

We can check existence of such pairs of paths in parallel for each combination of k1, k2, and ℓ. By Lemma 5, we can represent the weights of all paths from vαi ki to vβi ℓ by a finite set Si of integer pairs. So to check (5) it suffices to verify if for some (a1, b1) ∈ S1 and (a2, b2) ∈ S2 there exist nonnegative integers i1, i2 with

which, by Bézout's identity, exist if and only if the following interval contains an integer:

The existence of such an integer can be verified in TC0 (for all (a1, b1) ∈ S1 and (a2, b2) ∈ S2 in parallel); hence, we can check the consistency in TC0 in the size of D.

Finally, let Π be a non-ground normal DatalogMTLdiamondminuscore program. Note that although the grounding ΠD of Π with constants from D can be computed in AC0 , the graph GdΠD depends not only on Π and d but also on D; this would prevent us from exploiting the TC0 procedure for ground programs. However, if D′ and D′′ are the same modulo renaming of constants not occurring in Π, then GkΠD′ and GkΠD′′ are isomorphic. Since we are interested in datasets with at most two facts and with arity of predicates fixed by Π, the number of nonisomorphic graphs for such datasets can be bounded without knowing D. Thus, we can compute the representatives of such non-isomorphic graphs in a data-independent way and reuse our TC0 procedure for ground programs.

Now, we show P-hardness for consistency checking in DatalogMTL⊟core , that holds even for propositional programs.

Theorem 7. Consistency checking in propositional DatalogMTL⊟core is P-hard in data complexity.

Proof sketch. The proof uses some ideas from the hardness proofs for pointwise semantics by Ryzhikov et al. (2019). We reduce the well-known P-complete path system accessibility problem (PSA) to inconsistency. An instance G of PSA is a tuple (V, E, S, vt), where V = {v1, . . . , vn} is a finite set of nodes, E is a ternary relation on V such that i < j < k for each (vi, vj, vk) ∈ E, S ⊆ V is a set of (source) nodes, and vt ∈ V is a (target) node. The answer to G is affirmative if vt is accessible, where a node vk is accessible if vk ∈ S or there are accessible nodes vi, vj such that (vi, vj , vk) ∈ E.

Let Π be the (fixed) program consisting of the following rules over propositions P , P ′ , P ′′ , and Q:

Consider now a PSA instance G as above, and let e1, . . . , em be an enumeration of E preserving the 'application order'- that is, such that for every edge eℓ with node vk as the third argument, vk is not the first or second argument of any eh with h < ℓ. Let DG be a dataset containing the following facts, for every ℓ such that 1 ≤ ℓ ≤ m+ 1:

and the following facts, for every eℓ = (vi, vj, vk):

For instance, DG, for G with V = {v1, v2, v3}, E = {(v1, v2, v3)}, S = {v1, v2}, and t = 3, is as follows.

It can then be easily checked that vt is accessible if and only if Π and DG are inconsistent.

4 Linear Fragments

Since linear fragments of DatalogMTL are extensions of corresponding core fragments, all lower bounds established in Section 4 for core fragments hold also for linear fragments. To obtain favourable computational properties, we focus on DatalogMTLdiamondminuslin and show NL-completeness of consistency checking in data complexity. The lower bound is inherited from plain linear Datalog, but we will prove it also for propositional DatalogMTLdiamondminuslin programs.

For the upper bound, we will concentrate on programs in a normal form, extending the one for the core case; a DatalogMTLdiamondminuslin program is normal if it consists only of rules of the following form, where α, α1, α2, and β are IDB atoms, φ is a possibly empty conjunction of EDB literals, and ϱ is a non-empty bounded positive interval:

Each DatalogMTLdiamondminuslin program can be normalised similarly as before-that is, by introducing rules with fresh predicates.

Naively, an inconsistency checking algorithm could guess a derivation of ⊥ from a normal program and an input dataset. This, however, does not lead to an NL algorithm since the length of a derivation and the representation of its elements (in particular numbers occurring in intervals) are unbounded. We next show how to overcome this problem.

Theorem 8. Consistency checking for DatalogMTLdiamondminuslin is NLcomplete in data complexity. The lower bound holds already for propositional DatalogMTLdiamondminuslin .

Proof sketch. The lower bound is by reduction of consistency checking for propositional normal DatalogMTLdiamondminuscore under pointwise semantics, where datasets consist of punctual facts and only the time points explicit in the dataset constitute the temporal universe of interpretations; this problem is NLcomplete in data complexity [Ryzhikov et al., 2019]. Given a propositional normal DatalogMTLdiamondminuscore program Π, we introduce a fresh IDB proposition QA for each literal A of the form diamondminusϱP in Π, and a fresh EDB proposition Q. We then construct a propositional DatalogMTLdiamondminuslin program Π′ by replacing each literal A as above in Π by QA and adding rules QA ← A ∧ Q. For each (punctual) dataset D, Π and D are consistent under pointwise semantics if and only if so are Π′ and D∪{Q@ϱ | ϱ occurs in D} under continuous semantics.

For the upper bound, consider a normal DatalogMTLdiamondminuslin program Π and a dataset D. By Lemma 1, Π and D are inconsistent if and only if there are a grounding ⊥ ← β1 ∧ β2 of a rule in Π and derivations of both facts βi@ϱ for some (Π,D)-interval ϱ. We can see each derivation as a sequence of facts over ruler intervals with IDB predicates. Since, such a sequence may be of exponential length, to achieve the bound, we will represent such derivations concisely as follows. Let Φ be the set of all groundings of the conjunctions φ of EDB literals in rules of Π such that all the atoms in the groundings are in D. For each φ ∈ Φ, we compute the maximal intervals in which D entails φ, which is feasible in TC0 . Such intervals allow us to compute in L the partitioning of the whole Q into sections-that is, the maximal intervals such that if D entails φ ∈ Φ in some time point in a section σ, then D entails φ in the whole σ. Let Φσ be the set of all φ ∈ Φ entailed in a section σ by D. We represent each derivation sequence as the subsequence of polynomial length containing only the first and the last facts in the derivation from every section. Each interval ϱ in the subsequence that may have endpoints with exponentially long binary representations is represented concisely as a pair of a pointer to the time point t from D

closest to ϱ and the number dist({t}, ϱ), which is polynomially representable in the size of D (special care is required when ϱ is in the first/last section). Hence, such representation of a derivation can be guessed fact by fact in NL.

Next, we show how to verify correctness of a guessed representation. The key step is to check that each fact αi+1@ϱi+1 in the subsequence can be derived from the preceding fact αi@ϱi. If ϱi and ϱi+1 are in different sections, then we check, in L, whether there is a 1-step derivation of αi+1@ϱi+1 from αi@ϱi. Otherwise-that is, when ϱi and ϱi+1 are in the same section σ-the derivation of αi+1@ϱi+1 from αi@ϱi can be of exponential length. To deal with this case, we construct in L a program Πσ by first deleting each rule in the grounding of Π mentioning some EDB conjunction not in Φσ, and then deleting all EDB literals from the remaining rules. Then Πσ is a ground normal DatalogMTLdiamondminuscore program, so we can show, as in the proof of Lemma 4, that the following are equivalent:

1. there is a derivation usingΠandD that startswithαi@ϱi and ends with αi+1@ϱi+1;
2. there is a path in GdΠσ (for d being the density of Π and D) of weight dist(ϱi, ϱi+1) from vαi ℓ to vαi+1 ℓ , where k and ℓ are, respectively, the (Π,D)-types of ϱi and ϱi+1.

The graph GdΠσ can be constructed in L, while checking existence of an appropriate path is feasible in NL, so existence of a derivation of αi+1@ϱi+1 from αi@ϱi is in NL.

5 Discussion and FutureWork

We have focused on fragments which mention only the past temporal operators diamondminus and ⊟, however, analogous results immediately follow for the future temporal operators diamondplus and ⊞.

Corollary 9. Consistency checking is TC0 -complete, P-hard, and NL-complete for DatalogMTLdiamondpluscore , DatalogMTL⊞core , and DatalogMTLdiamondpluslin , respectively, and the lower bounds hold already for the propositional fragments.

Low complexity fragments have also been identified for propositional DatalogMTL under the pointwise semantics [Kikot et al., 2018; Ryzhikov et al., 2019]. Results for pointwise and continuous semantics are, however, different: reasoning in DatalogMTL is CONP-complete under pointwise semantics, but PSPACE-complete for continuous semantics.

We see many possibilities for future work. First, it is unclear if the bound in Theorem 7 is tight, as well as whether the upper bound applies to DatalogMTL⊟lin . Second, it would be interesting to study also combined complexity. Third, we want to consider DatalogMTL over integer timelines, which may lead to lower complexity and which have been already considered for MTL [Gutiérrez-Basulto et al., 2016]. Finally, our complexity bounds do not directly provide practical reasoning algorithms, which we would like to construct.

Acknowledgments

This work was supported by the AIDA project (Alan Turing Institute), the SIRIUS Centre for Scalable Data Access (Research Council of Norway), Samsung Research UK, Siemens AG, and the EPSRC projects AnaLOG (EP/P025943/1), OASIS (EP/S032347/1) and UK FIRES (EP/S019111/1).