# materialisationbased_reasoning_in_datalogmtl_with_bounded_intervals__a7a960a0.pdf

Materialisation-Based Reasoning in Datalog MTL with Bounded Intervals

Przemysław A. Wał ega, Michał Zawidzki, Dingmin Wang, Bernardo Cuenca Grau

Department of Computer Science, University of Oxford, UK {przemyslaw.walega, michal.zawidzki, dingmin.wang, bernardo.cuenca.grau}@cs.ox.ac.uk

Datalog MTL is a powerful extension of Datalog with operators from metric temporal logic (MTL) which has received significant attention in recent years. In this paper, we investigate materialisation-based reasoning (a.k.a. forward chaining) in the context of Datalog MTL programs and datasets with bounded intervals, where partial representations of the canonical model are obtained through successive rounds of rule applications. Although materialisation does not naturally terminate in this setting, it is known that the structure of canonical models is ultimately periodic. Our first contribution in this paper is a detailed analysis of the periodic structure of canonical models; in particular, we formulate saturation conditions whose satisfaction by a partial materialisation implies the ability to recover the full canonical model via unfolding; this allows us to compute the actual periods describing the repeating parts of the canonical model as well as to establish concrete bounds on the number of rounds of rule applications required to achieve saturation. Based on these theoretical results, we propose a practical reasoning algorithm where saturation can be efficiently detected as materialisation progresses, and where the relevant periods used to evaluate entailment of queries via unfolding are efficiently computed. We have implemented our algorithm and our experiments suggest that our approach is both scalable and robust.

Introduction Datalog MTL is a powerful rule-based language for representing temporal knowledge that has found applications in ontology-based data access (Brandt et al. 2018; Kikot et al. 2018; Kalaycı et al. 2018; Koopmann 2019) and stream reasoning (Wał ega, Kaminski, and Cuenca Grau 2019). It extends Datalog (Ceri, Gottlob, and Tanca 1989) with operators from metric temporal logic (Koymans 1990) interpreted over the rational timeline. For example, the following Datalog MTL rule states that a person can travel if they had a negative COVID test at some point in the last 2 days (x[0,2]) and have been double-vaccinated for 14 days ( [0,14]):

Can Travel(x) x[0,2]Neg Test(x) [0,14]Dbl Vacc(x).

Reasoning in Datalog MTL is of high complexity, which makes its adoption in applications problematic. In particular, satisfiability and fact entailment are Exp Space-complete

Copyright 2023, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

(Brandt et al. 2018) and PSpace-complete in data complexity (Wał ega et al. 2019). Decision procedures are based on the observation that, although the timeline is densely ordered, the canonical model of a program and a dataset can be partitioned according to discrete sequences of intervals, inside which all time points satisfy the same facts. This enables the reduction (with exponential blow-up) of fact entailment in Datalog MTL to satisfiability of linear temporal logic (LTL) formulas (Brandt et al. 2018) or to non-emptiness of Büchi automata (Wał ega et al. 2019). As a result, canonical models have a periodic structure, with periods of bounded length (Artale et al. 2021a). Although these techniques are useful for providing complexity upper bounds for reasoning, they are based on exponential reductions and were not designed for efficient implementation. The most common technique of choice in scalable Datalog reasoners is materialisation (a.k.a. forward chaining), where facts entailed by a program and dataset are derived in successive rounds of rule applications until a fixpoint is reached (Bry et al. 2007; Motik et al. 2014; Carral et al. 2019; Bellomarini, Sallinger, and Gottlob 2018).1 Once the materialisation has been computed, queries can be answered directly and rules are not further considered. In contrast to Datalog where materialisation naturally terminates, in Datalog MTL a fixpoint may only be reachable after infinitely many rounds of rule applications. To circumvent this challenge, the Me Teo R reasoner (Wang et al. 2022) combines materialisation and automata-based reasoning, where automata construction ensures completeness where materialisation does not terminate; experiments, however, show a significant performance reduction in such cases (Wang et al. 2022). An alternative approach is to focus on Datalog MTL fragments for which materialisation is guaranteed to terminate (Wał ega, Zawidzki, and Cuenca Grau 2021); such fragments, however, impose significant restrictions effectively disallowing recursion through time . In this paper, we investigate the design of reasoning algorithms for Datalog MTL that rely solely on materialisation, dispense with automata construction altogether, and do not limit recursion. We focus on bounded Datalog MTL programs and datasets, where is not mentioned as an end-

1In this setting, both the reasoning process and its output are often referred to as materialisation.

The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)

point of any interval; this is a natural and expressive fragment, in which reasoning is as hard as in the unrestricted language (Wał ega, Zawidzki, and Cuenca Grau 2021). Our first contribution is a detailed analysis of the periodic structure of canonical models. We formulate saturation conditions that a partial materialisation needs to satisfy so that the canonical model can be recovered via unfolding; this allows us to compute the actual periods describing the repeating parts of the model based only on the form of the partial materialisation constructed so far, as well as to establish concrete bounds on the number of rounds of rule applications required to achieve saturation. This is a challenging problem since Datalog MTL rules may recursively propagate facts towards both future and past time points, and hence regularities observed in a partial materialisation may not correspond to the periodic structure of the full canonical model. Based on these theoretical results, we propose a practical reasoning algorithm where saturation can be efficiently detected as materialisation progresses, and where the relevant periods used to evaluate entailment queries via unfolding are efficiently computed. We have implemented our algorithm and evaluated its performance on a temporal extension of Lehigh University Benchmark (Wang et al. 2022) as well as using the i Temporal benchmark generator (Bellomarini, Nissl, and Sallinger 2022). Our results show that the overhead introduced by saturation checks during materialisation is negligible, saturation can be reached after a reasonable number of rounds of rule applications, and entailment checks performed after reaching saturation can be conducted very efficiently.

Preliminaries We recapitulate the syntax and semantics of Datalog MTL, focusing on the standard continuous semantics over the rational timeline (Brandt et al. 2018; Wał ega et al. 2019).

