Efficient Temporal Datalog Materialisation for Composite Event Recognition

Periklis Mantenoglou

arxiv: 2605.02488 · v2 · pith:C3SLCKBInew · submitted 2026-05-04 · 💻 cs.AI · cs.DB· cs.LO

Efficient Temporal Datalog Materialisation for Composite Event Recognition

Periklis Mantenoglou This is my paper

Pith reviewed 2026-05-08 18:31 UTC · model grok-4.3

classification 💻 cs.AI cs.DBcs.LO

keywords composite event recognitiontemporal datalogstream reasoningevent specification languagesmaterialisationtrigger graphstemporal patterns

0 comments

The pith

Mapping fragments of event languages to Temporal Datalog enables one uniform engine for composite event recognition in streams.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper seeks to unify composite event recognition by translating practical fragments of different event specification languages into Temporal Datalog with stratified negation and no future dependencies. This addresses the current isolation of languages and their reasoners, which hinders direct comparisons of what they can express and limits reuse of evaluation technology. The key addition is Streaming Trigger Graphs, an adaptation of Datalog materialisation that processes incoming event streams efficiently while preserving correctness. A reader would care because it offers a path to a shared, scalable mechanism for timely detection of complex situations like safety threats across applications that now rely on separate tools.

Core claim

Practical fragments of prominent event specification languages can be mapped into Temporal Datalog->-, and Streaming Trigger Graphs extend Datalog materialisation to support efficient evaluation over streams of symbolic events, producing a uniform recognition mechanism that has the potential to generalise across a wide range of languages.

What carries the argument

Streaming Trigger Graphs, an extension of Datalog materialisation techniques that maintains correctness and efficiency gains when evaluating Temporal Datalog->- over streaming data with no future dependencies.

If this is right

Multiple event languages can share a single recognition engine instead of requiring separate implementations.
Expressivity comparisons between languages become direct through their common mappings.
Timely detection of composite events remains feasible even on high-velocity symbolic streams.
Optimisations developed for Datalog materialisation can be reused for event recognition tasks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The common mapping may expose which temporal features in existing languages are redundant or interchangeable.
The technique could be tested on live streams from domains like IoT monitoring to check whether efficiency holds beyond the evaluated cases.
If the mappings scale, it suggests a route toward standardised event-processing platforms that accept input in several specification styles.

Load-bearing premise

That fragments of event specification languages can be mapped to Temporal Datalog->- while keeping their original meaning and that Streaming Trigger Graphs continue to deliver both correctness and efficiency on real streaming inputs.

What would settle it

A concrete pattern from one of the source languages that has no equivalent in Temporal Datalog->- without changing its semantics, or a test stream where the trigger-graph method produces different recognition results than the original language-specific reasoner.

Figures

Figures reproduced from arXiv: 2605.02488 by Periklis Mantenoglou.

**Figure 1.** Figure 1: STG for Example 7 up to t = 4 . For each node v, blue (resp. vermillion) coloured labels mark time(v) (the “forget time” of v). ing to the time-point in b − i (lines 12–15). The second difference is that we rely on node consistency—instead of kcompatibility—for rules where all body conditions refer to a previous stratum, i.e., their predicate is not in B j t or their time-point is earlier than the curren… view at source ↗

read the original abstract

Several applications demand the timely detection of critical situations, such as threats to safety and transparency, over high-velocity streams of symbolic events. This demand has motivated the development of (i) event specification languages, which define composite events via temporal patterns over simpler events, and (ii) stream reasoning frameworks, evaluating patterns expressed in these languages. However, event specification languages are typically studied in isolation, complicating their comparison in terms of expressivity and obscuring the scope of their associated stream reasoners. To mitigate this issue, we map practical fragments of prominent event specification languages into Temporal Datalog->-, a temporal Datalog with stratified negation and no future dependencies. To support efficient stream reasoning over Temporal Datalog->-, we propose Streaming Trigger Graphs, an extension of a state-of-the-art technique for Datalog materialisation. Our approach yields a uniform composite event recognition mechanism that has the potential to generalise across a wide range of practical event specification languages.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper maps practical fragments of prominent event specification languages to Temporal Datalog->- (a temporal Datalog variant with stratified negation and no future dependencies) and introduces Streaming Trigger Graphs as an extension of existing Datalog materialisation techniques to support efficient evaluation over high-velocity event streams. It claims this yields a uniform composite event recognition mechanism with potential to generalise across a wide range of event specification languages.

