A compositional framework for algebraic quantitative online monitoring over continuous-time signals
A compositional framework for algebraic quantitative online monitoring over continuous-time signals
复制标题
连续时间信号代数定量在线监测的组合框架
DOI：
10.1007/s10009-023-00719-w
复制
发表时间：
2023
影响因子：
1.5
通讯作者：
Wang, Zhifu
中科院分区：
文献类型：
--
作者：
Mamouras, Konstantinos;Chattopadhyay, Agnishom;Wang, Zhifu
研究了密集时间和连续时间信号的度量时序逻辑(MTL)性质的在线监测算法。我们考虑一种基于完备格的抽象代数语义。这种语义包括作为特殊情况的标准布尔(定性)语义和广泛使用的实值健壮性(定量)语义。我们的语义还扩展到部分排序的真值，并允许对满意度中的不确定性进行建模。我们提出了一种构造在线监视器的合成方法，该方法转换分段恒定(密集时间和连续时间)信号的精确表示。这些监测器基于一类无限状态的确定性信号换能器，它(1)允许产生相对于输入信号具有某种有界延迟的输出信号，(2)不会在输出信号中引入无界变异性。我们的监测框架的一个关键组成部分是密集时间信号上的高效滑动窗口聚集算法。我们已经实现了我们的监控框架，并通过与最近提出的在线监控工具Reelay和RTAMT进行比较，对其进行了实验评估。
We investigate online monitoring algorithms over dense-time and continuous-time signals for properties written in metric temporal logic (MTL). We consider an abstract algebraic semantics based on complete lattices. This semantics includes as particular cases the standard Boolean (qualitative) semantics and the widely used real-valued robustness (quantitative) semantics. Our semantics also extends to truth values that are partially ordered and allows the modeling of uncertainty in satisfaction. We propose a compositional approach for the construction of online monitors that transform exact representations of piecewise constant (dense-time and continuous-time) signals. These monitors are based on a class of infinite-state deterministic signal transducers that (1) are allowed to produce the output signal with some bounded delay relative to the input signal, and (2) do not introduce unbounded variability in the output signal. A key ingredient of our monitoring framework is an efficient algorithm for sliding-window aggregation over dense-time signals. We have implemented and experimentally evaluated our monitoring framework by comparing it to the recently proposed online monitoring tools Reelay and RTAMT.
登录
查看更多内容
DOI：
10.1109/tcad.2018.2858460
发表时间：
2018-11-01
影响因子：
2.9
作者：
Jaksic, Stefan;Bartocci, Ezio;Nickovic, Dejan
通讯作者：
Nickovic, Dejan
具有有限滞后的在线信号监控
DOI：
10.1109/tcad.2020.3013053
发表时间：
2020
影响因子：
2.9
作者：
Mamouras, Konstantinos;Wang, Zhifu
通讯作者：
Wang, Zhifu
影响因子：
2.5
作者：
Alur, R;Feder, T;Henzinger, TA
通讯作者：
Henzinger, TA
影响因子：
2.5
作者：
Bonakdarpour, Borzoo;Fraigniaud, Pierre;Rajsbaum, Sergio;Rosenblueth, David;Travers, Corentin
通讯作者：
Travers, Corentin
StreamQRE：流数据定量查询的模块化规范和高效评估
DOI：
10.1145/3062341.3062369
发表时间：
2017
期刊：
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Mamouras, Konstantinos;Raghothaman, Mukund;Alur, Rajeev;Ives, Zachary G.;Khanna, Sanjeev
通讯作者：
Khanna, Sanjeev