Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
From MaRDI portal
Publication:2105455
DOI10.1016/j.ic.2022.104965OpenAlexW4296691831MaRDI QIDQ2105455
Mingshuai Chen, Qiuye Wang, Naijun Zhan, Bai Xue, Joost-Pieter Katoen
Publication date: 8 December 2022
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2209.09703
semidefinite programmingbilinear matrix inequalitiesbarrier certificatesdifference-of-convex programminginductive invariants
Uses Software
Cites Work
- Seeking Darboux polynomials
- Barrier certificates revisited
- Simple approximations of semialgebraic sets and their applications to control
- Construction of parametric barrier functions for dynamical systems using interval analysis
- The algorithmic analysis of hybrid systems
- Successive linearization methods for nonlinear semidefinite programs
- Synthesizing invariant barrier certificates via difference-of-convex programming
- A Newton-like method for solving rank constrained linear matrix inequalities
- First and second order analysis of nonlinear semidefinite programs
- Convergence analysis of difference-of-convex algorithm with subanalytic data
- DC programming and DCA: thirty years of developments
- DC decomposition of nonconvex polynomials with algebraic techniques
- Global optimization for the biaffine matrix inequality problem
- Convex computation of extremal invariant measures of nonlinear dynamical systems and Markov processes
- Vector barrier certificates and comparison systems
- Automated and formal synthesis of neural barrier certificates for dynamical models
- Nonlinear Craig interpolant generation
- A novel approach for solving the BMI problem in barrier certificates generation
- Exact algorithms for semidefinite programs with degenerate feasible set
- A linear programming relaxation based approach for generating barrier certificates of hybrid systems
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Local and superlinear convergence of a primal-dual interior point method for nonlinear semidefinite programming
- Church's thesis meets the \(N\)-body problem
- The complexity of the matrix eigenproblem
- An alternating direction method for solving convex nonlinear semidefinite programming problems
- Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
- Simulation-guided lyapunov analysis for hybrid dynamical systems
- Stability and stabilization of polynomial dynamical systems using Bernstein polynomials
- A practical method for computing the largestM-eigenvalue of a fourth-order partially symmetric tensor
- Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
- Decidability of the Reachability for a Family of Linear Vector Fields
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Constraint-Based Approach for Analysis of Hybrid Systems
- Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization
- Approximate Volume and Integration for Basic Semialgebraic Sets
- Trust-Region Interior-Point SQP Algorithms for a Class of Nonlinear Programming Problems
- Linear Matrix Inequalities in System and Control Theory
- Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
- Control Barrier Function Based Quadratic Programs for Safety Critical Systems
- A Global Algorithm for Nonlinear Semidefinite Programming
- Reachability Analysis for Solvable Dynamical Systems
- An Interior Point Constrained Trust Region Method for a Special Class of Nonlinear Semidefinite Programming Problems
- Formal Synthesis of Stochastic Systems via Control Barrier Certificates
- Synthesizing barrier certificates using neural networks
- Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems
- Constraints for Continuous Reachability in the Verification of Hybrid Systems
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Combining Convex–Concave Decompositions and Linearization Approaches for Solving BMIs, With Application to Static Output Feedback
- Validating numerical semidefinite programming solvers for polynomial invariants
- Symbolic reachability computation for families of linear vector fields
- Delta-decision procedures for exists-forall problems over the reals
- Synthesis in pMDPs: a tale of 1001 parameters
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