Time and Intervals. The (rational) timeline is the ordered set Q of rational numbers; each element of the timeline is called a time point. We consider binary representations of integers, and represent each rational number as a fraction with an integer numerator and a positive integer denominator. An interval ϱ is a non-empty subset of Q satisfying two properties: (i) for all t1, t2, t3 Q with t1 < t2 < t3 and t1, t3 ϱ, it is the case that t2 ϱ, and (ii) both the greatest lower bound ϱ and the least upper bound ϱ+ of ϱ are in Q { , }. The bounds ϱ and ϱ+ are the left and right endpoints of ϱ, respectively, and |ϱ| = ϱ+ ϱ is the length of ϱ. Interval ϱ is punctual if it has a single time point, it is positive if it does not contain negative time points, and bounded if both of its endpoints are rationals numbers. For intervals ϱ and ϱ we define the operations ϱ + ϱ = {t + t | t ϱ and t ϱ } and ϱ = { t | t ϱ}. We use the standard representation ϱ , ϱ+ for an interval ϱ, where the left bracket is either [ or (, the right bracket is either ] or ), and ϱ and ϱ+ are representations of the left and right endpoints of ϱ, respectively. Brackets [ and ] indicate that the corresponding endpoints are included in the interval, whereas ( and ) indicate that they are not included. We often abbreviate a punctual

interval [t, t] as t. Since different intervals cannot have the same representation, we will often abuse notation and identify an interval representation with the interval it represents. Syntax. Assume a function-free first-order signature. A relational atom is a first-order atom of the form P(s), with P a predicate and s a tuple of terms whose length matches the arity of P. A metric atom is an expression given by the following grammar, where P(s) is a relational atom and ϱ a positive interval:

M ::= | | P(s) | xϱM | |ϱM | ϱ M | ϱM | MSϱM | MUϱM.

A rule is an expression of the form

M M1 Mn, for n 1, (1)

where each Mi is a metric atom, whereas M is a metric atom not mentioning x, |, S, and U, and hence generated by the following grammar:2

M ::= | P(s) | ϱM | ϱM .

The conjunction M1 Mn in Expression (1) is the rule s body; each Mi is a body atom and M is the rule s head. A rule is safe if all its variables occur in the body. A program is a finite set of safe rules. A program is bounded if all intervals it mentions are bounded. An expression (metric atom, rule, or program) is ground if it has no variables. The grounding ground(Π) of Π is the set of all ground rules obtained by assigning constants to variables in Π. A metric fact over an interval ϱ is an expression M@ϱ, with M a ground metric atom; it is relational if so is M and bounded if so is ϱ. A dataset is a finite set of relational facts; it is bounded if so is each of its facts. For a dataset D we let t D and t+ D be, respectively, the minimal and maximal rational numbers mentioned as endpoints of intervals in D (or 0 if D mentions no numbers).

Semantics. An interpretation I specifies, for each ground relational atom P(s) and each time point t, whether P(s) is satisfied at t, in which case we write I, t |= P(s). This notion extends to other ground metric atoms as specified in Table 1. Interpretation I satisfies a metric fact M@ϱ, written I |= M@ϱ, if I, t |= M for all t ϱ. Interpretation I satisfies a ground rule r if, for any time point t, whenever I satisfies each body atom of r at t, then I also satisfies the head of r at t. Interpretation I satisfies a (possibly non-ground) rule r if I satisfies each rule in ground({r}); it satisfies a program Π if I satisfies each rule in Π; moreover, I satisfies Π in an interval ϱ if, for each r ground(Π) and each t ϱ, whenever I satisfies each body atom of r at t, then I satisfies the head of r at t. Interpretation I is a model of a program Π if it satisfies Π, and it is a model of a dataset D if it satisfies each fact in D. A program Π and a dataset D entail a metric fact M@ϱ, written as (Π, D) |= M@ϱ, if each model of both Π and D is also a model of M@ϱ. We may write D |= M@ϱ instead of ( , D) |= M@ϱ.

2For convenience, we additionally disallow in rule heads, which ensures consistency and allows us to focus on fact entailment and the computation of canonical interpretations.

I, t |= for each t I, t |= for no t

I, t |= xϱM iff I, t |= M for some t with t t ϱ

I, t |= |ϱM iff I, t |= M for some t with t t ϱ

I, t |= ϱM iff I, t |= M for all t with t t ϱ

I, t |= ϱM iff I, t |= M for all t with t t ϱ

I, t |= M1SϱM2 iff I, t |= M2 for some t with t t ϱ

and I, t |= M1 for all t (t , t)

I, t |= M1UϱM2 iff I, t |= M2 for some t with t t ϱ

and I, t |= M1 for all t (t, t )

Table 1: Semantics of ground metric atoms

An interpretation I contains an interpretation I , written I I, if I , t |= P(s) implies I, t |= P(s), for each ground relational atom P(s) and time point t. Then, I is the least interpretation in a set X of interpretations if I I for every I X. Each dataset D admits the least interpretation ID among all models of D and we say that a dataset D represents an interpretation I if I = ID.

Canonical Model We let the immediate consequence operator TΠ for a program Π be the function mapping an interpretation I to the least interpretation TΠ(I) containing I and satisfying the following property for each r ground(Π): whenever I satisfies each body atom of r at a time point t, then TΠ(I) satisfies the head of r at t. Successive applications of TΠ to ID define a transfinite sequence of interpretations T α Π(ID) for ordinals α as follows: (i) T 0 Π(ID) = ID, (ii) T α+1 Π (ID) = TΠ(T α Π(ID)) for α an ordinal, and (iii) T α Π(ID) = S β<α T β Π(ID) for α a limit ordinal. The canonical model CΠ,D of Π and D is the interpretation T ω1 Π (ID), where ω1 is the first uncountable ordinal. Since we do not allow in rule heads, CΠ,D is always a model of Π and D, and it is the least such model (Brandt et al. 2017). Interpretation CΠ,D can be divided into regularly distributed (Π, D)-intervals whose time points satisfy the same ground atoms (Wał ega et al. 2019). In particular, the (Π, D)-ruler is the set of time points of the form t + i div(Π), for t Q mentioned in D and i Z, and where div(Π) = 1

