Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Bernd Finkbeiner, Martin Fränzle, Florian Kohn, Paul Kröger

TL;DR

The paper addresses bounded-memory runtime monitoring of RLola specifications under sensor calibration and measurement noise. It combines symbolic semantics to represent the infinite slack-variable space with zonotopes as a bounded-memory over-approximation domain, enabling sound monitoring independent of trace length. The authors formalize the symbolic evaluation, introduce zonotope-based state pruning, and compare several over-approximation strategies, showing that the choice of method materially affects precision and false positives. This approach provides a practical, scalable framework for robust online monitoring of safety-critical systems under uncertainty, with implications for both design-time specifications and runtime verification tools.

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 RLola specifications. We demonstrate that zonotopes precisely capture the affine state of the monitor and that their over-approximation produces a sound bounded-memory monitor. We present a comparison of different zonotope over-approximation strategies in the context of runtime monitoring, evaluating their performance and false-positive rates.

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

TL;DR

The paper addresses bounded-memory runtime monitoring of RLola specifications under sensor calibration and measurement noise. It combines symbolic semantics to represent the infinite slack-variable space with zonotopes as a bounded-memory over-approximation domain, enabling sound monitoring independent of trace length. The authors formalize the symbolic evaluation, introduce zonotope-based state pruning, and compare several over-approximation strategies, showing that the choice of method materially affects precision and false positives. This approach provides a practical, scalable framework for robust online monitoring of safety-critical systems under uncertainty, with implications for both design-time specifications and runtime verification tools.

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 RLola specifications. We demonstrate that zonotopes precisely capture the affine state of the monitor and that their over-approximation produces a sound bounded-memory monitor. We present a comparison of different zonotope over-approximation strategies in the context of runtime monitoring, evaluating their performance and false-positive rates.
Paper Structure (18 sections, 2 theorems, 16 equations, 5 figures, 1 table)

This paper contains 18 sections, 2 theorems, 16 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. The Challenge.
  4. Related Work
  5. Preliminaries
  6. RLola
  7. Trigger Conditions in RLola.
  8. Error Model
  9. Approximate Online Monitoring of RLola
  10. Symbolic Semantics
  11. Symbolic Algorithm
  12. Symbolic Evaluation Algorithm.
  13. Zonotope Approximation
  14. Evaluation
  15. Omnidirectional movement.
  16. ...and 3 more sections

Key Result

lemma \@thmcounterlemma

$\forall {\rho_{\textit{in}}}. \lvert \widehat{\llbracket S \rrbracket}_{\rho_{\textit{in}}} \rvert = \llbracket S \rrbracket_{\rho_{\textit{in}}}$

Figures (5)

  • Figure 1: An industrial robot that can move in the two dimensions of a plane.
  • Figure 2: A plot of the zonotope spanned by the monitor state at time 4s.
  • Figure 3: The approximation error for the robotic system example from \ref{['sec:motivation']}.
  • Figure 4: The error around the $x$ position and the false-positive rates for \ref{['spec:free_robot']}.
  • Figure 5: Average approximation error for the example in \ref{['spec:free_robot']}.

Theorems & Definitions (7)

  • definition \@thmcounterdefinition: RLola Syntax
  • definition \@thmcounterdefinition: Semantics of Stream Expressions
  • definition \@thmcounterdefinition: Semantics of Specifications
  • definition \@thmcounterdefinition: Consistency
  • definition \@thmcounterdefinition: Symbolic Semantics of Specifications
  • lemma \@thmcounterlemma: Symbolic Correctness
  • theorem \@thmcountertheorem: Correctness