A compositional framework for algebraic quantitative online monitoring over continuous-time signals

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.