Incremental Maintenance of DatalogMTL Materialisations
- URL: http://arxiv.org/abs/2511.12169v2
- Date: Wed, 19 Nov 2025 16:30:26 GMT
- Title: Incremental Maintenance of DatalogMTL Materialisations
- Authors: Kaiyue Zhao, Dingqi Chen, Shaoyu Wang, Pan Hu,
- Abstract summary: We propose DRedMTL, an incremental reasoning algorithm for DatalogMTL with bounded intervals.<n>Our algorithm builds upon the classical DRed algorithm, which incrementally updates the materialisation of a Datalog program.<n>We have implemented this approach and tested it on several publicly available datasets.
- Score: 5.957946033104924
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- 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.
Related papers
- Time Series Reasoning via Process-Verifiable Thinking Data Synthesis and Scheduling for Tailored LLM Reasoning [46.72047865932384]
We introduce VeriTime, a framework that tailors large language models for time series reasoning through data synthesis, data scheduling, and RL training.<n>Extensive experiments show that VeriTime substantially boosts LLM performance across diverse time series reasoning tasks.
arXiv Detail & Related papers (2026-02-08T05:42:35Z) - LLM/Agent-as-Data-Analyst: A Survey [54.08761322298559]
Large language models (LLMs) and agent techniques have brought a fundamental shift in the functionality and development paradigm of data analysis tasks.<n>LLMs enable complex data understanding, natural language, semantic analysis functions, and autonomous pipeline orchestration.
arXiv Detail & Related papers (2025-09-28T17:31:38Z) - Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended) [49.46686813437884]
We show that it is possible to compute data-aware optimal alignments in a rich setting with general data types and data conditions.<n>This is achieved by carefully combining the two best-known approaches to deal with control flow and data dependencies.
arXiv Detail & Related papers (2025-06-30T10:16:21Z) - AUCAD: Automated Construction of Alignment Dataset from Log-Related Issues for Enhancing LLM-based Log Generation [19.410504836739058]
This paper explores enhancing the performance of LLM-based solutions for automated log statement generation by post-training with a purpose-built dataset.<n>A novel approach called AUCAD automatically constructs such a dataset with information extracting from log-related issues.<n>Both human and experimental evaluations indicate that these models significantly outperform existing LLM-based solutions.
arXiv Detail & Related papers (2024-12-25T08:43:00Z) - Goal-Driven Reasoning in DatalogMTL with Magic Sets [4.885086628404422]
DatalogMTL is a powerful rule-based language for temporal reasoning.<n>We introduce a new reasoning method for DatalogMTL which exploits the magic sets technique.<n>We show that the proposed approach significantly and consistently outperformed state-of-the-art reasoning techniques.
arXiv Detail & Related papers (2024-12-10T07:40:37Z) - Dynamic Data Pruning for Automatic Speech Recognition [58.95758272440217]
We introduce Dynamic Data Pruning for ASR (DDP-ASR), which offers fine-grained pruning granularities specifically tailored for speech-related datasets.
Our experiments show that DDP-ASR can save up to 1.6x training time with negligible performance loss.
arXiv Detail & Related papers (2024-06-26T14:17:36Z) - Data is all you need: Finetuning LLMs for Chip Design via an Automated design-data augmentation framework [50.02710905062184]
This paper proposes an automated design-data augmentation framework, which generates high-volume and high-quality natural language aligned with Verilog and EDA scripts.
The accuracy of Verilog generation surpasses that of the current state-of-the-art open-source Verilog generation model, increasing from 58.8% to 70.6% with the same benchmark.
arXiv Detail & Related papers (2024-03-17T13:01:03Z) - Seminaive Materialisation in DatalogMTL [10.850687097496373]
DatalogMTL is an extension of Datalog with metric temporal operators.
We propose a materialisation-based procedure to minimise redundant computation.
Our experiments show that our optimised seminaive strategy for DatalogMTL is able to significantly reduce materialisation times.
arXiv Detail & Related papers (2022-08-15T10:04:44Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
This paper studies Linear Temporal Logic over Finite Traces (LTLf)
proposition letters are replaced with first-order formulas interpreted over arbitrary theories.
The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
arXiv Detail & Related papers (2022-04-28T17:57:33Z) - MeTeoR: Practical Reasoning in Datalog with Metric Temporal Operators [12.145849273069627]
We present a novel approach for practical reasoning in DatalogMTL which combines materialisation (a.k.a. forward chaining) with automata-based techniques.
MeTeoR is a scalable system which enables reasoning over complex temporal rules and involving datasets of millions of temporal facts.
arXiv Detail & Related papers (2022-01-12T17:46:18Z) - Query Evaluation in DatalogMTL -- Taming Infinite Query Results [2.9005223064604078]
We study infinite models that eventually become constant and introduce sufficient criteria for programs that allow for such representation.
We provide a novel algorithm for reasoning over finite representable DatalogMTL programs that incorporates all of the previously discussed representations.
arXiv Detail & Related papers (2021-09-21T09:37:28Z) - Self-Supervised Log Parsing [59.04636530383049]
Large-scale software systems generate massive volumes of semi-structured log records.
Existing approaches rely on log-specifics or manual rule extraction.
We propose NuLog that utilizes a self-supervised learning model and formulates the parsing task as masked language modeling.
arXiv Detail & Related papers (2020-03-17T19:25:25Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.