k, with k being the product of all denominators in the rational endpoints of the intervals mentioned in Π (for definiteness, if Π has no intervals with rational endpoints, we let k = 1 and hence div(Π) = 1). A (Π, D)-interval is either a punctual interval over a time point on the (Π, D)-ruler or an interval (t1, t2) with t1 and t2 consecutive time points on the (Π, D)-ruler. We say than an interpretation I is a (Π, D)-interpretation if, for every relational fact M@t, it holds that I |= M@t implies I |= M@ϱ, where ϱ is the (Π, D)-interval containing t. It turns out that CΠ,D as well as T α Π(ID), for any ordinal α, is a (Π, D)- interpretation (Wał ega et al. 2019).

Reasoning. We consider fact entailment, that is, checking if a relational fact is entailed by a program and a dataset. This problem is PSpace-complete in data complexity, that is, when the size of a program is considered as fixed (Wał ega et al. 2019), and Exp Space-complete in combined complexity, where complexity is measured also with respect to the program (Brandt et al. 2017). The same complexity bounds hold already in the case of bounded programs and datasets (Wał ega, Zawidzki, and Cuenca Grau 2021).

Periodic Structure of the Canonical Model In this section, we establish the theoretical basis for our novel reasoning approach. Given a bounded program Π and a dataset D, we present saturation conditions stating the properties that a partial materialisation T k Π(ID) needs to satisfy so that the full canonical model can be recovered. We call an interpretation satisfying these conditions saturated and show how to compute relevant periods and exploit them to unfold the interpretation into the canonical model of Π and D. This allows us to check entailment of any fact. For convenience of presentation, we fix for the remainder of this section an arbitrary bounded program Π, bounded dataset D, and natural number k. Moreover, for an interpretation I and an interval ϱ, we let the projection I |ϱ of I over ϱ be the interpretation that coincides with I on ϱ and makes all relational atoms false outside ϱ. We say that an interpretation I is a shift of I if there is a rational number q such that I |= M@ϱ if and only if I |= M@(ϱ + q), for each (relational) fact M@ϱ. Furthermore, for a rule r, we define its depth, written as depth(r), as the sum of right endpoints of all intervals occurring in the operators of r (or 0 if r mentions no intervals), and we let depth(Π) be the maximum depth of its rules. As shown in the following proposition, the depth of a bounded rule determines the time points that can be affected by an application of this rule. Proposition 1. For every interpretation I, time point t, and bounded rule r, it holds that I satisfies r at t if and only if so does I |[t depth(r),t+depth(r)].

Proof. By definition, I satisfies r at t if and only if the body of r does not hold at t or the head of r holds at t. By the definition of depth(r), all the facts corresponding to the satisfaction of the body and the head of r at t are over intervals contained in [t depth(r), t + depth(r)]. This directly implies the claim in the proposition.

Having introduced these basic concepts, we are now ready to define our notion of a saturated interpretation. Definition 2. Interpretation T k Π(ID) is saturated if there exist closed intervals ϱ1, ϱ2, ϱ3, and ϱ4 of length 2depth(Π), whose endpoints are located on the (Π, D)-ruler and satisfy ϱ+ 1 < ϱ+ 2 < t D and t+ D < ϱ 3 < ϱ 4 , and such that the following properties hold: T k Π(ID) satisfies Π in [ϱ 1 , ϱ+ 4 ]; T k Π(ID) |ϱ1 and T k Π(ID) |ϱ3 are shifts of T k Π(ID) |ϱ2 and T k Π(ID) |ϱ4, respectively.

Any pair of intervals [ϱ 1 , ϱ 2 ) and (ϱ+ 3 , ϱ+ 4 ], for ϱ1, ϱ2, ϱ3, ϱ4 as above, will be referred to as periods of T k Π(ID).

Intuitively, a saturated interpretation contains a central fragment [ϱ 1 , ϱ+ 4 ] which satisfies D and such that a single application of TΠ does not derive any new facts within this fragment (i.e., the interpretation satisfies Π within [ϱ 1 , ϱ+ 4 ]). In the left segment of this central fragment there are two intervals ϱ1 and ϱ2 each of length 2depth(Π) in which T k Π(ID) satisfies the same relational facts modulo a shift. Analogously, in the right segment of the central fragment there are intervals ϱ3 and ϱ4 also with repeating contents. It is worth emphasising that in the definition of a saturated interpretation (first item), we consider only a single materialisation step, which can be effectively checked. As we will show in Theorem 5, rather surprisingly, this condition is enough to guarantee that a saturated interpretation can be unfolded into the canonical model. We next define the unfolding of a saturated interpretation relatively to a pair (ϱleft, ϱright) of its periods. Although there can be many such pairs of intervals, the key properties of the unfolding are independent of the choice of periods.

Definition 3. The (ϱleft, ϱright)-unfolding, of a saturated interpretation T k Π(ID) with periods (ϱleft, ϱright), is the interpretation C such that:

C |[ϱ left,ϱ+ right]= T k Π(ID) |[ϱ left,ϱ+ right],

C |ϱleft n |ϱleft| is a shift of T k Π(ID) |ϱleft, for any n N, C |ϱright+n |ϱright| is a shift of T k Π(ID) |ϱright, for any n N.

We observe that the unfolding is unique and can be obtained from the least interpretation coinciding with T k Π(ID) on [ϱ left, ϱ+ right] by subsequently copying the fragment of this interpretation that spans ϱleft infinitely many times to the left and the fragment of this interpretation that spans ϱright infinitely many times towards the right on the timeline. In Theorem 5 we will show that the unfolding of a saturated interpretation coincides with the canonical model. The proof of this theorem exploits a generalisation of a technical lemma from the literature (Wał ega, Zawidzki, and Cuenca Grau 2021, Lemma 11), which we provide next.

