将归纳不变量编码为障碍证书：基于凹凸差规划的综合性合成
计算机科学中的逻辑
2022-09-21 v1 动力系统
摘要
障碍证书常作为将不安全区域与状态可达集隔离的归纳不变量，因而被广泛用于证明混合系统（可能跨越无限时间域）的安全性。我们提出一种关于障碍证书的新条件，称为不变量障碍证书条件，可见证微分动力系统的无界时间安全性。所提条件是达成归纳不变性的最弱可能条件。我们证明，解除不变量障碍证书条件——从而合成不变量障碍证书——可编码为求解受双线性矩阵不等式（BMI）约束的优化问题。我们进一步提出基于凹凸差（difference-of-convex）规划的综合性算法，其通过求解一系列凸优化问题来逼近 BMI 问题的局部最优。该算法被纳入分支定界框架，以分治方式搜索全局最优。我们给出方法的弱完备性结果：即，只要存在足以证明系统安全的归纳不变量（给定模板形式），就保证（在某些温和假设下）能找到障碍证书。在基准上的实验结果展示了我们方法的有效性与高效性。
引用
@article{arxiv.2209.09703,
title = {Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
journal= {arXiv preprint arXiv:2209.09703},
year = {2022}
}
备注
To be published in Inf. Comput. arXiv admin note: substantial text overlap with arXiv:2105.14311