Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis

DOI10.1016/j.nahs.2024.101491zbMATH Open1544.93552MaRDI QIDQ6581256

Stanley Bak, Niklas Kochdumper

Publication date: 30 July 2024

Published in: Nonlinear Analysis. Hybrid Systems (Search for Journal in Brave)

zbMATH Keywords

linear systemsformal verificationmodel checkingreachability analysisautomationsignal temporal logic

Mathematics Subject Classification ID

Linear systems in control theory (93C05) Automated systems (robots, etc.) in control theory (93C85) Attainable sets, reachability (93B03) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Constrained zonotopes: a new tool for set-based estimation and fault detection
• Formal analysis of piecewise affine systems through formula-guided refinement
• STL model checking of continuous and hybrid systems
• Linearization-based algorithms for mixed-integer nonlinear programs with convex continuous relaxation
• Avoiding geometric intersection operations in reachability analysis of hybrid systems
• An Introduction to Practical Formal Methods Using Temporal Logic
• Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis
• Utilizing dependencies to obtain subsets of reachable sets
• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Symbolic reachability computation for families of linear vector fields
• Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems
• Adaptive parameter tuning for reachability analysis of nonlinear systems
• Fully Automated Verification of Linear Systems Using Inner and Outer Approximations of Reachable Sets

This page was built for publication: Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis