We study the offline monitoring problem for stream-based specifications of cyber-physical systems. A stream-based monitor translates streams of input data, such as sensor readings, into streams of aggregate statistics and verdicts about the safety of the system. Since physical sensors are prone to measurement noise and errors, it becomes necessary to track the uncertainty in the processing and aggregation steps within the monitor. In previous joint work with Martin Fränzle and Paul Kröger, we proposed RLola, an extension of the stream-based language Lola [8] with slack variables that capture this uncertainty, and an online monitoring algorithm for a fragment of RLola. This paper introduces an offline monitoring algorithm for RLola based on satisfiability modulo theories (SMT). While the online algorithm evaluates boolean trigger conditions one at a time, verifying the existence of a hypothetical ground-truth trace that avoids the trigger condition at the current time step, offline monitoring assumes that the complete system trace is given: the offline algorithm then verifies the existence of a hypothetical ground-truth trace that avoids the trigger conditions across all time-steps. As a result, the offline algorithm can identify trigger violations that the online algorithm fails to detect. We evaluate the algorithm’s precision and running time using an example, comparing it to the existing online monitoring algorithm.
2026-05-11
2026-06-24