Cutting Corners on Uncertainty: Zonotope Abstractions for Stream-based Runtime Monitoring

Abstract

Stream-based monitoring assesses the health of safety-critical systems by transforming input streams of sensor measurements into output streams that determine a verdict. These inputs are often treated as accurate representations of the physical state, although real sensors introduce calibration and measurement errors. Such errors propagate through the monitor's computations and can distort the final verdict. Affine arithmetic with symbolic slack variables can track these errors precisely, but independent measurement noise introduces a fresh slack variable upon each measurement event, causing the monitor's state representation to grow without bound over time. Therefore, any bounded-memory monitoring algorithm must unify slack variables at runtime in a way that generates a sound approximation. This paper introduces zonotopes as an abstract domain for online monitoring of general Robust-Lola (RLola) specifications. We demonstrate that zonotopes precisely capture uncertainty in the monitor's state and that their over-approximation produces a sound, bounded-memory monitor. We present a comparison of different zonotope over-approximation strategies for runtime monitoring, evaluating their performance and false-positive rates. Finally, we implement the most effective strategy in RLola and demonstrate improvements in both precision and runtime compared to existing approaches based on realistic benchmarks.