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.

Related papers

https://doi.org/10.1007/978-3-030-53288-8_29 (CAV 2020)

Last publication date

14 July 2020

Related tools

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

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.