Lemma 4. Let ϱ be a closed interval of length depth(Π) and D a dataset representing CΠ,D |ϱ. Then both of the following hold:

1. If ϱ+ t+ D, then CΠ,D |(ϱ+, )= CΠ,D |(ϱ+, ). 2. If ϱ t D, then CΠ,D |( ,ϱ )= CΠ,D |( ,ϱ ).

Proof sketch. Both items have similar proofs, so we focus on the first one. The inclusion CΠ,D |(ϱ+, ) CΠ,D |(ϱ+, ) follows from the fact that CΠ,D |= D , so CΠ,D CΠ,D. To show that CΠ,D |(ϱ+, ) CΠ,D |(ϱ+, ) it suffices to prove inductively that, for every ordinal α and relational fact M@t with t > ϱ+, if T α Π(ID) |= M@t, then T α Π(ID ) |= M@t. We conduct the induction similarly to the proof due to Wał ega, Zawidzki, and Cuenca Grau (2021, Lemma 11), but using depth(Π) in the inductive step.

Theorem 5. The (ϱleft, ϱright)-unfolding C of a saturated interpretation T k Π(ID) with periods (ϱleft, ϱright) coincides with the canonical model CΠ,D.

Proof sketch. We first show that CΠ,D C. Since CΠ,D is the least model of Π and D, it suffices to show that C is a model of Π and D. As [t D, t+ D] [ϱ left, ϱ+ right], we obtain that the projection of T k Π(ID) over [ϱ left, ϱ+ right] is a model of D. However, by Definition 3, C and T k Π(ID) coincide on [ϱ left, ϱ+ right], so C is also a model of D. To show that C satisfies Π in ϱ = [ϱ left + depth(Π), ϱ+ right depth(Π)], it suffices, by Proposition 1, to show that the projection of C over [ϱ left, ϱ+ right] satisfies Π in ϱ; this holds since C and T k Π(ID) coincide on [ϱ left, ϱ+ right] and T k Π(ID) satisfies Π in [ϱ left, ϱ+ right], as it is saturated. It remains to argue that C satisfies Π at each t outside ϱ. Assume that t < ϱ , so t < ϱ left + depth(Π). Then, there exists a unique pair of n N and t [ϱ left + depth(Π), ϱ+ left + depth(Π)) such that t + n |ϱleft| = t . This, by the definition of C, implies that C |[t depth(Π),t+depth(Π)] is a shift of C |[t depth(Π),t +depth(Π)]. Thus, by Proposition 1, C satisfies Π at t if and only if C satisfies Π at t . The latter holds since t ϱ and, as we already showed, C satisfies Π in ϱ. The proof for t > ϱ right depth(Π) is similar, so CΠ,D C. We show that C CΠ,D. The projection of C over [ϱ left, ϱ+ right] is in CΠ,D since C and T k Π(ID) coincide on this interval and T k Π(ID) CΠ,D. To show that the projection of C over ( , ϱ left] is in CΠ,D, we argue that C |[ti,ϱ+ right] CΠ,D |[ti,ϱ+ right] by induction on

consecutive timepoints ti on the (Π, D)-ruler, with t0 = ϱ left. The base holds since C and T k Π(ID) coincide on [ϱ left, ϱ+ right]. For the inductive step, let ϱA = [ti, ti 1), ϱB = [ti 1, ti 1 + depth(Π)], ϱ A = ϱA + |ϱleft|, and ϱ B = ϱB + |ϱleft|. Hence, it suffices to show that C |ϱA CΠ,D |ϱA. We note that C |ϱB is a shift of C |ϱ B by the construction of C and the fact that (ϱ B)+ ϱ+ left + depth(Π). Thus, by the inductive assumption and CΠ,D C, we obtain that CΠ,D |ϱB is a shift of CΠ,D |ϱ B. By the construction of C we know that C |ϱA is a shift of C |ϱ A and since the lengths of ϱB and ϱ B equal depth(Π), we can use Lemma 4 to show that CΠ,D |ϱA is a shift of CΠ,D |ϱ A. By the inductive assumption, C |ϱA CΠ,D |ϱA and so, C |ϱA CΠ,D |ϱA. The proof of the inclusion C |[ϱ+ right, ) CΠ,D |[ϱ+ right, ) is symmetric; thus, C CΠ,D.

Theorem 5 states that the unfolding of a saturated interpretation around any pair of its periods coincides with the canonical model. Thus, we can refer to an unfolding of a saturated interpretation without explicitly referring to its periods. We conclude this section by establishing a bound kmax, depending on Π and D, which ensures that T k Π(ID) is saturated for some k kmax. Intuitively, kmax is the number of facts that we can construct by combining atoms relevant to Π and D with (Π, D)-intervals contained in a sufficiently large interval ϱ. The interval ϱ is chosen so that [t D, t+ D] ϱ, and such that its fragments [ϱ , t D) and (t+ D, ϱ+] to the left

and right of D, respectively, contain so many intervals of length 2depth(Π) with endpoints on the (Π, D)-ruler, that their contents need to repeat. These repetitions guarantee the existence of intervals ϱ1, . . . , ϱ4 from Definition 2.

Theorem 6. There exists k kmax such that T k Π(ID) is saturated, where the bound kmax is defined as follows. Let A be the number of ground relational atoms in the grounding of Π with constants from Π and D, let B be the number of (Π, D)-intervals within [t D, t D + 2depth(Π)], and let ϱ = [t w 2depth(Π), tw + 2depth(Π)], where < t 2 < t 1 < t D and t+ D < t1 < t2 < . . . are sequences of consecutive time points on the (Π, D)-ruler, whil w = 1 + B (2A)B. Then kmax is the product of A and the number of (Π, D)-intervals contained in ϱ.

