Staying on Spec: Real-Time Monitoring under Uncertainty with a Maritime Case Study

What the math gives to ML

The paper's transferable asset is its separation between uncertain future behavior and specification evaluation: instead of scoring one predicted trajectory, it computes lower and upper robustness over a reachable set. This gives a neural predictor or policy an explicit safety interval, allowing detection when some plausible future violates a specification even if the mean prediction is safe. A practical adaptation is to train a trajectory predictor or controller with a differentiable surrogate of worst-case temporal-logic robustness, using scenario-generated future particles as an empirical reachable tube. The approach is promising for learned robotics policies and world models where uncertainty calibration matters more than average prediction error.