Robust Satisfaction of Temporal Logic over Real-Valued Signals

2 min read

Donzé and Maler give Signal Temporal Logic (STL) a real-valued semantics, so a monitor reports how far a trajectory is from satisfying or violating a formula as well as a yes or no. Atomic predicates are inequalities f(x) ≥ 0 over continuous signals; negation flips the sign, conjunction takes the minimum, and the timed until takes a max over a window of mins. They define space robustness, a new time robustness (how far events can shift in time before the verdict changes) and a combined space-time measure, give an algorithm for piecewise-linear signals, and compute the sensitivity of robustness to system parameters.

Findings

  • Soundness: the sign of the space robustness equals the Boolean verdict. If the robustness is r, every signal whose predicate values stay within r of the original gets the same verdict, so r is a noise margin.
  • Conjunction can be computed in time linear in the number of signal samples. For the until operator they conjecture a bound of (number of samples) times (samples inside the time window), and report better behaviour in practice.
  • In their comparison, TaLiRo (the only other robustness tool at the time) scaled linearly with signal length but, in some cases, exponentially with formula size. Their algorithm behaved as their analysis predicted on the same data.
  • Robustness sensitivity to parameters lets simulation-based verification steer towards parameter values that break a property.

Limits

  • Robustness is measured on the predicate values the specification names, not on the raw state. Two formulae that mean the same thing can give different margins.
  • The algorithm works offline on complete, piecewise-linear simulated traces. Running it online on a robot needs bounded horizons, which the paper does not cover.
  • The authors expect applications in switching circuits and biochemical pathways. Robots are not discussed.

Relevance

STL robustness is now the common currency for robot monitors that need a margin (“how close to the geofence”), for falsification, and for control barrier style objectives. A monitor that reports margins can warn before a violation, which helps failure recovery. It builds on temporal logic and timed models; see runtime monitoring and safe control.