提出增量推理算法,让时间逻辑推理更快响应数据更新。
Incremental Maintenance of DatalogMTL Materialisations
- 基于经典DRed算法,设计新操作符处理周期性时间事实
- 实验显示比重算快数倍,部分场景快上百倍
- 适合频繁更新的实时时序数据系统
DatalogMTL在经典Datalog语言中引入度量时序逻辑(MTL),支持对时序数据的丰富推理。现有基于物化和自动机的方法虽具完备性和正确性,但无法高效处理动态更新,而这正是真实应用场景的关键需求。本文提出DRedMTL,一种针对有界区间的时间逻辑推理增量算法。与仅包含有限事实的Datalog物化不同,DatalogMTL物化需以有限事实加周期区间表示,通过展开构建完整结果。为此,算法设计专用操作符,高效处理此类周期性表示。我们实现了该方法并在多个公开数据集上测试,结果表明DRedMTL通常显著优于重算,部分情况下提速达数量级。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。