Efficiently computing a distance-based robustness measure for a fragment of Signal Temporal Logic

When verifying real-time, safety-critical systems, it is instructive to know not just whether a property is satisfied or not, but to have a quantitative measure that expresses how safely it is satisfied, or how badly it was failed. When the objects of study are timed signals, specifications are often written in Signal Temporal Logic or STL. In this setting Fainekos and Pappas pioneered a notion known as the robustness of satisfying a formula, which precisely captures this degree of satisfaction or failure. But all subsequent works on robustness for STL move away from this original definition, preferring to compute more easily tractable approximates.

In this talk, we will return to the original notion, and study a robustness measure defined as the exact distance between a signal and the boundary of satisfiability for the STL specification. Moreover, we will see why this can be efficiently computed for interesting STL formulae such as the bounded response property. Based on joint work with Mohammed Foughali and Eugene Asarin.