通过凸差规划合成不变屏障证书

屏障证书通常作为一种归纳不变量，将不安全区域与状态可达集隔离，因此被广泛用于证明混合系统（可能在无限时间范围内）的安全性。我们提出了一种关于屏障证书的新条件，称为不变屏障证书条件，可见证微分动力系统的无界时间安全性。所提条件是迄今为止关于屏障证书限制最小的条件，并且可证明为达到归纳不变性所需的最弱条件。我们表明，解除不变屏障证书条件——从而合成不变屏障证书——可编码为求解受双线性矩阵不等式（BMI）约束的优化问题。我们进一步提出了一种基于凸差规划的合成算法，该算法通过求解一系列凸优化问题来逼近 BMI 问题的局部最优解。该算法被纳入分支定界框架中，以分治方式搜索全局最优。我们给出了方法的弱完备性结果，即在存在足以证明系统安全的归纳不变量（以给定模板形式）时，保证（在某些温和假设下）能找到屏障证书。在基准示例上的实验结果证明了我们方法的有效性和高效性。