Proof sketch. The canonical model CΠ,D satisfies at most kmax relational facts over (Π, D)-intervals contained in ϱ. Since each application of TΠ (before reaching a fixpoint) introduces at least one new relational fact over a (Π, D)-interval, there needs to exist k kmax such that T k Π(ID) |ϱ= T k+1 Π (ID) |ϱ. We argue that T k Π(ID) is saturated for such k by showing that ϱ contains intervals ϱ1, . . . , ϱ4 satisfying the conditions from Definition 2. To show the existence of ϱ1 and ϱ2, we observe that ϱ contains w = 1 + B (2A)B intervals of length 2depth(Π) whose endpoints are located on the (Π, D)-ruler to the left of t D. We can show that there must exist amongst them two distinct intervals ϱ1 and ϱ2 such that T k Π(ID) |ϱ1 is a shift of T k Π(ID) |ϱ2. Indeed, each interval of the form [t, t + 2depth(Π)], for t on the (Π, D)-ruler, contains the same number of (Π, D)-intervals as [t D, t D + 2depth(Π)] does, which equals B. In each of these (Π, D)-intervals there can hold at most 2A combinations of relational atoms, which gives rise to (2A)B different contents of an interval of the form [t, t + 2depth(Π)]. Additionally, these intervals can differ depending on the location of (Π, D)-intervals they contain. By the definition of the (Π, D)-ruler, there are at most B different layouts of (Π, D)-intervals contained in an interval of the form [t, t + 2depth(Π)]. Hence, in total, there are at most B (2A)B intervals of the form [t, t + 2depth(Π)] with different contents. Thus, in a set of w = 1 + B (2A)B such intervals, there needs to be a pair of distinct intervals ϱ1 and ϱ2 such that T k Π(ID) |ϱ1 is a shift of T k Π(ID) |ϱ2. Analogously, we can show the existence of required ϱ3 and ϱ4 to the right of t+ D, so the second item from Definition 2 holds. Moreover, since [ϱ 1 , ϱ+ 4 ] ϱ and T k Π(ID) |ϱ= T k+1 Π (ID) |ϱ, we obtain that T k Π(ID) satisfies Π in [ϱ 1 , ϱ+ 4 ]. Thus, the first item from Definition 2 holds as well, and so, T k Π(ID) is saturated.

The bound kmax from Theorem 6 is doubly exponential in the size of Π and D, but only exponential in the size of D. Essentially, this bound shows us how much time is needed to perform reasoning, which is consistent with the computational complexity of reasoning in Datalog MTL, namely Exp Space in combined complexity (Brandt et al. 2017) and PSpace in data complexity (Wał ega et al. 2019).

Algorithm 1: Reasoning via Periods Detection

Input: a bounded program Π, a bounded dataset D, and a relational fact M@ϱ Output: a Boolean value True or False

1 Dnow := D;

3 if Dnow |= M@ϱ then return True;

4 (ϱleft, ϱright) := Periods(Π, D, Dnow);

5 if ϱleft = and ϱright = then

6 if Entails(Π, D, Dnow, ϱleft, ϱright, M@ϱ) then return True;

7 else return False;

8 Dnow := Apply Rules(Π, Dnow);

The results from the previous section suggest the reasoning procedure in Algorithm 1, which checks if a bounded program Π and a dataset D entail a relational fact M@ϱ. The algorithm successively applies the rules of Π to the dataset (Line 8) until one of two stopping conditions hold. The first condition (Line 3) detects if the materialisation Dnow constructed thus far entails the input fact M@ϱ, in which case the algorithm reports that the input fact is entailed. The second condition checks if Dnow is saturated (i.e., represents a saturated interpretation). To this end, the algorithm computes in Line 4 two non-empty intervals which are periods of Dnow (if Dnow is saturated), or introduces two empty intervals (if Dnow is not saturated). If Dnow is saturated, the algorithm exploits Dnow and its periods to check whether M@ϱ is entailed (Lines 6 7). We next describe in detail the computations of the algorithm and establish their correctness. In what follows, we fix an arbitrary input Π, D, and M@ϱ to Algorithm 1 and assume that the notions of a saturated interpretation and its periods are relative to Π and D. We also let the projection D |ϱ of a dataset D over an interval ϱ be the dataset obtained by intersecting all intervals in facts from D with ϱ .

Rule Application In each iteration of the loop, Algorithm 1 applies the procedure Apply Rules (Line 8), which implements a single round of rule applications to Dnow, and thus, mimics an application of the immediate consequence operator TΠ to IDnow. Hence, in the beginning of a (k + 1)st iteration of the loop, the dataset Dnow in Algorithm 1 represents T k Π(ID). This is a basic component of materialisation in Datalog MTL, already implemented in the literature (Wang et al. 2022, Algorithm 1).

First Stopping Condition In Line 3, Algorithm 1 checks whether the materialisation Dnow constructed so far entails the input fact M@ϱ. Since facts in Dnow are stored in a coalesced form, to check if Dnow |= M@ϱ, it suffices to scan Dnow and verify whether there is M@ϱ Dnowwith ϱ ϱ .

Second Stopping Condition Algorithm 1 calls the Periods procedure in Line 4 to check, in an iteration k + 1 of the loop, if T k Π(ID) is saturated. The procedure searches

for intervals ϱ1, . . . , ϱ4 satisfying the conditions in Definition 2 and returns the periods of the interpretation T k Π(ID) if it is saturated or a pair of empty intervals otherwise. To this end, the procedure performs one round of rule applications to Dnow, computing Dnext. Then, it computes an interval ϱmax as either the empty interval (if Dnow and Dnext do not coincide on [t D, t+ D]), or otherwise as the maximal interval containing [t D, t+ D] and such that Dnow and Dnext coincide on ϱmax. Interval ϱmax is next used to search for ϱ1 and ϱ2, namely all pairs of intervals contained in ϱmax, located to the left of t D, with endpoints on the (Π, D)-ruler, and of lengths 2depth(Π), are compared. The first pair of such intervals with the same contents in Dnow is set as ϱ1 and ϱ2; otherwise ϱ1 and ϱ2 are empty intervals. In a similar way intervals ϱ3 and ϱ4 are computed. Finally, the procedure outputs a pair of intervals ([ϱ 1 , ϱ 2 ), (ϱ+ 3 , ϱ+ 4 ]), or ( , ) if any of the intervals ϱ1, . . . , ϱ4 is empty.

