S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems

DOI10.1007/978-3-642-19835-9_21zbMath1316.68069OpenAlexW2131399618MaRDI QIDQ3000653

Yashwanth Annpureddy, Georgios E. Fainekos, Sriram Sankaranarayanan, Che Liu

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_21

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Related Items (26)

Verisig 2.0: verification of neural network controllers using Taylor model preconditioning ⋮ Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness ⋮ Bounded invariant verification for time-delayed nonlinear networked dynamical systems ⋮ An automated system repair framework with signal temporal logic ⋮ Robust online monitoring of signal temporal logic ⋮ Quantitative monitoring of STL with edit distance ⋮ Extracting counterexamples induced by safety violation in linear hybrid systems ⋮ Multi-Requirement Testing Using Focused Falsification ⋮ Formal methods to comply with rules of the road in autonomous driving: state of the art and grand challenges ⋮ Stealthy attacks formalized as STL formulas for Falsification of CPS Security ⋮ Quantifying conformance using the Skorokhod metric ⋮ Unnamed Item ⋮ Using Symmetry Transformations in Equivariant Dynamical Systems for Their Safety Verification ⋮ Proving the existence of fair paths in infinite-state systems ⋮ Clairvoyant monitoring for signal temporal logic ⋮ TeLEx: learning signal temporal logic from positive examples using tightness metric ⋮ A survey of challenges for runtime verification from advanced application domains (beyond software) ⋮ On checking equivalence of simulation scripts ⋮ Solving reachability problems by a scalable constrained optimization method ⋮ Falsification of hybrid systems with symbolic reachability analysis and trajectory splicing ⋮ Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers ⋮ Adaptive testing for specification coverage and refinement in CPS models ⋮ Compositional falsification of cyber-physical systems with machine learning components ⋮ Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties ⋮ Survey on mining signal temporal logic specifications ⋮ System design of stochastic models using robustness of temporal properties

Uses Software

• Matlab
• StateFlow
• S-TaLiRo
• TaLiRo
• Breach

Cites Work

• Robustness of temporal logic specifications for continuous-time signals
• Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
• Falsification of LTL Safety Properties in Hybrid Systems
• Hybrid Systems: Computation and Control
• Simulation and the Monte Carlo Method

This page was built for publication: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems