关于无界域上基于半定规划的屏障证书合成的完备性
系统与控制
2024-07-10 v4 系统与控制
摘要
屏障证书作为见证系统安全性的微分不变量，在信息物理系统（CPS）的验证中起着关键作用。主流的屏障证书合成计算方法基于半定规划（SDP），利用Putinar正位置定理。因此，这些方法受到阿基米德条件的限制，该条件要求所有变量有界，即系统定义在有界域上。对于无界域上的系统，不幸的是，现有方法变得不完备，可能无法识别潜在的屏障证书。在本文中，我们针对无界情况解决了这一局限性。我们首先通过齐次化（优化社区最近使用的一种技术，将无界优化问题简化为有界问题）给出了多项式屏障证书的完整刻画。此外，受此公式的启发，我们引入了齐次化系统的定义，并提出了具有更强表达能力的一族非多项式屏障证书的完整刻画。实验结果表明，我们的两种方法在保持相当效率水平的同时更加有效。
引用
@article{arxiv.2312.15416,
title = {On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains},
author = {Hao Wu and Shenghua Feng and Ting Gan and Jie Wang and Bican Xia and Naijun Zhan},
journal= {arXiv preprint arXiv:2312.15416},
year = {2024}
}
备注
Accepted by the 26th international symposium on Formal Methods (FM2024). 18 pages, 1 figure. Updated on 2024.7.9, fix two typos in Lemma 1 and Equation 10