Fact Entailment Checking after Saturation After constructing a saturated dataset Dnow (representing T k Π(ID), for some k N) with periods (ϱleft, ϱright), Algorithm 1 calls the procedure Entails (Line 6) to check whether the input fact M@ϱ holds in the unfolding of T k Π(ID). This can be easily checked by exploiting Definition 3 of unfolding.

From our theoretical results in the previous section it follows that the algorithm is sound and complete:

Theorem 7. Algorithm 1 outputs True if (Π, D) |= M@ϱ, otherwise it outputs False. Moreover, the algorithm terminates after at most kmax + 1 (c.f. Theorem 6) iterations of its main loop.

We conclude this section with an example illustrating the execution of Algorithm 1.

Example 8. Consider Π = { [0,1]P P, [1,1]Q Q}, D = {P@0, Q@1.5}, and a query fact M@t = Q@ 4.5. After 5 iterations of the loop in Algorithm 1, the dataset Dnow consists of facts P@[0, 5] and Q@t, for all t { 3.5, 2.5, 1.5, 0.5, 0.5, 1.5}. The stopping condition from Line 3 does not hold, but the condition in Line 5 does. Indeed, Dnow is saturated and its periods computed in Line 4 are ϱleft = [ 3.5, 2.5) and ϱright = (4.0, 4.5]. The unfolding of Dnow is the canonical model of Π and D depicted in Figure 1. Then, in Line 6, Algorithm 1 can exploit Dnow, ϱleft, and ϱright to detect entailment of any fact. In particular, the input fact Q@ 4.5 is entailed, and so, Algorithm 1 returns True in Line 6.

5 4 3 2 1 0 1 2 3 4 5 6

Q Q Q Q Q Q Q

ϱright =(4.0, 4.5] ϱleft =[ 3.5, 2.5) t Dex t+ Dex

Saturated dataset

Figure 1: Canonical model CΠ,D of Π and D

Experimental Evaluation

We have implemented Algorithm 1 and conducted two experiments.3 The first experiment compares our implementation with Me Teo R (Wang et al. 2022), which we take as the baseline; we did not consider other reasoners, such as Ontop (Kalaycı et al. 2018), as they support only non-recursive programs, where canonical interpretations are always finite. The second experiment tests the scalability of our implementation on datasets of increasing size. All experiments were conducted on a Dell Power Edge R730 server with 512 GB of RAM and two Intel Xeon E5-2640 2.6 GHz processors running Fedora 33, kernel version 5.8.17. We used as benchmarks a temporal extension of the Lehigh University Benchmark (LUBM) (Wang et al. 2022) and the i Temporal bechmark generator (Bellomarini, Nissl, and Sallinger 2022). The LUBM extension provides a fixed Datalog MTL program which extends the 56 Datalog rules in LUBM with 29 temporal rules involving recursion and mentioning all metric operators in Datalog MTL. We used the i Temporal benchmark generator to construct another recursive Datalog MTL program with 19 rules. Both of the benchmarks allow for the generation of datasets of increasing size.

Comparison with the Baseline. We compared our implementation with Me Teo R, which combines materialisation with automata-based reasoning techniques. For the LUBM benchmark, Figure 2 (left), we considered a dataset D with 5 million facts and query facts F@t, where F is a fixed relational atom (about the predicate Full Professor) and t { 500, 400, . . . , 500}. Reasoning with D and the fragment Π of the benchmark s program that is relevant for F is non-trivial and materialisation does not terminate for them. Facts F@t with t > 0 are entailed by Π and D, so such facts are decided by Me Teo R using materialisation only. Thus, the larger t, the larger the number of materialisation steps the baseline performs; as shown in Figure 2, materialisation times increase linearly with t. In our new approach, we observe a similar linear growth up until t = 300, where saturation is achieved. This indicates that saturation checks during materialisation come with negligible overhead. Once saturation is reached, our approach does not require further materialisation steps and fact entailment can be decided based on the saturated dataset. Thus, fact entailment running times are roughly identical for all facts with t 300, while for Me Teo R they continue to grow with t. Facts F@t, with t < 0 are not entailed, hence Me Teo R must resort to automata-based techniques. Due to the optimisations implemented in Me Teo R, automata-based reasoning works well for facts with time points that lie close to the dataset, but performance degrades as t becomes located further away. In contrast, our approach proceeds as in the previous case; it will materialise in linear running time until a saturated dataset is obtained, at which point running times stabilise and become independent of t. In the case of the i Temporal benchmark, we considered a dataset with 1000 facts and facts G@t with a specific atom

3Our implementation can be accessed through the following link: https://github.com/wdimmy/Datalog MTLPeriodicity.

F@-500 F@0 F@500 0

Fact whose entailment is checked

Running time (in seconds)

Baseline Our approach

G@-100 G@0 G@100 0

Figure 2: Comparison with the baseline on the LUBM (on the left) and i Temporal (on the right) benchmarks

G and t { 100, 80, . . . , 100}; we observed the same type of behaviour as for LUBM (see Figure 2, right).

Scalability in Data Size. In the second experiment, we analysed how saturation times increase with the size of the input dataset. We considered the same programs as in the first experiment, together with sequences of datasets of increasing size. For the LUBM benchmark, we generated two sequences, each containing 6 datasets. In the first sequence all the intervals of temporal facts are contained within the range [0, 50] and we increase the size of datasets by introducing atoms with new constants. In the second sequence, the number of constants is the same but the number of facts increases; facts occupy increasing ranges of time, namely, [0, 5 10i], for i {1, . . . , 6}. In both sequences, the datasets have 103, 104, 105, 106, 107, and 108 facts, respectively. As depicted in Figure 3 (left), in both cases running times grow proportionally with data size; this suggests that our approach is scalable with respect to both the number of constants and the temporal range of the dataset. We observe that the running times for the second sequence of facts are around twice smaller than for the first sequence (except the first dataset which is the same in both sequences), so increasing the number of constants seems to have a larger impact on our approach than increasing the temporal domain. We performed a similar experiment for the i Temporal benchmark (see Figure 3, right), which confirmed our observations from the LUBM experiment.

