Probabilistic monitoring

A deterministic monitor evaluates the trace you give it, but the trace is a set of observations, and observations carry noise. Most real-world systems are stochastic, and their behavior can vary even under identical inputs. Probabilistic Signal Temporal Logic makes that uncertainty part of the specification with one operator, P~p(phi), which asks whether the inner formula holds with probability at least, or at most, p over the distribution of trajectories the readings could have come from. What PrSTL adds develops the operator.

The three stages

A probabilistic check goes through three stages. First, stochastic signal lifting turns the recorded trace into an ensemble. You attach a noise model to each signal, and the lifter draws realizations of the true trajectory consistent with the reading. Robustness evaluation runs the deterministic engine on every realization, producing one robustness value per sampled trajectory. Statistical aggregation counts how many of those trajectories satisfy the inner formula, estimates the satisfaction probability, and builds a confidence interval around the estimate so the verdict carries its own uncertainty.

A first probabilistic check

The same five-sample speed trace from the monitoring section, now checked under Gaussian sensor noise with standard deviation 0.3.

import sentil
from sentil import Formula, LiftingRegistry, NoiseModel

trace = sentil.Trace([0, 1, 2, 3, 4], {"speed": [12, 9, 7, 4, 6]})

lifting = LiftingRegistry()
lifting.register("speed", NoiseModel.gaussian(0.0, 0.3))

phi = Formula.parse("P>=0.9 (G (speed > 5))")
result = phi.check(trace, lifting)

print(result.probability, result.holds)
print(result.interval.lower, result.interval.upper)

use sentil::{LiftingRegistry, Monitor, MonitorConfig, NoiseInteraction, NoiseModel, Trace};

let mut trace = Trace::new([0.0, 1.0, 2.0, 3.0, 4.0])?;
trace.add_signal("speed", [12.0, 9.0, 7.0, 4.0, 6.0])?;

let mut lifting = LiftingRegistry::new();
lifting.register("speed", NoiseModel::gaussian(0.0, 0.3)?, NoiseInteraction::Additive);

let monitor = Monitor::new("P>=0.9 (G (speed > 5))", MonitorConfig::new())?;
let result = monitor.check(&trace, &lifting)?;

println!("{} {}", result.probability, result.holds);

sentil smc -f 'P>=0.9(G (speed > 5))' -t speeds.csv --noise 'speed=gaussian:0,0.3'

The deterministic robustness at the dip to four was exactly -1.0. Under noise of width 0.3 that dip rarely recovers above five, so the estimated probability that G (speed > 5) holds comes back low and the verdict fails.

check returns an SmcResult object which includes the ff fields; the estimated probability, the confidence interval around it, the raw counts, and a holds verdict against the operator's threshold. Lift a trace into an ensemble explains what the estimate is and for how valid the estimated probability is, see confidence intervals.

Concepts

How to