WEX: Formal Specifications for Windows in Stream Processing

TL;DR

This paper introduces WEX, a formal logic-based language for precisely specifying windowing operations in stream processing, enabling advanced analysis and supporting complex window definitions beyond traditional methods.

Contribution

WEX provides a formal, logic-based framework for defining and analyzing windowing in stream processing, including complex and custom window types, with decidability results for certain cases.

Findings

WEX can express traditional and complex windowing constructs.

Decidability of window analysis depends on alphabet properties.

Formal semantics enable static analysis of windowing logic.

Abstract

A key operation in processing an unbounded data stream is windowing, which extracts finite portions of streams for further handling. The existing frameworks and query languages either require windows to be defined using ad hoc imperative languages or are limited to rudimentary constructs such as time- or count-based windows. We propose Window EXpression, a formal specification for precisely expressing windowing constructs based on monadic second-order logic. WEX can naturally express traditional windowing constructs such as sliding windows and tumbling windows, as well as more complex windows whose start and end indices are triggered based on the satisfaction of given logical conditions. After introducing a model of symbolic automata with lookbacks over an alphabet theory, we present another equivalent representation of WEX based on symbolic regular expressions. The precise semantics of windowing enable static analysis over WEX. In particular, we show that, in general, it is undecidable to check whether a WEX allows an unbounded number of overlapping windows. However, when the data stream is over a finite alphabet, or the alphabet theory has the so-called completion property, the problem becomes decidable.