Reference. Work-in-Progress: Towards a Theory of Robust Quantitative Semantics for Signal Temporal Logic
Cite
Cited by (1)
A General Framework for Robust Quantitative Semantics of Signal Temporal Logic chen-2026-a
Quantitative semantics of Signal Temporal Logic (STL) play an important role in both the falsification and control synthesis for dynamical systems by assigning numerical quantities to truth values. Recently, several different quantitative semantics have been proposed, offering better performance in many cases. Yet a general, systematic understanding of the structure and properties of quantitative semantics is missing. In this paper, we develop a general framework to model quantitative semantics. We focus mainly on soundness, which requires that the quantitative semantics of a statement is positive when the statement is true, and negative when the statement is false. This ensures that counterexamples will not be missed during verification. We derive simple, necessary conditions in our framework for soundness. We show how several recently proposed quantitative semantics fit in our framework, and how others do not, typically because they do not strictly satisfy soundness. We implement various quantitative semantics, including existing semantics from literature, in our framework and compare their effectiveness as objective functions for optimization-based falsification on both novel and existing benchmarks.
Cites 18 works (0 here)
External (18)
- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring (2021)
- A Compositional Framework for Quantitative Online Monitoring over Continuous-Time Signals (2021)
- A smooth robustness measure of signal temporal logic for symbolic control (2020)
- Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications (2019)
- Robust control for signal temporal logic specifications using discrete average space robustness (2019)
- Control from Signal Temporal Logic Specifications with Smooth Cumulative Quantitative Semantics (2019)
- TeLEx: learning signal temporal logic from positive examples using tightness metric (2019)
- Quantitative monitoring of STL with edit distance (2018)
- An algebraic framework for runtime verification (2018)
- Using Valued Booleans to Find Simpler Counterexamples in Random Testing of Cyber-Physical Systems (2018)
- Smooth operator: Control using the smooth robustness of temporal logic (2017)
- Objective functions for falsification of signal temporal logic properties in cyberphysical systems (2017)
- Temporal Logic as Filtering (2016)
- Benchmarks for Temporal Logic Requirements for Automotive Systems (2015)
- Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems (2010)
- Robust Satisfaction of Temporal Logic over Real-Valued Signals (2010)
- Robustness of temporal logic specifications for continuous-time signals (2009)