Robust Runtime Monitoring with Slack Variables
Bernd Finkbeiner, Martin Fränzle, Florian Kohn, and Paul Kröger
Stream-based monitoring is a runtime assurance technique for cyber-physical systems, where monitors are synthesized from formal specifications. These monitors evaluate system behavior during execution, typically using data from physical sensors. However, sensor measurements are subject to noise and calibration errors, introducing uncertainty in the monitored data. Robustness is the hyperproperty that requires that small variations in the input – such as those caused by sensor noise – result in only small variations in the monitor’s verdicts. In this talk, we present methods for constructing robust monitors using symbolic slack variables and affine arithmetic, and discuss the practical and theoretical challenges involved.
4th Workshop on Hyperproperties: Advances in Theory and Applications (Hyper 2025).