PV1 SISBMI: Sequential Iterative Scheme for solving a Bilinear Matrix Inequalityby solving a BMI problem checks if the unsafe state region is reachable

Algorithm & tool, called Sequential Iterative Scheme for solving a BMI (bilinear matrix inequality)

Application domain/field

Expected input

Expected output

Feasible solution (u*,v*) for the BMI problem

Internals

A barrier certificate is a function where the zero level set separates the unsafe region from all reachable states of a system. The existence of a barrier certificate implies that the unsafe region is not reachable, therefore safety verification can be transformed into the problem of barrier certificate generation. Barrier certificate generation is equivalent to solving a bilinear matrix inequality (BMI) with a particular type.
Hybrid system

Related papers

A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation (CAV 2020)

Last publication date

14 July 2020

Related tools

Compared to in the CAV '20 paper: PENBMI, SOSTOOLS

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.