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

DOI10.1016/J.NAHS.2024.101491zbMATH Open1544.93552MaRDI QIDQ6581256FDOQ6581256

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)

Cites Work

• Avoiding geometric intersection operations in reachability analysis of hybrid systems
• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Formal analysis of piecewise affine systems through formula-guided refinement
• Title not available (Why is that?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Constrained zonotopes: a new tool for set-based estimation and fault detection
• An introduction to practical formal methods using temporal logic
• Symbolic reachability computation for families of linear vector fields
• Utilizing dependencies to obtain subsets of reachable sets
• Title not available (Why is that?)
• 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
• 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

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