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

• Safety properties
• Hybrid systems
• Bilinear Matrix inequality (BMI)
• Barrier certificate generation
• Safety verification

Expected input

• BMI problem
• Initial values $u^0,v^0,Z^0$ and $U^0$

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.