报告题目：A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation

主办单位：英国威廉希尔体育公司

报告专家：杨争峰

专家所在单位：华东师范大学

报告时间：2020年7月15日15:00

报告地点：腾讯会议（会议ID：281 685 978）

专家简介：杨争峰，华东师范大学软件工程学院教授。2006年于中国科学院数学与系统科学研究院获博士学位。主要从事符号计算、形式化方法、软件工程等研究，在CAV、EMSOFT、FM、ISSAC、CVPR等国际会议和JSC、ACM TECS、IEEE TCAD等国际期刊上发表学术论文40余篇。

报告摘要:Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a bilinear matrix inequality (BMI) with a particular type. In this talk, we reveal the special feature of the problem, and adopt it to build a novel computational method. The proposed method introduces a sequential iterative scheme that is able to find analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more efficient than them. In addition, different from popular LMI solving based methods, it does not make the verification conditions more conservative, and thus reduces the risk of missing feasible solutions. Benefitting from these two appealing features, it can produce barrier certificates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.

邀请人：郑大彬