Average-based Robustness for Continuous-Time Signal Temporal Logic
This work addresses robustness evaluation in formal verification for systems with complex dynamics, though it appears incremental as it builds on existing STL frameworks.
The authors tackled the problem of evaluating robustness for continuous-time Signal Temporal Logic specifications by proposing a new average-based robustness score that considers the entire signal evolution rather than just the most severe point, and demonstrated its advantages in falsification and control synthesis for complex and multi-agent systems.
We propose a new robustness score for continuous-time Signal Temporal Logic (STL) specifications. Instead of considering only the most severe point along the evolution of the signal, we use average scores to extract more information from the signal, emphasizing robust satisfaction of all the specifications' subformulae over their entire time interval domains. We demonstrate the advantages of this new score in falsification and control synthesis problems in systems with complex dynamics and multi-agent systems.