DatalogMTL is a recently introduced extension of Datalog with operators from metric temporal logic (MTL). It allows for performing complex temporal reasoning tasks over the rational timeline, which makes it suitable for many practical applications. Although the main reasoning tasks in DatalogMTL are decidable, they have high computational complexity, and so, developing practically eficient reasoning techniques is challenging. Consequently, a number of approaches have been recently established; some of them have already been implemented and tested experimentally, but no comparison of these techniques has been provided yet. To fill this gap, we present an overview of reasoning techniques in DatalogMTL, sketch relations between them, and discuss their properties. Moreover, we present our ongoing research in this area and possible future directions thereof.
DatalogMTL [
Active() ←
Turbine () ∧ ⊟[0,60)Below 0.15() ∧ x[60,63] ⊟[
Due to its high expressive power, DatalogMTL has found a number of potential applications,
including stream reasoning [
In this paper, we provide a comprehensive overview of the diferent reasoning techniques available for DatalogMTL and discuss future research directions. In particular, we observe that reasoning techniques for DatalogMTL can be divided into two main groups: 1. Approaches based on materialisation (a.k.a. forward chaining), which derive and store in memory all facts that are entailed by a program and dataset. This is obtained by means of successive rounds of rule applications until a fixpoint is reached; the resulting set of facts is called the materialisation. In these approaches, fact entailment and query answering are performed directly over the materialisation. The main obstacle, however, is that the materialisation process in DatalogMTL is not guaranteed to terminate. 2. Approaches based on discretisation of the rational timeline, that is, on partitioning the dense timeline into a discrete sequence of intervals, within which all the time points satisfy the same relational atoms. Since this sequence of intervals is discrete, it allows us for exploiting techniques used for reasoning in temporal logics interpreted over the discrete timeline (e.g., linear temporal logic LTL). The problem of such approaches is that their implementations are usually ineficient in practice.
In the remainder of this paper, we will discuss in detail these approaches. We start by recapitulating the syntax, semantics, and main reasoning tasks for DatalogMTL in Section 2. In Section 3, we describe materialisation-based reasoning techniques, which exploit the fixpoint characterisation of the DatalogMTL semantics; in particular, we discuss the naïve approach to materialisation which does not guarantee termination, introduce finitely materialisable programs for which materialisation always terminates, and discuss algorithms based on sliding windows which are particularly useful in the stream reasoning setting. Next, in Section 4, we describe reasoning based on the discretisation of time; we show how the timeline can be discretised and how discretisation can be used to devise a translation to LTL or to provide Büchi automata and arithmetic progressions capturing the meaning of a DatalogMTL program. Finally, we present our ongoing research and outline its possible future directions in Section 5.
In this section, we introduce DatalogMTL; we will focus on the standard setting given by
‘continuous semantics’ and interpretations over the rational timeline. It is, however, worth
mentioning that DatalogMTL was also studied under an alternative ‘pointwise’ semantics [
Syntactically, DatalogMTL is an extension of Datalog with the MTL operators x, |, ⊟, ⊞, , and , which are indexed with rational intervals containing only non-negative numbers. We distinguish two types of atoms. Relational atoms are standard Datalog atoms of the form (s), with an arbitrary arity predicate and a tuple s of terms (variables or constants). Metric atoms extend relational atoms by allowing MTL operators, and are generated by the following grammar:
::= ⊤ | ⊥ | (s) | x | | | ⊟ | ⊞ | | .
Then, DatalogMTL rules are of the form ′ ← 1 ∧ · · · ∧ , for ≥ 1, where each body atom is a metric atom, and the head atom ′ is a metric atom not mentioning any of the ‘non-deterministic’ operators x, |, , and . As usual, a program Π is a finite set of safe rules, but the definition of safety in DatalogMTL is slightly more elaborated than in Datalog. In particular, we do not only require that each variable in a rule’s head occurs in this rule’s body, but also that this occurrence in the body is not in a left operand of or . This additional requirement discards, for example, a rule of the form () ← ()[0,0]⊤, which is equivalent to () ← ⊤ (see the semantics of DatalogMTL operators from the next subsection), and so, should not be treated as safe.
A DatalogMTL dataset is a finite set of facts of the form @, where is a ground (i.e., with no variables) relational atom and is an interval in which holds true.
A DatalogMTL interpretation I can be seen as a set containing one standard Herbrand interpretation for each rational time point. More precisely, I specifies, for each ground relational atom and each time point ∈ Q, whether holds at , in which case we write I, |= . Satisfaction of relational atoms determines satisfaction of (more complex) metric atoms, as presented below.
I, |= ⊤ I, |= ⊥ I, |= x I, |= | I, |= ⊟ I, |= ⊞ I, |= 12 I, |= 12 if if if if if if for each , for no , I, ′ |= for some ′ with − ′ ∈ , I, ′ |= for some ′ with ′ − ∈ , I, ′ |= for all ′ with − ′ ∈ , I, ′ |= for all ′ with ′ − ∈ , I, ′ |= 2 for some ′ with − ′ ∈ and I, ′′ |= 1 for all ′′ ∈ (′, ), I, ′ |= 2 for some ′ with ′ − ∈ and I, ′′ |= 1 for all ′′ ∈ (, ′).
A fact @ is satisfied if is satisfied at all time points ∈ , whereas a rule is satisfied if, for each of its ground instances ′ and for each time point , if all the body atoms of ′ are satisfied at , then so is the head of ′. As usual, a model of a dataset or of a program Π is an interpretation which satisfies all facts in or all rules in Π , respectively. Program Π and dataset are consistent if they have a model (note that if none of the rules mentions ⊥ in the head, then an inconsistency cannot occur—in the absence of negation in the language of DatalogMTL, ⊥ is the only means for expressing a contradiction), and they entail a fact @ if each model of both Π and is a model of @.
The main reasoning tasks considered in DatalogMTL are fact entailment and consistency checking.
These problems polynomially reduce to the complements of each other [
We observe that there is a group of reasoning techniques for DatalogMTL whose main component is the materialisation process. This process mimics the fixpoint characterisation of DatalogMTL semantics, as we describe in the first part of this section.
The fixpoint characterisation is based on the observation that each pair of a consistent program Π and a dataset admits a unique least model, which we refer to as their canonical interpretation CΠ,. As in Datalog, we can construct this interpretation by applying rules of Π to in a forward-chaining manner until a fixpoint is reached. However, unlike in Datalog, the fixpoint in DatalogMTL may only be reachable after infinitely many materialisation steps; for example, given a fact @0, the rule ⊞1 ← propagates to all positive integers, which requires materialisation steps.
Formally, we define the immediate consequence operator Π for a program Π as the operator mapping each interpretation I to the least interpretation containing I and satisfying the following property for each ground instance of a rule in Π : whenever I satisfies each body // initialise new Procedure 1: Materialisation-based reasoning
Input: A program Π and a dataset
Output: A dataset 1 new := ; 2 repeat 3 4 5 until old = new; 6 return new; old := new; // copy new before applying rules new := the least dataset representation of Π(Inew ); atom of at a time point , then Π(I) satisfies the head of at . Subsequent applications of Π to the (least) model I of define the following sequence of interpretations, for all ordinals : Π0 (I) = I, Π (I) = Π (︀ Π− 1(I)︀) , Π (I) = ⋃︁ Π(I), < for a successor ordinal, for a limit ordinal.
If Π and are consistent, then the canonical interpretation is obtained after at most 1 (i.e.,
the first uncountable ordinal) applications of the immediate consequence operator; that is,
CΠ, = Π1 (I) [
The fixpoint characterisation suggests a naïve materialisation-based reasoning approach presented in Procedure 1; given a program Π and a dataset , the procedure applies the immediate consequence operator Π until no new facts can be derived, that is, a fixpoint is reached.
We have recently implemented this approach in the metric temporal reasoner MeTeoR, and
provided an eficient way of computing Π(Inew ), which allowed us to handle datasets with
hundreds of millions of facts [
The advantage of rewriting DatalogMTL programs into SQL is that constructed queries can
be evaluated with standard systems such as PostgreSQL or Apache Spark. The downside of
this approach, however, is that relying on SQL systems limits the possibility of controlling and
optimising computations which are specific to DatalogMTL materialisation. Such materialisation
requires, for example, computing numerous temporal joins, and the experimental evaluation [
Clearly, materialisation is a sound reasoning technique, but the procedure is not always terminating, as reaching the fixpoint may require an infinite number of materialisation steps. However, if a fixpoint is reached, then a representation of the full canonical interpretation can be kept in memory, which can be used for an eficient verification of entailment of any fact. 6 until old = new; 7 return true; Algorithm 2: Checking finite materialisability for a single dataset
Input: A bounded program Π and a bounded dataset Output: A Boolean value old := new; new := the least dataset representation of Π(Inew ); if there is @ ∈ new with ̸⊆ Π, then Return false;
Recent experiments suggest that, when materialisation terminates, it is a very scalable technique for DatalogMTL which is well suited for reasoning with large temporal datasets. Therefore, a natural question arises—for which reasoning instances does naïve materialisation terminate?
This question has recently been studied by introducing the notion of finitely materialisable programs. In particular, we can consider a data-dependent and a data-independent variant of this notion as follows. We say that a program Π is finitely materialisable for a dataset if, when applied to , the immediate consequence operator Π reaches a fixpoint in finitely many steps. The data-independent notion considers finite materialisability of Π for all datasets.
The problem of checking whether a program is finitely materialisable, as well as the complexity
of reasoning in finitely materialisable programs have recently been studied for programs and
datasets in which all intervals are bounded (i.e., do not mention infinities as endpoints) [
On the other hand, checking if a program Π is finitely materialisable for all datasets reduces
to checking if Π is finitely materialisable for a specific critical dataset Π consisting of facts
(s)@[0, depth(Π)] , for all predicates occurring in Π , all tuples s of constants in Π (and one
additional fresh constant), and depth(Π) a suficiently large number depending on the intervals
occurring in Π [
Testing finite materialisability is a useful static analysis task, which can be performed ofline. If the program is finitely materialisable, then a scalable materialisation-based algorithm with termination guarantees can be used. Reasoning with finitely materialisable programs is also suficiently easier from the theoretical point of view, as it is ExpTime-complete for combined complexity, in contrast to ExpSpace-completeness for full DatalogMTL.
Another reasoning approach in DatalogMTL consists in materialising all the facts within a
bounded fragment of the timeline—called a window—and then sliding the window by some
distance towards the future. The algorithm ‘forgets’ all the facts outside the current window
and repeats the process, by materialising all the facts in the current window, and then, sliding it
further towards the future. The main advantage of this approach is that it keeps in memory only
facts describing a fixed fragment of the timeline. Hence, the approach is particularly useful in
the stream reasoning setting, where reasoning is performed based on a continuously increasing
and potentially infinite stream of input facts, in contrast to a static dataset considered in the
standard setting [
Like the other materialisation-based techniques for reasoning in DatalogMTL, using sliding
windows constitutes a sound approach. Notice, however that, in general, materialisation based
only on the information kept within a bounded window may lead to the incompleteness of
reasoning. Nevertheless, completeness can be retained for forward-propagating programs, where
rules can propagate information only towards the future, and which are a natural choice in the
stream reasoning setting [
Although the timeline in DatalogMTL is dense, it can be divided into regularly distributed
intervals which are uniform in the sense that all time points belonging to the same interval
satisfy exactly the same relational atoms. This observation was first exploited to partition the
rational timeline, for a program Π and dataset , into punctual intervals [ · , · ] and open
intervals (( − 1) · , · ), for each ∈ Z, where is the greatest common divisor (gcd) of the
numbers occurring as interval endpoints in Π and [
Discretisartion of time was exploited by Brandt et al. [
In its basic variant, LTL is a propositional modal logic interpreted over the ordered set of natural numbers, whose language involves boolean connectives and temporal operators ○ for at the previous time point , □ for always in the past, ○ for at the next time point, and □ for always in the future. An LTL formula is satisfiable if there exists an LTL model in which is satisfied at 0.
Since, in contrast to DatalogMTL, the language of LTL is propositional, the first step in the translation is to ground Π with all constants occurring in Π or . Then, every relational atom (c) occurring in the grounding of Π with constants from Π and is translated into a propositional symbol c. Moreover, since LTL does not allow for metric operators, the binaryencoded MTL operators occurring in Π need to be rewritten to basic LTL operators. Note that both the grounding of the initial program Π and then expanding the binary-encoded numbers involved in an MTL operator into sequences of LTL operators lead to an exponential blow-up. For example, assume that Π mentions an atom ⊟[0,60)(). Moreover, let Π and mention 100 constants 1, . . . , 100 and assume that after a discretisation of the timeline the interval [0, 60) contains 600 intervals. Then ⊟[0,60)() is translated to an LTL-formula containing 100 conjuncts (one conjunct for each ∈ {1, . . . , 100}), each of the form () ∧ ○ () ∧ ○ ○ () ∧ · · · ∧ ○ ⏟ · · · ○ 599⏞ ().
Consequently, Π, is exponentially large. Since satisfiability checking in LTL is
PSpacecomplete, this approach provides an ExpSpace reasoning procedure for DatalogMTL, which is
worst-case optimal. Although it allows for using optimised of-the-shelf reasoning systems for
LTL, it turns out that due to the exponential grounding of a program and the encoding of MTL
operators, the approach is ineficient in practice [
Another method of reasoning in DatalogMTL was obtained by directly applying to DatalogMTL
techniques known for LTL, instead of translating the former to the latter. In particular, one of
the main approaches to checking satisfiability of an LTL-formula consists in constructing a
generalised non-deterministic Büchi automaton whose states are sets of formulas relevant for ,
alphabet consists of sets of propositions, whereas transition relation and accepting conditions
ensure that words accepted by the automaton are exactly models of [
To adapt this technique to the needs of DatalogMTL, the automaton was modified as
follows [
It was shown that consistency checking in DatalogMTL reduces to checking non-emptiness
of (pairs of) the above-described automata, and that the latter is feasible in PSpace [
This approach provides a worst-case optimal reasoning approach for full DatalogMTL, which
was implemented as part of the MeTeoR system [
Discretisation of time proved also useful in establishing low-complexity fragments of DatalogMTL. In particular, it allowed for constructing specific reasoning techniques for fragments in which x is the only MTL operator occurring in a program, and moreover, each rule is core, that is, has at most one body atom (DatalogMTLx) or each rule is linear in the sense that it can mention at most one intensional (IDB) body atom (DatalogMTLx).
The discussed reasoning technique for DatalogMTLx is based on two main observations.
First, since there are no conjunctions in rule bodies nor box operators (which simulate
conjunctions), all derivations in DatalogMTLx can be seen as sequences of facts, where each
fact is derived only based on the previous fact in the sequence. Secondly, although the second
type of the timeline discretisation from Section 4.1 yields intervals of diferent length, there
are polynomially many types of intervals (c.f. the figure from Section 4.1 with four types of
intervals). These observations allow us to represent all derivations as paths in a temporal
dependency graph [
• 1 0 3 4 • 0 • 1 8 8
• 0
•
1
8
8
The graph shows that, for example, holding at some interval of type 1 (vertex 1 ) allows us
to derive in the interval of type 0 (vertex 0) which is located 3 intervals (the weight of the
edge from 1 to 0) to the right from . Lengths of paths (i.e., derivations) connecting any pair
of vertices in such a graph can be succinctly represented with a set of arithmetic progressions
after transforming the initial graph into the Chrobak normal form for automata [
This reasoning technique can be extended to DatalogMTLx. The structure of DatalogMTLx programs allows for decomposing the timeline into (polynomially many) sections in which reasoning can be performed with the technique established for DatalogMTLx. The existence of these sections, however, leads to an increase of the data complexity from TC0 to NL.
Although fact entaiment in both DatalogMTLx and DatalogMTLx is tractable in data complexity, and the discussed algorithms are optimal, to the best of our knowledge they have not yet been implemented.
A promising direction of future work, thrusting from the ongoing research on reasoning
techniques for DatalogMTL, stems from the observation that the canonical model of a program
Π and a dataset has a periodic structure (which corresponds to ultimately periodic LTL models).
In particular, by the translation to LTL and reasoning techniques that rely on Büchi automata,
it follows that there exists a left period 1 and a right period 2 such that for all (suficiently
small) time points , the same relational atoms hold in CΠ, at and − 1, whereas for all
(suficiently large) , the same relational atoms hold in CΠ, at and + 2. If we knew 1 and
2 in advance, we could use them to significantly speed up the materialisation process, and
potentially guarantee its termination for of all programs. The main problem, however, is that
although an (impractically large) upper bound on the length of the periods can be determined
[
Another interesting direction focuses on optimising materialisation, e.g., by developing semi naïve and parallel rule evaluation strategies and incremental materialisation maintenance techniques.
This work has been supported by the EPSRC projects OASIS (EP/S032347/1), AnaLOG (EP/P025943/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.