Quantitative and Approximate Monitoring

TL;DR

This paper extends runtime verification to include quantitative and approximate monitoring, enabling estimation of numerical trace properties with resource-accuracy trade-offs, and formalizes the framework with trade-offs and resource effects.

Contribution

It introduces a formal framework for quantitative and approximate monitoring, generalizing classical boolean monitoring and analyzing resource-accuracy trade-offs.

Findings

Quantitative monitors can improve estimates with more resources.

Additional registers can enhance monitoring precision.

The framework generalizes classical boolean monitoring to quantitative properties.

Abstract

In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime verification to monitors that attempt to estimate numerical values of quantitative trace properties (instead of attempting to conclude boolean values of trace specifications), such as maximal or average response time along a trace. Quantitative monitors are approximate: with every finite prefix, they can improve their estimate of the infinite trace's unknown property value. Consequently, quantitative monitors can be compared with regard to a precision-cost trade-off: better approximations of the property value require more monitor resources, such as states (in the case of finite-state monitors) or registers, and additional resources yield better approximations. We introduce a formal framework for quantitative and approximate monitoring, show how it conservatively generalizes the classical boolean setting for monitoring, and give several precision-cost trade-offs for monitors. For example, we prove that there are quantitative properties for which every additional register improves monitoring precision.