Reference. A General Framework for Robust Quantitative Semantics of Signal Temporal Logic
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.
Cite
Cites 36 works (1 here)
With notes (1)
Work-in-Progress: Towards a Theory of Robust Quantitative Semantics for Signal Temporal Logic jeannin-2022-work
External (35)
- Mixed Integer Linear Programming Approach for Control Synthesis with Weighted Signal Temporal Logic (2023)
- Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods (2022)
- A Compositional Framework for Quantitative Online Monitoring over Continuous-Time Signals (2021)
- Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis (2021)
- Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness (2021)
- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring (2021)
- A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics (2020)
- Evaluating Optimization Solvers and Robust Semantics for Simulation-Based Falsification (2020)
- A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control (2020)
- Enhancing Temporal Logic Falsification With Specification Transformation and Valued Booleans (2020)
- ARCH-COMP 2019 Category Report: Falsification (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)
- Robust control for signal temporal logic specifications using discrete average space robustness (2019)
- Arithmetic-Geometric Mean Robustness for Control from Signal Temporal Logic Specifications (2019)
- Average-based Robustness for Continuous-Time Signal Temporal Logic (2019)
- Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications (2018)
- Using Valued Booleans to Find Simpler Counterexamples in Random Testing of Cyber-Physical Systems (2018)
- Benchmarks for Temporal Logic Requirements for Automotive Systems (2018)
- An Algebraic Framework for Runtime Verification (2018)
- Monitoring mobile and spatially distributed cyber-physical systems (2017)
- Smooth operator: Control using the smooth robustness of temporal logic (2017)
- Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
- Functional gradient descent method for Metric Temporal Logic specifications (2014)
- Powertrain control verification benchmark (2014)
- Probabilistic Temporal Logic Falsification of Cyber-Physical Systems (2013)
- Falsification of temporal properties of hybrid systems using the cross-entropy method (2012)
- S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems (2011)
- Robust Satisfaction of Temporal Logic over Real-Valued Signals (2010)
- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems (2010)
- Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems (2010)
- Robustness of temporal logic specifications for continuous-time signals (2009)
- Model Checking Quantitative Linear Time Logic (2008)
- Monitoring Temporal Properties of Continuous Signals (2004)
- Specifying real-time properties with metric temporal logic (1990)