报告题目: A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation
直播平台及链接： 腾讯会议（会议ID：682 336 686）
Barrier certi?cates 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 certi?cate 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 ?nd analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more e?cient than them. In addition, di?erent from popular LMI solving based methods, it does not make the veri?cation conditions more conservative, and thus reduces the risk of missing feasible solutions. Bene?tting from these two appealing features, it can produce barrier certi?cates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.
杨争峰，华东师范大学软件工程学院教授。2006年于中国科学院数学与系统科学研究院获博士学位。主要从事符号计算、形式化方法、软件工程等研究，在CAV、EMSOFT、FM、ISSAC、CVPR等国际会议和JSC、ACM TECS、IEEE TCAD等国际期刊上发表学术论文40余篇。