Incremental Maintenance of DatalogMTL Materialisations

AI summary

Overview

Research area: Knowledge representation and reasoning, specifically materialisation-based reasoning over temporal knowledge bases. The work sits at the intersection of Datalog rule languages, metric temporal logic (MTL), and incremental view maintenance.

Technical level: Advanced. The paper assumes familiarity with Datalog semantics, least models and immediate-consequence operators, transfinite iteration, and temporal logic operators, and it formalises its algorithm over saturated interpretations and periodic unfoldings.

Scope in one sentence: The paper defines DRedMTL, an incremental algorithm for maintaining the materialisation of bounded DatalogMTL programs when explicit facts are added to or removed from the dataset, and evaluates it against rematerialisation on publicly available datasets.

What This Paper Is About

DatalogMTL extends Datalog with metric temporal logic so that rules can reason over time, but existing materialisation-based reasoners recompute the entire materialisation from scratch whenever the input data changes. This is wasteful for applications with frequent updates. The paper adapts the classical Delete/Rederive (DRed) algorithm from plain Datalog to DatalogMTL, where materialisations are infinite but can be finitely represented as a set of facts plus periodic intervals. The goal is to update such a finite periodic representation in place, rather than rebuilding it.

Key Contributions

1. DRedMTL, an incremental maintenance algorithm for DatalogMTL materialisations. Drawing on the DRed algorithm for plain Datalog, it provides overdeletion, rederivation, and insertion stages that update a materialisation in response to deletions (E⁻) and insertions (E⁺) into a dataset E, without recomputation from scratch. The authors state that, to their knowledge, no incremental maintenance algorithm for DatalogMTL reasoning previously existed.

2. A formal notion of periodic materialisation. The paper defines a periodic materialisation as a triple ⟨I, ϱ_L, ϱ_R⟩ where I is a saturated interpretation and ϱ_L and ϱ_R are its left and right periods, together with an unfolding operation unfold(I) that reconstructs the canonical model ℭ_{Π,E}. This gives a finite object that the update algorithm can maintain in place.

3. A new seminaïve evaluation operator for DatalogMTL updates. The operator Π⟨I ⋮ Δ⟩ computes consequences that depend on the facts changed in the previous round, generalising seminaïve evaluation so that it both narrows the affected consequences and supports period identification.

4. A period-identification algorithm (Pds) that works on updates rather than the whole materialisation. Instead of comparing intervals across the entire materialisation, the algorithm identifies periods within the updated facts and their consequences, with loop termination triggered by successfully discovering a period pair. An accompanying example shows how this cuts period detection from O(n) comparisons to O(1) comparisons for the case studied.

Main Findings

• Incremental maintenance is feasible for DatalogMTL. The paper shows how overdeletion, rederivation, and insertion for plain Datalog can be lifted to the temporal setting by operating on saturated interpretations and their periods rather than on finite fact sets.

• Two specific obstacles had to be overcome. First, seminaïve evaluation had not been studied in combination with the construction of saturated interpretations; second, unlike Datalog, a large share of DatalogMTL materialisation cost goes to period identification (termination checks), so that procedure had to be made incremental too.

• Period detection is the cost driver. The paper explains that period identification enumerates pairs of intervals of a given length and compares their contents pairwise, so its cost grows with the number of facts inside those intervals. Restricting this to updated facts, rather than the full materialisation, is the central efficiency argument.

• Recursion over time propagates changes non-locally. Because DatalogMTL permits recursion over time and can produce unbounded intervals, a deletion cannot be handled by propagating only to immediate derivations; effects can propagate across time through periodic patterns, which is why the rederivation stage enlarges its interval of interest across rounds of the loop.

• Illustrative worked example. For a program consisting of the single rule ⊞[0,1] R(x) ← ⊟[9,10] R(x) with dataset E = {R(a_i)@[0,1] | 0 < i < n}, E⁻ = {R(a_1)@[0,1]}, and E⁺ = {R(a_n)@[0,1]}, the paper reports depth(Π) = 11, saturation at k = 4, with possible periods ϱ_left = [-24, -23) and ϱ_right = [24, 34). Rematerialisation and full materialisation take O(n) time, whereas the incremental overdeletion takes O(1) time.

• Experimental claim. The approach was implemented (the paper lists code, datasets, and instructions at github.com/Horizon12275/DREDmtl-for-DatalogMTL) and tested on several publicly available datasets. The reported outcome is that DRedMTL "often significantly outperforms rematerialisation, sometimes by orders of magnitude," with the stated advantage being largest for small updates. Specific dataset names, dataset sizes, rule counts, timings, and speedup factors are not reported in the provided content.

• A concrete application motivates the work. The authors' research group applied DatalogMTL to automatic detection of power transformer anomalies: gas-in-oil sensor readings feed a rule engine, and a rule derives OTF(x) (oil thermal fault) from HasEthylene(x,y), HasEthane(x,z), and the past-ten-minute conditions ⊟[0,10] AboveThirty(y) and ⊟[0,10] AboveSeventy(z), i.e. gas concentrations above 30 ppm and 70 ppm at some time point in the past ten minutes.

Methodology in Plain English

