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

DOI10.1016/J.NAHS.2024.101491MaRDI QIDQ6581256zbMATH OpenFDO

Authors Niklas Kochdumper, Stanley Bak

Publication date 30 July 2024

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

zbMATH Keywords

linear systemsmodel checkingautomationreachability analysisformal verificationsignal temporal logic

Mathematics Subject Classification ID

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

Recommendations

• Data-driven verification of stochastic linear systems with signal temporal logic constraints
• Reachability analysis of linear systems with stepwise constant inputs
• STL model checking of continuous and hybrid systems
• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Tightened reachability constraints for the verification of linear hybrid systems

Cites work

• scientific article; zbMATH DE number 1956650 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Adaptive parameter tuning for reachability analysis of nonlinear systems
• An introduction to practical formal methods using temporal logic
• Avoiding geometric intersection operations in reachability analysis of hybrid systems
• Constrained zonotopes: a new tool for set-based estimation and fault detection
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal analysis of piecewise affine systems through formula-guided refinement
• Fully Automated Verification of Linear Systems Using Inner and Outer Approximations of Reachable Sets
• Linearization-based algorithms for mixed-integer nonlinear programs with convex continuous relaxation
• STL model checking of continuous and hybrid systems
• Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis
• Symbolic reachability computation for families of linear vector fields
• Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems
• Utilizing dependencies to obtain subsets of reachable sets

Cited in

(2)

• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Constraint-driven nonlinear reachability analysis with automated tuning of tool properties

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6581256)