Robustness of temporal logic specifications for continuous-time signals

DOI10.1016/j.tcs.2009.06.021zbMath1186.68287OpenAlexW2049399166WikidataQ57581866 ScholiaQ57581866MaRDI QIDQ732015

George J. Pappas, Georgios E. Fainekos

Publication date: 9 October 2009

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2009.06.021

zbMATH Keywords

robustnessmetric spacestestinglinear and metric temporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (49)

Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability ⋮ Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness ⋮ Crossing the Bridge between Similar Games ⋮ Model measuring for discrete and hybrid systems ⋮ An automated system repair framework with signal temporal logic ⋮ Finite abstractions with robustness margins for temporal logic-based control synthesis ⋮ Robust online monitoring of signal temporal logic ⋮ Quantitative monitoring of STL with edit distance ⋮ Least-violating symbolic controller synthesis for safety, reachability and attractivity specifications ⋮ Linear temporal logic for hybrid dynamical systems: characterizations and sufficient conditions ⋮ Robust, expressive, and quantitative linear temporal logics: pick any two for free ⋮ Extracting counterexamples induced by safety violation in linear hybrid systems ⋮ Specifiable robustness in reactive synthesis ⋮ From LTL to rLTL monitoring: improved monitorability through robust semantics ⋮ A few lessons learned in reinforcement learning for quadcopter attitude control ⋮ Multi-Requirement Testing Using Focused Falsification ⋮ Linear Time Monitoring for One Variable TPTL ⋮ Temporal Robustness of Stochastic Signals ⋮ Elliptical Slice Sampling for Probabilistic Verification of Stochastic Systems with Signal Temporal Logic Specifications ⋮ A framework to measure the robustness of programs in the unpredictable environment ⋮ Model predictive monitoring of dynamical systems for signal temporal logic specifications ⋮ Temporal logic explanations for dynamic decision systems using anchors and Monte Carlo tree search ⋮ Stealthy attacks formalized as STL formulas for Falsification of CPS Security ⋮ Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems ⋮ Robust control for signal temporal logic specifications using discrete average space robustness ⋮ Rigorous Simulation-Based Analysis of Linear Hybrid Systems ⋮ A survey of challenges for runtime verification from advanced application domains (beyond software) ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Feedback control strategies for multi-agent systems under a fragment of signal temporal logic tasks ⋮ Robustness of temporal logic specifications for continuous-time signals ⋮ Parameter Synthesis Through Temporal Logic Specifications ⋮ Algebraic quantitative semantics for efficient online temporal monitoring ⋮ Sampling polynomial trajectories for LTL verification ⋮ Towards physical hybrid systems ⋮ Funnel control for fully actuated systems under a fragment of signal temporal logic specifications ⋮ Adaptive testing for specification coverage and refinement in CPS models ⋮ Risk verification of stochastic systems with neural network controllers ⋮ Parameter synthesis of polynomial dynamical systems ⋮ Survey on mining signal temporal logic specifications ⋮ System design of stochastic models using robustness of temporal properties ⋮ Unwinding biological systems ⋮ MITL verification under timing uncertainty ⋮ A fuzzy real-time temporal logic ⋮ Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications

Uses Software

• TaLiRo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Real-time logics: Complexity and expressiveness
• Robustness of temporal logic specifications for continuous-time signals
• Averaging of nonsmooth systems using dither
• A theory of timed automata
• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Estimation of the Lipschitz constant of a function
• Dynamical properties of timed automata
• Almost ASAP semantics: from timed models to timed implementations
• Distance to the intersection of two sets
• Robust Sampling for MITL Specifications
• On the Expressiveness of MTL Variants over Dense Time
• Temporal Logic Verification Using Simulation
• Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling
• Robust Model-Checking of Linear-Time Properties in Timed Automata
• Hierarchical Synthesis of Hybrid Controllers from Temporal Logic Specifications
• Robust Test Generation and Coverage for Hybrid Systems
• The benefits of relaxing punctuality
• Verification in continuous time by discrete reasoning
• What good are digital clocks?
• Approximation Metrics for Discrete and Continuous Systems
• Robust Analysis of Timed Automata Via Channel Machines
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Automata, Languages and Programming
• Hybrid Systems: Computation and Control
• Formal Modeling and Analysis of Timed Systems
• CONCUR 2003 - Concurrency Theory

This page was built for publication: Robustness of temporal logic specifications for continuous-time signals