Robust Lola — Artifact

This artifact accompanies the paper on robust runtime monitoring with RLola. It contains the RTLola interpreter and CLI with support for zonotope-based slack variable tracking, Python bindings for the interpreter, and the evaluation notebooks that reproduce the results from the paper.

Repository structure

Robust-Lola/
├── RTLola-Frontend/        RTLola parser and HIR
├── rtlola-interpreter/     RTLola interpreter and CLI
├── rlolapythonbinding/     Python bindings (PyO3 / maturin)
├── evaluation/             Benchmarks, traces, and Jupyter notebooks
├── INSTALL.md              Build and installation instructions
└── LICENSE

Installation

See INSTALL.md for prerequisites and build instructions for the CLI and Python bindings.

Usage

The rtlola-cli provides three main commands: monitor, smt, and analyze.

Monitoring a specification

Run a specification against a CSV trace in offline mode:

rtlola-cli monitor --csv-in trace.csv --offline relative spec.lola

Key options:

Option	Description
--csv-in <FILE> / --stdin	Input source (CSV file or standard input)
--online / --offline <FMT>	Online uses wall-clock time; offline reads timestamps from the input. Formats: relative, relative-nanos, offset, absolute, absolute-rfc3339
-v, --verbosity <LEVEL>	Output detail: silent, violations, warnings, public (default), outputs, streams, debug
-s, --statistics <LEVEL>	Compute statistics: none (default), runtime, all
--output-format <FMT>	Output as logger (default), json, or csv
-z, --zonotope-transform <METHOD>	Zonotope reduction method (see below)
--bound <N>	Bound on the number of slack variables kept after reduction
--intervals	Print affine values as intervals instead of symbolic form

Zonotope reduction methods

The --zonotope-transform flag selects how affine equations in the monitor's memory are approximated:

Method	Description
none (default)	Keep affine equations as-is
interval	Approximate by the interval after each cycle
box	Approximate by the interval hull
colinear	Combine colinear generators (lossless)
colinear-scale	Combine most colinear generators, scale the rest
girard	Girard (2005)
scott	Scott et al. — constrained zonotopes
pca	Kopetzki et al. (CDC 2017) — PCA-based
clustering	Kopetzki et al. (CDC 2017) — clustering-based
clustering-rand	Clustering with random generator selection
clustering-diverse	Clustering with directionally diverse selection
combastel	Combastel (ECC 2003)
althoff-a	Althoff (2010) — Method A

Example with Girard reduction keeping at most 10 slack variables:

rtlola-cli monitor --csv-in trace.csv --offline relative \
    --zonotope-transform girard --bound 10 --intervals spec.lola

SMT-based analysis

Encode a specification and trace as an SMT query to check for trigger violations or compute permissible value ranges:

rtlola-cli smt --csv-in trace.csv spec.lola
rtlola-cli smt --csv-in trace.csv --optimize stream_name spec.lola

Option	Description
--optimize <STREAM>	Compute the permissible value range of the given stream
--optimize-output <FILE>	Write optimization results to a CSV file
--input-limit <N>	Limit the input trace to the first N events
--save-encoding <FILE>	Write the SMT-LIB2 constraint system to a file

Static analysis

Parse and type-check a specification without running it:

rtlola-cli analyze spec.lola

Benchmarks

The evaluation/ directory contains four case studies. Each has a dedicated Jupyter notebook, RTLola specifications in evaluation/specs/, and input traces in evaluation/traces/.

Discrete Robot

The running example from the paper. This specification lies in the fragment of RLola for which exact bounded memory monitors exist. Because the monitors are exact, the benchmark evaluates the benefit of slack variables compared to classical approaches such as interval-based logics.

Notebook: evaluation/discrete_robot.ipynb

Bump Robot

A more realistic robotics system that estimates its position from smoothed velocity measurements in two coordinates. Exponential smoothing of the measurements leads to an uneven decay of slack variables, which places the specification outside the exact fragment. The benchmark shows that monitoring states can still be effectively approximated.

Notebook: evaluation/bumper_robot.ipynb

Omnidirectional Robot

A stress test for the zonotope reduction methods. The robot estimates its position from acceleration and direction measurements, which creates a non-trivial coupling of measurement noise in the x and y coordinate streams. The resulting monitor memory corresponds to genuinely hard-to-approximate zonotopes.

Notebook: evaluation/omni_robot.ipynb

Real Driving Emissions

A monitor deployed to detect carbon monoxide emissions of a vehicle driving under realistic conditions. This benchmark demonstrates the expressivity of the language — it features a sensor noise model different from the robot examples and conditional statements over uncertain values. It also provides a direct comparison with UnaaLola, which was evaluated on the same benchmark.

Notebook: evaluation/rde.ipynb

Running the evaluation

See evaluation/README.md for detailed instructions on setting up the Python environment and running the notebooks.

License

This project is licensed under the Apache License 2.0 — see LICENSE for details.