WEX: Formal Specifications for Windows in Stream Processing
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908657746182144 |
|---|---|
| author | Hitarth, S Praveen, M. |
| author_facet | Hitarth, S Praveen, M. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2209_04244 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | WEX: Formal Specifications for Windows in Stream Processing Hitarth, S Praveen, M. Formal Languages and Automata Theory 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. |
| title | WEX: Formal Specifications for Windows in Stream Processing |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2209.04244 |