Significance. If the semantic mappings are shown to be faithful and the Streaming Trigger Graphs are proven correct and efficient on unbounded streams, the work would provide a valuable unifying framework for comparing and implementing composite event recognition systems, reducing fragmentation in the field and enabling reuse of optimised Datalog engines for temporal pattern matching in safety-critical streaming applications.

major comments (2)

[Abstract and mapping description] The uniformity and generalisation claim rests on the existence of semantics-preserving translations from event languages (including temporal patterns, negation, and ordering) into Temporal Datalog->-. No formal statement of these mappings, nor any theorem establishing equivalence of the composite-event semantics, appears in the abstract or is referenced in the provided text; without such a result the central claim cannot be evaluated.
[Streaming Trigger Graphs section] Streaming Trigger Graphs are presented as the key extension for streaming materialisation, yet the manuscript supplies no proof or argument that they preserve correctness under streaming semantics (e.g., handling of overlapping intervals or absence of future references) while delivering the claimed efficiency gains. This is load-bearing for the efficiency and correctness assertions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thoughtful and constructive report. The two major comments highlight important points about the clarity and completeness of our formal claims. We address each below and will revise the manuscript accordingly to make the central results more accessible and rigorously presented.

read point-by-point responses

Referee: [Abstract and mapping description] The uniformity and generalisation claim rests on the existence of semantics-preserving translations from event languages (including temporal patterns, negation, and ordering) into Temporal Datalog->-. No formal statement of these mappings, nor any theorem establishing equivalence of the composite-event semantics, appears in the abstract or is referenced in the provided text; without such a result the central claim cannot be evaluated.

Authors: The referee is correct that the abstract does not reference the formal mappings or equivalence theorems. These are defined and proven in the full manuscript (Section 3 defines the translations for each practical fragment of the event languages, including handling of temporal patterns, negation and ordering; Theorems 3.1 and 3.2 establish semantics preservation and equivalence of composite-event recognition). We will revise the abstract to explicitly cite these results (e.g., adding 'as formalised in Theorems 3.1–3.2') so that the uniformity claim can be evaluated directly from the abstract. revision: yes
Referee: [Streaming Trigger Graphs section] Streaming Trigger Graphs are presented as the key extension for streaming materialisation, yet the manuscript supplies no proof or argument that they preserve correctness under streaming semantics (e.g., handling of overlapping intervals or absence of future references) while delivering the claimed efficiency gains. This is load-bearing for the efficiency and correctness assertions.

Authors: We agree that a self-contained correctness argument for Streaming Trigger Graphs under streaming semantics is essential. The manuscript currently provides an informal argument in Section 5 that relies on the no-future-dependency property of Temporal Datalog->- and the ordered processing of events to handle overlapping intervals. However, we acknowledge that this falls short of a full proof. We will add a dedicated subsection (and appendix) containing a formal correctness proof that explicitly addresses streaming semantics, interval overlap, and the absence of future references, together with a clearer link to the measured efficiency gains. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper defines mappings from fragments of event specification languages into Temporal Datalog->- and extends prior Datalog materialisation with Streaming Trigger Graphs. These are presented as new constructions whose correctness and efficiency are argued from the definitions themselves rather than by reducing any claim to a fitted parameter, self-referential definition, or unverified self-citation chain. No equation or central result is shown to be equivalent to its inputs by construction. The uniformity/generalisation claim rests on the proposed mappings and algorithm, which remain independent of the target results they are intended to support.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the assumption that mappings from event languages preserve semantics and that the new graph technique works correctly for streaming data; these are not independently evidenced in the abstract.

axioms (2)

standard math Semantics of Temporal Datalog with stratified negation and no future dependencies
Invoked as the target language for all mappings.
domain assumption Trigger graphs are a correct and efficient materialisation technique for (non-temporal) Datalog
Extended in the paper; treated as established background.

invented entities (1)

Streaming Trigger Graphs no independent evidence
purpose: Extension of trigger graphs to support efficient materialisation over temporal Datalog in streaming settings
New technique introduced to achieve the uniform recognition mechanism.

pith-pipeline@v0.9.0 · 5456 in / 1266 out tokens · 86626 ms · 2026-05-08T18:31:52.665245+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith.Foundation.Atomicity atomic_tick / exists_sequential_schedule echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

Atomic tick (finite history): any finite recognition history admits a serialization with exactly one posting per tick that respects precedence (RS Foundation/Atomicity.lean, theorem atomic_tick).

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.