Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Incremental Maintenance of DatalogMTL Materialisations

Kaiyue Zhao, Dingqi Chen, Shaoyu Wang, Pan Hu

TL;DR

The paper tackles the problem of maintaining DatalogMTL materialisations under dynamic updates by introducing DRedMTL, an incremental algorithm built on the classic DRed approach but adapted for temporal recursion through periodic materialisations. It develops a seminaïve evaluation operator tailored to the DatalogMTL setting and a period identification mechanism to ensure finite termination, enabling unfolding of infinite temporal reasoning into a finite representation. The method employs a trio of periodic operators (Ext, Aln, Cup) and three update phases (Overdelete, Rederive, Insert) to update the materialisation efficiently without full recomputation. Experiments on multiple public benchmarks demonstrate substantial speedups over rematerialisation, especially for small updates, highlighting the approach's practicality for streaming and time-sensitive domains. The work lays the foundation for scalable, dynamic temporal reasoning in real-world applications and suggests avenues for integrating with other incremental strategies and stream-processing frameworks.

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.

Incremental Maintenance of DatalogMTL Materialisations

TL;DR

The paper tackles the problem of maintaining DatalogMTL materialisations under dynamic updates by introducing DRedMTL, an incremental algorithm built on the classic DRed approach but adapted for temporal recursion through periodic materialisations. It develops a seminaïve evaluation operator tailored to the DatalogMTL setting and a period identification mechanism to ensure finite termination, enabling unfolding of infinite temporal reasoning into a finite representation. The method employs a trio of periodic operators (Ext, Aln, Cup) and three update phases (Overdelete, Rederive, Insert) to update the materialisation efficiently without full recomputation. Experiments on multiple public benchmarks demonstrate substantial speedups over rematerialisation, especially for small updates, highlighting the approach's practicality for streaming and time-sensitive domains. The work lays the foundation for scalable, dynamic temporal reasoning in real-world applications and suggests avenues for integrating with other incremental strategies and stream-processing frameworks.

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.

Paper Structure

This paper contains 26 sections, 50 theorems, 36 equations, 4 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Syntax of DatalogMTL
  4. Semantics of DatalogMTL
  5. Materialisation for DatalogMTL
  6. The Delete/Rederive Algorithm
  7. Motivation
  8. DRed for DatalogMTL
  9. Algorithm Overview
  10. Period Identification
  11. Implementation of Periodic Operators
  12. Evaluation
  13. Benchmarks
  14. Test Settings
  15. Results
  16. ...and 11 more sections

Key Result

Theorem 1

If given input $\mathds{D}_1$,$\mathds{D}_2$, Algorithm algo:periodic_minus and algo:periodic_union output $\mathds{D}_m$ and $\mathds{D}_u$, respectively, then $\mathsf{unfold}(\mathds{D}_1)-\mathsf{unfold}(\mathds{D}_2) = \mathsf{unfold}(\mathds{D}_m)$ and $\mathsf{unfold}(\mathds{D}_1)\cup\mathsf

Theorems & Definitions (105)

  • Definition 1
  • Definition 2
  • Example 1
  • Definition 3
  • Theorem 1
  • Theorem 2
  • Theorem 2
  • Claim 1
  • proof
  • Claim 2
  • ...and 95 more