Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions

DOI10.1145/3575870.3587121MaRDI QIDQ6202080zbMATH OpenFDO

Authors Mark Wetzlinger, Niklas Kochdumper, Stanley Bak, Matthias Althoff

Publication date 21 February 2024

Published in Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://mediatum.ub.tum.de/1710697

zbMATH Keywords

set-based computingformal verificationiterative refinementhigh-dimensional systemsautomated parameter tuningcounterexample.

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 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)

Cites work

• scientific article; zbMATH DE number 1444339 (Why is no real title available?)
• scientific article; zbMATH DE number 1444352 (Why is no real title available?)
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• A dynamic algorithm for approximate flow computations
• A note on regularity and positive definiteness of interval matrices
• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Adaptive reachability algorithms for nonlinear systems using abstraction error analysis
• Computational techniques for hybrid system verification
• Conservative time discretization: a comparative study
• Constrained zonotopes: a new tool for set-based estimation and fault detection
• Counterexample-Guided Refinement of Template Polyhedra
• Differential dynamic logic for hybrid systems
• Efficient dynamic error reduction for hybrid systems reachability analysis
• Eliminating spurious transitions in reachability with support functions
• Ellipsotopes: Uniting Ellipsoids and Zonotopes for Reachability Analysis and Fault Detection
• Flowpipe approximation and clustering in space-time
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• JuliaReach
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Parsimonious, Simulation Based Verification of Linear Systems
• Reachability Analysis for Solvable Dynamical Systems
• Reachability Analysis of Hybrid Systems Using Support Functions
• Reachability analysis of continuous-time piecewise affine systems
• Reachability analysis of linear systems using support functions
• Simulation-equivalent reachability of large linear systems with inputs
• Systematic Simulation Using Sensitivity Analysis
• Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis

This page was built for publication: Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions

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