Monitoring with STL

Signal temporal logic states how a real-valued signal should behave over time, and a monitor checks a trace against that specification.

Your first monitor

Take a five-sample speed trace and the property that speed always stays above five.

import sentil
from sentil import Formula

trace = sentil.Trace([0, 1, 2, 3, 4], {"speed": [12, 9, 7, 4, 6]})
phi = Formula.parse("G (speed > 5)")
phi.robustness(trace)   # -1.0

use sentil::{Formula, Trace};

let trace = Trace::from_signal([0.0, 1.0, 2.0, 3.0, 4.0], "speed", [12.0, 9.0, 7.0, 4.0, 6.0])?;
let phi = Formula::parse("G (speed > 5)")?;
let rho = phi.robustness(&trace)?;   // -1.0

sentil check -f 'G (speed > 5)' -t speeds.csv

check
  formula     G (speed > 5)
  trace       speeds.csv
  semantics   dense
  verdict     violated
  robustness  -1.000000

Offline and Online

There are two types of deterministic runtime monitoring. Offline monitoring takes a whole recorded trace at once and checks it. Online monitoring feeds the monitor one timed sample at a time as a sensor produces it, and each update returns a verdict without waiting for the trace to end. The robustness values agree between the modes on the same data. The difference is whether you hold the full trace in memory or stream it past the monitor.

Select and use offline runtime monitoring when you have recorded data and you want to do something with it. Go for online monitoring when you monitor a live loop and need a verdict per step within a deadline.

Robustness options

Formula.robustness over a Trace returns one number, the robustness at the earliest time in the trace. It is the offline call for a single verdict.

Formula.robustness_signal over a Trace returns the robustness at every sample, so you can plot how the margin evolves. Formula.violations reports the intervals where that signal is negative.

OnlineMonitor.update takes a timestamp and the current variable values and returns a Robustness carrying whether the verdict has resolved, whether it is satisfied, and the value. This is the streaming surface; the whole-trace Monitor accepts the same fold, and the three-stage pipeline draws the line between the two classes.

from sentil import OnlineMonitor

monitor = OnlineMonitor("G[0, 10](speed > 5)")
for t, speed in enumerate([12, 9, 7, 4, 6]):
    r = monitor.update(float(t), {"speed": float(speed)})
    if r.resolved and not r.satisfied:
        print(f"violated at t={t}, margin {r.value}")

Concepts

How-to guides

When you need the exact syntax, the reference tab has the grammar, with every alias and precedence rule, and the operators with formal semantics and edge cases.