103 104 105 106 107 108 0

102 103 104 105

Size of a dataset

Running time (in seconds)

Increasing constants Increasing time range

101 102 103 104 105 0

Figure 3: Scalability of our approach tested on the LUBM (on the left) and i Temporal (on the right) benchmarks

Related Work

The complexity of reasoning in Datalog MTL and its fragments has been studied in recent years (Brandt et al. 2018; Wał ega et al. 2019, 2020b), as well as their alternative semantics with favourable computational properties have been proposed (Wał ega et al. 2020a; Ryzhikov, Wał ega, and Zakharyaschev 2019). Datalog MTL has also been extended with stratified negation (Tena Cucala et al. 2021) and with unrestricted negation under stable model semantics (Wał ega et al. 2021), which is related to recent research on metric temporal ASP (Cabalar et al. 2020). Several techniques have been proposed for reasoning in Datalog MTL. Brzoska (1998) introduced proof systems based on solving linear inequalities, Me Teo R (Wang et al. 2022) is based on an algorithm combining materialisation and automata-based techniques, whereas Ontop implements a reasoning algorithm based on query rewriting that is applicable to non-recursive programs (Kalaycı et al. 2018). The use of blocking conditions to stop further application of inference rules while retaining completeness is routinely exploited in automated reasoning, especially in the context of modal (Bolander and Blackburn 2007; Schmidt and Waldmann 2015; Areces and Orbe 2015), temporal (Reynolds 2016; Chafik et al. 2021), and description logics (Horrocks and Sattler 1999; Schmidt and Tishkovsky 2011; Glimm, Horrocks, and Motik 2010). Periodicity of temporal models has been extensively investigated for LTL (Manna and Wolper 1982; Sistla and Clarke 1985) and its fragments (Artale et al. 2013), the temporal logic TPTL for the specification of real-time systems (Alur and Henzinger 1994), the temporalised description logic EL (Gutiérrez-Basulto, Jung, and Kontchakov 2016), and the metric temporal extension LTLbin ALC of the description logic ALC (Baader et al. 2020). It has been shown that canonical models in LTL-based rule-languages are periodic and the lengths of offsets and periods in such interpretations are bounded by an exponential function of the number of predicates involved (Artale et al. 2021b). In contrast to our approach, however, no effective method of computing such periods was established. There have been various other proposals for extending Datalog with temporal constructs (Baudinet, Chomicki, and Wolper 1993; Beck et al. 2015) such as Datalog1S and Datalogn S (Chomicki and Imieli nski 1988; Chomicki 1990, 1995); in particular problems corresponding to finite materialisability have been considered in this setting (Chomicki and Imieli nski 1988).

Conclusions and Future Work

We have proposed a novel materialisation-based approach for reasoning in Datalog MTL a highly expressive extension of Datalog with operators from metric temporal logic. Our algorithm achieves termination by exploiting a specific saturation condition, which ensures that materialisation can be stopped after a bounded number of rounds of rule applications, without compromising completeness of reasoning. We have implemented our approach and conducted experiments supporting its feasibility in practice.

Acknowledgments This research was supported in whole or in part by the EPSRC projects OASIS (EP/S032347/1), Con Cu R (EP/V050869/1) and UK FIRES (EP/S019111/1), the SIRIUS Centre for Scalable Data Access, and Samsung Research UK. For the purpose of Open Access, the authors have applied a CC BY public copyright licence to any Author Accepted Manuscript (AAM) version arising from this submission.

References Alur, R.; and Henzinger, T. A. 1994. A Really Temporal Logic. J. ACM, 41(1): 181 203. Areces, C.; and Orbe, E. 2015. Symmetric blocking. Theor. Comput. Sci., 606: 25 41. Artale, A.; Kontchakov, R.; Kovtunova, A.; Ryzhikov, V.; Wolter, F.; and Zakharyaschev, M. 2021a. First-order rewritability of ontology-mediated queries in linear temporal logic. Artif. Intell., 299: 103536. Artale, A.; Kontchakov, R.; Kovtunova, A.; Ryzhikov, V.; Wolter, F.; and Zakharyaschev, M. 2021b. First-order rewritability of ontology-mediated queries in linear temporal logic. Artif. Intell., 299: 103536. Artale, A.; Kontchakov, R.; Ryzhikov, V.; and Zakharyaschev, M. 2013. The Complexity of Clausal Fragments of LTL. In Proc. of LPAR, 35 52. Baader, F.; Borgwardt, S.; Koopmann, P.; Ozaki, A.; and Thost, V. 2020. Metric Temporal Description Logics with Interval-Rigid Names. ACM Trans. Comput. Logic, 21(4). Baudinet, M.; Chomicki, J.; and Wolper, P. 1993. Temporal Deductive Databases. In Tansel, A. U.; Clifford, J.; Gadia, S. K.; Segev, A.; and Snodgrass, R. T., eds., Temporal Databases: Theory, Design, and Implementation, 294 320. Benjamin/Cummings. Beck, H.; Dao-Tran, M.; Eiter, T.; and Fink, M. 2015. LARS: A Logic-Based Framework for Analyzing Reasoning over Streams. In Proc. of AAAI, 1431 1438. Bellomarini, L.; Nissl, M.; and Sallinger, E. 2022. i Temporal: An extensible Temporal Benchmark Generator. In Proc. of ICDE, 2021 2033. Bellomarini, L.; Sallinger, E.; and Gottlob, G. 2018. The Vadalog system: Datalog-based reasoning for knowledge graphs. Proc. VLDB Endow., 11(9): 975 987. Bolander, T.; and Blackburn, P. 2007. Termination for Hybrid Tableaus. J. Log. Comput., 17(3): 517 554. Brandt, S.; Kalaycı, E. G.; Ryzhikov, V.; Xiao, G.; and Zakharyaschev, M. 2018. Querying Log Data with Metric Temporal Logic. J. Artif. Intell. Res., 62: 829 877. Brandt, S.; Kontchakov, R.; Ryzhikov, V.; Xiao, G.; and Zakharyaschev, M. 2017. Ontology-based data access with a Horn fragment of metric temporal logic. In Proc. of AAAI, 1070 1076. Bry, F.; Eisinger, N.; Eiter, T.; Furche, T.; Gottlob, G.; Ley, C.; Linse, B.; Pichler, R.; and Wei, F. 2007. Foundations of rule-based query answering. In Reasoning Web, 1 153.

