一句话：提出数据转换器模型以实现流数据查询的模块化编译，并定义 QRE-Past 定量监控语言。
实时决策与运行时监控需要可模块化的声明式流数据查询。论文提出数据转换器（data transducer）模型：维护有限数据变量，按标签数据值更新变量，支持无歧义非确定性、指数级简洁控制和并行值合并，语义直接给出高效流式求值。其表达力等价于可流式正则转换（streamable regular transductions），即无后向边的 MSO 字符串到 DAG 变换；且比已有转换器更简洁，接近命令式代码，并支持并行组合、并、前缀和及无歧义解析组合子等模块化构造。作者据此定义 QRE-Past，融合过去时态逻辑与定量正则表达式，可免费编译为高效监控器。
In real-time decision making and runtime monitoring applications, declarative languages are commonly used as they facilitate modular high-level specifications with the compiler guaranteeing evaluation over data streams in an efficient and incremental manner. We introduce the model of Data Transducers to allow modular compilation of queries over streaming data. A data transducer maintains a finite set of data variables and processes a sequence of tagged data values by updating its variables using an allowed set of operations. The model allows unambiguous nondeterminism, exponentially succinct control, and combining values from parallel threads of computation. The semantics of the model immediately suggests an efficient streaming algorithm for evaluation. The expressiveness of data transducers coincides with streamable regular transductions , a robust and streamable class of functions characterized by MSO-definable string-to-DAG transformations with no backward edges. We show that the novel features of data transducers, unlike previously studied transducers, make them as succinct as traditional imperative code for processing data streams, but the structuring of the transition function permits modular compilation. In particular, we show that operations such as parallel composition, union, prefix-sum, and quantitative analogs of combinators for unambiguous parsing, can be implemented by natural and succinct constructions on data transducers. To illustrate the benefits of such modularity in compilation, we define a new language for quantitative monitoring, QRE-Past, that integrates features of past-time temporal logic and quantitative regular expressions. While this combination allows a natural specification of a cardiac arrhythmia detection algorithm in QRE-Past, compilation of QRE-Past specifications into efficient monitors comes for free thanks to succinct constructions on data transducers.
@article{paperbot693,
title = {Modular quantitative monitoring},
author = {Rajeev Alur and Konstantinos Mamouras and Caleb Stanford},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290363}
}