Table of Contents
Fetching ...

Complex event recognition under time constraints: towards a formal framework for efficient query evaluation

Julián García, Cristian Riveros

TL;DR

The paper tackles the problem of Complex Event Recognition under time constraints by formalizing timed CER through timed CEL and timed CEA. It proves that timed CEL and timed CEA have equivalent expressive power, establishing a robust framework for time-aware CER. It then identifies a determinizable fragment—synchronous resets timed CEA that includes swg-queries—and provides a streaming evaluation algorithm with constant update time and output-linear delay for deterministic monotonic single-clock timed CEA. The work lays groundwork for efficient real-time CER under time constraints while outlining open questions on broader determinizable fragments and extensions to more expressive features.

Abstract

This work studies Complex Event Recognition (CER) under time constraints regarding its query language, computational models, and streaming evaluation algorithms. We start by introducing an extension of Complex Event Logic (CEL), called timed CEL, with simple time operators. We show that timed CEL aids in modeling CER query languages in practice, serving as a proxy to study the expressive power of such languages under time constraints. For this purpose, we introduce an automata model for studying timed CEL, called timed Complex Event Automata (timed CEA). This model extends the existing CEA model with clocks, combining CEA and timed automata in a single model. We show that timed CEL and timed CEA are equally expressive, giving the first characterization of CER query languages under time constraints. Then, we move towards understanding the efficient evaluation of timed CEA over streams concerning its determinization and efficient algorithms. We present a class of timed CEA that are closed under determinization; furthermore, we show that this class contains swg-queries, an expressive class of CER queries recently introduced by Kleest-Meissner et al. Finally, we present a streaming evaluation algorithm with constant update time and output-linear delay for evaluating deterministic monotonic timed CEA with a single clock, which have only less equal or greater equal comparisons.

Complex event recognition under time constraints: towards a formal framework for efficient query evaluation

TL;DR

The paper tackles the problem of Complex Event Recognition under time constraints by formalizing timed CER through timed CEL and timed CEA. It proves that timed CEL and timed CEA have equivalent expressive power, establishing a robust framework for time-aware CER. It then identifies a determinizable fragment—synchronous resets timed CEA that includes swg-queries—and provides a streaming evaluation algorithm with constant update time and output-linear delay for deterministic monotonic single-clock timed CEA. The work lays groundwork for efficient real-time CER under time constraints while outlining open questions on broader determinizable fragments and extensions to more expressive features.

Abstract

This work studies Complex Event Recognition (CER) under time constraints regarding its query language, computational models, and streaming evaluation algorithms. We start by introducing an extension of Complex Event Logic (CEL), called timed CEL, with simple time operators. We show that timed CEL aids in modeling CER query languages in practice, serving as a proxy to study the expressive power of such languages under time constraints. For this purpose, we introduce an automata model for studying timed CEL, called timed Complex Event Automata (timed CEA). This model extends the existing CEA model with clocks, combining CEA and timed automata in a single model. We show that timed CEL and timed CEA are equally expressive, giving the first characterization of CER query languages under time constraints. Then, we move towards understanding the efficient evaluation of timed CEA over streams concerning its determinization and efficient algorithms. We present a class of timed CEA that are closed under determinization; furthermore, we show that this class contains swg-queries, an expressive class of CER queries recently introduced by Kleest-Meissner et al. Finally, we present a streaming evaluation algorithm with constant update time and output-linear delay for evaluating deterministic monotonic timed CEA with a single clock, which have only less equal or greater equal comparisons.

Paper Structure

This paper contains 29 sections, 20 theorems, 30 equations, 8 figures.

Key Result

Proposition 4.3

For every timed CEL formula $\varphi$ there exists a timed CEA $\mathcal{T}_\varphi$ such that ${\llbracket{}{\varphi}\rrbracket}(\bar{S}) = {\llbracket{}{\mathcal{T}_\varphi}\rrbracket}(\bar{S})$ for every stream $\bar{S}$.

Figures (8)

  • Figure 1: A timed stream $\bar{S}_{0}$ of temperatures ($T$) and humidities ($H$) with attributes $temp$ (degrees Celcius) and $hum$ (percentage), respectively. The timestamp is the third line, measured in seconds. The fourth line is the index position in the stream.
  • Figure 2: The semantics of CEL formulas defined over a stream $\bar{S} = e_1 e_2 \ldots e_n$ where each $e_i$ is an event.
  • Figure 3: The semantics of time operators of timed CEL for every timed CEL formulas $\varphi, \varphi_1, \varphi_2$, a timed stream $\bar{S} = (e_1, t_1) \ldots (e_n, t_n)$, and $I$ is an interval over $\mathbb{Q}_{\geq 0}$. Here, recall that $t_{{\mathsf{start}}(C)}$ is the timestamp of the event in index ${\mathsf{start}}(C)$.
  • Figure 4: CAECS node representations. In union nodes, the solid arrow represents the left child and the dashed arrow represents the right child.
  • Figure 5: Clock-aware gadget types. The gadget is the $g_1$ corresponds to a void gadget, $g_2$ corresponds to a reset gadget, $g_3$ corresponds to a clock-check gadget, $g_4$ corresponds to an empty gadget, $g_5$ corresponds to a composed gadget. In each gadget version, the entry node is the one pointed by the top-down arrow, and the exit node is the $\eta_i$ below.
  • ...and 3 more figures

Theorems & Definitions (52)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Example 3.1: Continued Example \ref{['ex:cel-query']}
  • Example 3.2
  • Example 4.1
  • Example 4.2
  • Proposition 4.3
  • proof : Proof sketch.
  • Proposition 4.4
  • ...and 42 more