This work aims to formally verify safety properties of discrete-time unknown systems by synthesizing extreme learning machine (ELM)-based barrier certificates by minimizing the Lipschitz constant of the candidate barrier by presenting a grid-based sampling technique to formally verify its validity using the minimum number of samples required.
Abstract
Deep learning methods like neural networks have greatly simplified the computation of safety certificates for complex nonlinear systems with unknown dynamics. However, due to the data-driven nature of these certificates and the complex architecture of neural networks, computation time as well as robustness guarantees across unseen data remain a challenge. This work aims to formally verify safety properties of discrete-time unknown systems by synthesizing extreme learning machine (ELM)-based barrier certificates. Compared to neural network counterparts, this approach greatly improves convergence guarantees and computational time due to its architectural simplicity and the convex nature of the underlying optimization problem. By minimizing the Lipschitz constant of the candidate barrier, we present a grid-based sampling technique to formally verify its validity using the minimum number of samples required. We demonstrate through numerical examples the effectiveness of our approach, and compare with traditional deep-learning based certificate synthesis to highlight its benefits.
This paper integrates modern Hopfield networks with a port-Hamiltonian neural ODE, enabling by design the construction of barrier functions yielding explicit admissible-input sets and quantitative robustness radii that are more robust to external solicitations than comparable existing approaches.
A novel two-stage training framework for provably stable neural network observers that decouples the optimization into a point-guided Lyapunov pre-training phase, which rapidly achieves high estimation accuracy and local stability over sampled states and an LMI fine-tuning phase that efficiently satisfies a strict glob...
Zhang-Yi Wang, Jia-Xu Liu, Song Chen et al.· 0 citations
Hamilton-Jacobi (HJ) reachability analysis offers formal safety guarantees for control systems, but training accurate neural certificates remains difficult, particularly when unsafe regions are hard to characterize. We propose a verification-guided training framework that addresses this by using probabilistic enumerati...
Mihaela-Larisa Clement, Tosca Pierro, E. Bartocci et al.· 0 citations
Control barrier functions are an effective model-based tool to formally certify the safety of a system. However, transferring their theoretical guarantees to real-world robotics systems requires high model fidelity. For example, payloads or wind disturbances can cause significant model perturbations to an aerial vehicl...
Li-Shuo Pan, Mattia Catellani, An Cao et al.· 0 citations
Model predictive control is a high-performance control method, but it incurs comparatively high online computational costs across many control tasks and is challenging to realize in low-level hardware settings. To address this, we present a framework for generating neural network controllers that provably inherit the s...
Hendrik Alsmeier, Maik Pfefferkorn, Rolf Findeisen· 0 citations
Semidefinite programming (SDP) certificates for feedback systems containing deep neural networks (NNs) typically scale with the total number of neurons, whereas small-gain tests are scalable but can be highly conservative. This paper develops a unified and scalable framework for incremental robust stability and perform...
Zi-Cheng Wang, Peter J. Seiler, G. Dullerud et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.