Synthesizing invariant barrier certificates via difference-of-convex programming

DOI10.1007/978-3-030-81685-8_21zbMath1493.68222arXiv2105.14311OpenAlexW3185235159MaRDI QIDQ832194

Joost-Pieter Katoen, Mingshuai Chen, Bai Xue, Naijun Zhan, Qiuye Wang

Publication date: 25 March 2022

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

Mathematics Subject Classification ID

Applications of mathematical programming (90C90) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming

Uses Software

• Sostools
• RSOLVER
• Benchmarks
• LMIRank
• z3
• TRICE
• PENLAB
• HSolver
• QSDPNAL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Seeking Darboux polynomials
• Barrier certificates revisited
• Construction of parametric barrier functions for dynamical systems using interval analysis
• The algorithmic analysis of hybrid systems
• Successive linearization methods for nonlinear semidefinite programs
• A Newton-like method for solving rank constrained linear matrix inequalities
• QSDPNAL: a two-phase augmented Lagrangian method for convex quadratic semidefinite programming
• DC programming and DCA: thirty years of developments
• Global optimization for the biaffine matrix inequality problem
• Vector barrier certificates and comparison systems
• A novel approach for solving the BMI problem in barrier certificates generation
• Decoupling abstractions of non-linear ordinary differential equations
• A linear programming relaxation based approach for generating barrier certificates of 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
• 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
• 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
• Trust-Region Interior-Point SQP Algorithms for a Class of Nonlinear Programming Problems
• 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
• 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
• Symbolic reachability computation for families of linear vector fields

This page was built for publication: Synthesizing invariant barrier certificates via difference-of-convex programming