The authors start from the DRed algorithm, which maintains a Datalog materialisation in three phases: overdeletion (eagerly remove everything that might have depended on the deleted facts), rederivation (recover those removed facts that still follow from the remaining data), and insertion (compute consequences of the newly added facts and of the rederived ones).

The complication is that DatalogMTL materialisations can be infinite. The authors rely on the established result that a bounded program and dataset have a saturated interpretation — a finite interpretation that already satisfies the program over a region and whose behaviour repeats with a fixed period to the left and to the right. From this finite representation, the full infinite canonical model is obtained by periodically unfolding the pattern.

Their algorithm maintains that finite object rather than raw facts. During overdeletion it iteratively applies the program to the deleted facts using a new seminaïve operator that only looks at facts derived in the previous round, while a period-identification routine (Pds) checks whether the updated facts already exhibit a repeating pattern. When a period pair is found, that run of the computation stops and the periodic materialisation is contracted. Rederivation runs the same loop in reverse, expanding the interval of interest round by round so that facts lost anywhere along the timeline can be recovered, again stopping as soon as periods are found. Insertion mirrors overdeletion, accumulating new facts and their consequences while checking for periodic structure.

The design intent is that the work done per update should scale with the size of the update, not the size of the whole materialisation, which is why period detection is confined to updated facts and their consequences.

Why This Matters

Impact on research. Materialisation-based reasoning is the dominant practical approach for DatalogMTL, and the paper identifies incremental maintenance as an unsupported feature of that landscape. By transplanting DRed into the temporal setting, it opens a line of work on update-efficient temporal rule reasoning parallel to the DRed, B/F, and FBF families for plain Datalog, and it raises the specific technical question of how termination checks (period identification) can themselves be made incremental.

Real-world applications (as described in the paper):

• Ontology-based query answering, cited via Brandt et al. 2018 and Güzel Kalayci et al. 2018.
• Stream reasoning, cited via Wałęga et al. 2023 and Wałęga et al. 2019, where data arrives continuously and updates are constant.
• Temporal reasoning in the financial sector, cited via Colombo et al. 2023, Nissl and Sallinger 2022, and Mori et al. 2022.
• Industrial monitoring of power transformers, the authors' own application, where gas-in-oil sensor readings are fed in real time to a DatalogMTL engine that fires alarms—a setting with frequent small data arrivals.

Industry relevance. The motivating scenario is a monitoring pipeline where sensors stream readings and alarms must be recomputed as data changes; recomputing a full materialisation for each small update is exactly the cost the algorithm targets. The paper reports that the benefit is largest for small updates, and updates in streaming and sensor settings are typically small compared with accumulated history. The authors also state that existing systems such as vadalog, MeTeoR, and magic set rewriting for DatalogMTL must recompute from scratch when explicit facts change.

Future Directions

• Benchmark transparency and broader evaluation. The paper reports significant improvements over rematerialisation but, in the content provided, does not name the datasets, their sizes, or give absolute timings; a fuller experimental picture across update sizes and program shapes would clarify when the approach pays off.
• Tightening the theoretical guarantees around period identification. The paper notes that correctly updating repeating structures is challenging because consequence propagation and termination-condition checks interact; proving and characterising the correctness and worst-case behaviour of on-the-fly period detection using only updated facts is a natural continuation.
• Worst-case behaviour for large or adversarial updates. The efficiency argument rests on updates being small relative to the materialisation; understanding degradation when an update touches a large fraction of the timeline is left open.
• Integration with existing DatalogMTL engines. The related work discusses vadalog, MeTeoR, and magic set rewriting for DatalogMTL; embedding incremental maintenance in those systems, and combining it with top-down or magic-set evaluation, is a plausible next step. The paper does not commit to these directions itself.

Target Audience

Researchers and advanced practitioners in knowledge representation, rule-based reasoning, and temporal databases who work on materialisation, incremental view maintenance, or query answering over temporal data. It is also relevant to engineers building always-on rule engines for streaming or sensor data (such as the transformer-monitoring scenario) who need reasoning results to stay current under frequent, small input changes. Readers need a working grasp of Datalog semantics and metric temporal logic operators to follow the formal sections; the paper's motivating example and algorithm outline are accessible to those with a background in logic programming, while the saturation and period constructions are aimed at specialists.

Authors’ abstract

DatalogMTL extends the classical Datalog language with metric temporal logic (MTL), enabling expressive reasoning over temporal data. While existing reasoning approaches, such as materialisation based and automata based methods, offer soundness and completeness, they lack support for handling efficient dynamic updates, a crucial requirement for real-world applications that involve frequent data updates. In this work, we propose DRedMTL, an incremental reasoning algorithm for DatalogMTL with bounded intervals. Our algorithm builds upon the classical DRed algorithm, which incrementally updates the materialisation of a Datalog program. Unlike a Datalog materialisation which is in essence a finite set of facts, a DatalogMTL materialisation has to be represented as a finite set of facts plus periodic intervals indicating how the full materialisation can be constructed through unfolding. To cope with this, our algorithm is equipped with specifically designed operators to efficiently handle such periodic representations of DatalogMTL materialisations. We have implemented this approach and tested it on several publicly available datasets. Experimental results show that DRedMTL often significantly outperforms rematerialisation, sometimes by orders of magnitude.