A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates

DOI10.1109/TAC.2007.902736zbMath1366.93711DBLPjournals/tac/PrajnaJP07OpenAlexW2033118636WikidataQ57581920 ScholiaQ57581920MaRDI QIDQ5282200

Ali Jadbabaie, Stephen Prajna, George J. Pappas

Publication date: 27 July 2017

Published in: IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/tac.2007.902736

Mathematics Subject Classification ID

Control/observation systems with incomplete information (93C41) Least squares and related methods for stochastic control systems (93E24) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Related Items (82)

State-based confidence bounds for data-driven stochastic reachability using Hilbert space embeddings ⋮ Safety-critical dynamic event-triggered control of nonlinear systems ⋮ Some applications of polynomial optimization in operations research and real-time decision making ⋮ Design and analysis of a potential-based controller for safe robot navigation in unknown GPS-denied environments with strictly convex obstacles ⋮ An iterative scheme of safe reinforcement learning for nonlinear systems via barrier certificate generation ⋮ A stochastic games framework for verification and control of discrete time stochastic hybrid systems ⋮ Deep recurrent neural networks with finite-time terminal sliding mode control for a chaotic fractional-order financial system with market confidence ⋮ Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability ⋮ Verification of Hybrid Systems ⋮ Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems ⋮ Computing sum of squares decompositions with rational coefficients ⋮ Necessary and sufficient conditions for the nonincrease of scalar functions along solutions to constrained differential inclusions ⋮ Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares programming ⋮ Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems ⋮ A compositional modelling and verification framework for stochastic hybrid systems ⋮ Output transient trajectory shaping control for a class of nonlinear systems ⋮ Sufficient conditions for forward invariance and contractivity in hybrid inclusions using barrier functions ⋮ A barrier function approach to finite-time stochastic system verification and control ⋮ Bridging the gap between optimal trajectory planning and safety-critical control with applications to autonomous vehicles ⋮ Control barrier functions for stochastic systems ⋮ An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems ⋮ Safety verification for distributed parameter systems using barrier functionals ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Computation of polytopic invariants for polynomial dynamical systems using linear programming ⋮ Safety verification for regime-switching jump diffusions via barrier certificates ⋮ Prescribed-Time Mean-Nonovershooting Control under Finite-Time Vanishing Noise ⋮ Robust control barrier functions under high relative degree and input constraints for satellite trajectories ⋮ Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems ⋮ Estimating infinitesimal generators of stochastic systems with formal error bounds ⋮ Formal safety verification of unknown continuous-time systems ⋮ Verifying Neural Network Controlled Systems Using Neural Networks ⋮ k-Inductive Barrier Certificates for Stochastic Systems ⋮ Compositional synthesis of control barrier certificates for networks of stochastic systems against \(\omega\)-regular specifications ⋮ Computing Differential Invariants of Hybrid Systems as Fixedpoints ⋮ Control Lyapunov–Barrier function based model predictive control for stochastic nonlinear affine systems ⋮ Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions ⋮ Safe Self-Triggered Control Based on Precomputed Reachability Sequences ⋮ A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications ⋮ Transverse contraction criteria for existence, stability, and robustness of a limit cycle ⋮ A computational approach to synthesizing guards for hybrid systems ⋮ Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates ⋮ A study of the double pendulum using polynomial optimization ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Barrier certificates revisited ⋮ Constrained control of input-output linearizable systems using control sharing barrier functions ⋮ A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets ⋮ Safe autonomy under perception uncertainty using chance-constrained temporal logic ⋮ Minimum wave speeds in monostable reaction–diffusion equations: sharp bounds by polynomial optimization ⋮ Maximizing the probability of attaining a target prior to extinction ⋮ Vector barrier certificates and comparison systems ⋮ Co-design of safe and efficient networked control systems in factory automation with state-dependent wireless fading channels ⋮ Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs ⋮ Safety verification of interconnected hybrid systems using barrier certificates ⋮ A learner-verifier framework for neural network controllers and certificates of stochastic systems ⋮ Hybrid controller synthesis for nonlinear systems subject to reach-avoid constraints ⋮ Data-driven verification and synthesis of stochastic systems via barrier certificates ⋮ Safety critical control design for nonlinear system with tracking and safety objectives ⋮ Verification of quantum systems using barrier certificates ⋮ Safety-critical multi-tasks control for switched systems via several barrier functions ⋮ A dynamic game approach to distributionally robust safety specifications for stochastic systems ⋮ Model reference safety-critical adaptive control for a class of nonlinearly parameterized systems ⋮ Learning safe neural network controllers with barrier certificates ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models ⋮ Soft-minimum and soft-maximum barrier functions for safety with actuation constraints ⋮ Sufficient conditions for robust safety in differential inclusions using barrier functions ⋮ On converse zeroing barrier functions ⋮ Invariant set estimation for piecewise affine dynamical systems using piecewise affine barrier function ⋮ Safety analysis of integrated adaptive cruise and Lane keeping control using multi-modal port-Hamiltonian systems ⋮ Sufficient conditions for feasibility of optimal control problems using control barrier functions ⋮ Safety of stochastic systems: an analytic and computational approach ⋮ Probabilistic ultimate bounds and invariant sets in nonlinear systems ⋮ Bounding Extreme Events in Nonlinear Dynamics Using Convex Optimization ⋮ Safety-critical optimal control for autonomous systems ⋮ A linear algebra method to decompose forms whose length is lower than the number of variables into weighted sum of squares ⋮ Computing differential invariants of hybrid systems as fixed points ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Compositional construction of control barrier functions for continuous-time stochastic hybrid systems ⋮ Safety stabilization of switched systems with unstable subsystems ⋮ Vehicle motion control under equality and inequality constraints: a diffeomorphism approach ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Safe-by-design control for Euler-Lagrange systems ⋮ Small-gain theorem for safety verification of interconnected systems

This page was built for publication: A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates