Simulation based computation of certificates for safety of dynamical systems

DOI10.1007/978-3-319-65765-3_17zbMATH Open1494.68172arXiv1707.00879OpenAlexW2964162272MaRDI QIDQ1683459FDOQ1683459

Authors: Stefan Ratschan 

Publication date: 1 December 2017

Abstract: In this paper, we present an algorithm for synthesizing certificates---so-called barrier certificates---for safety of hybrid dynamical systems. Unlike the usual approach of using constraint solvers to compute the certificate from the system dynamics, we synthesize the certificate from system simulations. This makes the algorithm applicable even in cases where the dynamics is either not explicitly available, or too complicated to be analyzed by constraint solvers, for example, due to the presence of transcendental function symbols. The algorithm itself allows the usage of heuristic techniques in which case it does not formally guarantee correctness of the result. However, in cases that do allow rigorous constraint solving, the computed barrier certificate can be rigorously verified, if desired. Hence, in such cases, our algorithm reduces the problem of finding a barrier certificate to the problem of formally verifying a given barrier certificate.

Full work available at URL: https://arxiv.org/abs/1707.00879

Recommendations

• Compositional safety analysis using barrier certificates
• Construction of parametric barrier functions for dynamical systems using interval analysis
• Hybrid Systems: Computation and Control
• Synthesizing invariant barrier certificates via difference-of-convex programming
• Automated and formal synthesis of neural barrier certificates for dynamical models

Mathematics Subject Classification ID

Simulation of dynamical systems (37M05) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (6)

• Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
• Compositional safety analysis using barrier certificates
• Automated and formal synthesis of neural barrier certificates for dynamical models
• Learning safe neural network controllers with barrier certificates
• Construction of parametric barrier functions for dynamical systems using interval analysis
• Synthesizing invariant barrier certificates via difference-of-convex programming

This page was built for publication: Simulation based computation of certificates for safety of dynamical systems

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