Modular Quantitative Monitoring
Modular Quantitative Monitoring
复制标题
DOI：
10.1145/3290363
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Stanford, Caleb
中科院分区：
文献类型：
--
作者：
Alur, Rajeev;Mamouras, Konstantinos;Stanford, Caleb
在实时决策和运行时监视应用程序中，声明性语言通常被使用，因为它们促进了模块化高级规格，并通过编译器以有效和增量的方式保证对数据流进行评估。我们介绍了数据传感器的模型，以允许在流数据上对查询进行模块化汇编。数据传感器通过使用允许的操作集更新其变量来维护有限的数据变量集，并通过更新其变量来处理一系列标记的数据值。该模型允许明确的非确定性，指数式简洁的控制以及将平行线程的值结合在一起。该模型的语义立即提出了一种有效的评估流算法。数据传感器的表现力与流式的常规传输相吻合，这是一种以MSO可定义的弦线对DAG变换为特征的强大而可流的功能类别，没有向后边缘。我们表明，与先前研究的换能器不同，数据传感器的新功能使它们与处理数据流的传统命令代码一样简洁，但是过渡函数的结构允许模块化编译。特别是，我们表明，可以通过自然和简洁的数据传感器上的自然和简洁的结构来实施诸如平行组成，联合，前缀，前缀，前缀和定量类似物，以进行明确解析。为了说明这种模块化在编译中的好处，我们为定量监视的新语言定义了QR-PAST，该语言整合了过去时间逻辑和定量正则表达式的特征。尽管这种组合允许在QR-Past中对心脏心律失常检测算法进行自然规范，但由于数据传感器上的简洁构造，将QR-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.