Brzoska, C. 1998. Programming in metric temporal logic. Theor. Comput. Sci., 202(1-2): 55 125. Cabalar, P.; Dieguez, M.; Schaub, T.; and Schuhmann, A. 2020. Towards metric temporal answer set programming. Theory Pract. Log. Program., 20(5): 783 798. Carral, D.; Dragoste, I.; González, L.; Jacobs, C. J. H.; Krötzsch, M.; and Urbani, J. 2019. VLog: A rule engine for knowledge graphs. In Proc. of ISWC, 19 35. Ceri, S.; Gottlob, G.; and Tanca, L. 1989. What you always wanted to know about Datalog (and never dared to ask). IEEE Trans. Knowl. Data. Eng., 1(1): 146 166. Chafik, A.; Cheikh-Alili, F.; Condotta, J.-F.; and Varzinczak, I. 2021. A One-Pass Tree-Shaped Tableau for Defeasible LTL. In Proc. of TIME, 16:1 16:18. Chomicki, J. 1990. Polynomial time query processing in temporal deductive databases. In Proc. of PODS, 379 391. Chomicki, J. 1995. Depth-bounded bottom-up evaluation of logic programs. J. Log. Program., 25(1): 1 31. Chomicki, J.; and Imieli nski, T. 1988. Temporal deductive databases and infinite objects. In Proc. of PODS, 61 73. Glimm, B.; Horrocks, I.; and Motik, B. 2010. Optimized Description Logic Reasoning via Core Blocking. In Proc. of IJCAR, 457 471. Gutiérrez-Basulto, V.; Jung, J. C.; and Kontchakov, R. 2016. Temporalized EL Ontologies for Accessing Temporal Data: Complexity of Atomic Queries. In Proc. of IJCAI, 1102 1108. Horrocks, I.; and Sattler, U. 1999. A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput., 9(3): 385 410. Kalaycı, E. G.; Xiao, G.; Ryzhikov, V.; Kalayci, T. E.; and Calvanese, D. 2018. Ontop-temporal: a tool for ontologybased query answering over temporal data. In Proc. of CIKM, 1927 1930. Kikot, S.; Ryzhikov, V.; Wał ega, P. A.; and Zakharyaschev, M. 2018. On the data complexity of ontology-mediated queries with MTL operators over timed words. In Proc. of DL. Koopmann, P. 2019. Ontology-based query answering for probabilistic temporal data. In Proc. of AAAI, 2903 2910. Koymans, R. 1990. Specifying real-time properties with metric temporal logic. Real-Time Syst., 2(4): 255 299. Manna, Z.; and Wolper, P. 1982. Synthesis of communicating processes from Temporal Logic specifications. In Proc. of Workshop on Logics of Programs, 253 281. Motik, B.; Nenov, Y.; Piro, R.; Horrocks, I.; and Olteanu, D. 2014. Parallel materialisation of Datalog programs in centralised, main-memory RDF systems. In Proc. of AAAI, 129 137. Reynolds, M. 2016. A New Rule for LTL Tableaux. In Proc. of Gand ALF, 287 301. Ryzhikov, V.; Wał ega, P. A.; and Zakharyaschev, M. 2019. Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics. In Proc. of IJCAI, 1851 1857.

Schmidt, R. A.; and Tishkovsky, D. 2011. Automated Synthesis of Tableau Calculi. Log. Methods Comput. Sci., 7(2): 1 32. Schmidt, R. A.; and Waldmann, U. 2015. Modal Tableau Systems with Blocking and Congruence Closure. In Proc. of TABLEAUX, 38 53. Sistla, A. P.; and Clarke, E. M. 1985. The Complexity of Propositional Linear Temporal Logics. J. ACM, 32(3): 733 749. Tena Cucala, D. J.; Wał ega, P. A.; Cuenca Grau, B.; and Kostylev, E. V. 2021. Stratified Negation in Datalog with Metric Temporal Operators. In Proc. of AAAI, 6488 6495. Wał ega, P. A.; Cuenca Grau, B.; Kaminski, M.; and Kostylev, E. V. 2019. Datalog MTL: Computational complexity and expressive power. In Proc. of IJCAI, 1886 1892. Wał ega, P. A.; Cuenca Grau, B.; Kaminski, M.; and Kostylev, E. V. 2020a. Datalog MTL over the Integer Timeline. In Proc. of KR, 768 777. Wał ega, P. A.; Cuenca Grau, B.; Kaminski, M.; and Kostylev, E. V. 2020b. Tractable Fragments of Datalog with Metric Temporal Operators. In Proc. of IJCAI, 1919 1925. Wał ega, P. A.; Kaminski, M.; and Cuenca Grau, B. 2019. Reasoning over streaming data in metric temporal Datalog. In Proc. of AAAI, 3092 3099. Wał ega, P. A.; Tena Cucala, D. J.; Kostylev, E. V.; and Cuenca Grau, B. 2021. Datalog MTL with Negation Under Stable Models Semantics. In Proc. of KR, 609 618. Wał ega, P. A.; Zawidzki, M.; and Cuenca Grau, B. 2021. Finitely materialisable Datalog programs with metric temporal operators. In Proc. of KR, 619 628. Wang, D.; Hu, P.; Wał ega, P. A.; and Grau, B. C. 2022. Me Teo R: Practical Reasoning in Datalog with Metric Temporal Operators. In Proc. of AAAI, 5906 5913.