屏障证明再探讨
摘要：通过使用屏障证书，可以根据所要验证的安全属性将考虑的混合系统（HS）的状态空间分为安全和不安全部分。因此，这个概念在HS的验证中被广泛使用。对于屏障证书的更强条件意味着可以合成更少表达力的屏障证书。另一方面，合成更具表达力的屏障证书通常意味着高复杂性。在[9]中，Kong等人考虑了如何放松屏障证书的条件，同时保持其凸性，以便可以利用半定编程（SDP）有效地合成更具表达力的屏障证书。在本文中，我们首先讨论如何以一般方式放松屏障证书的条件，同时保持其凸性。特别地，可以灵活地利用不同的较弱条件使用SDP有效地合成不同类型的具有更多表达力的屏障证书。这些屏障证书为验证所考虑的系统提供了更多的机会。我们还展示了如何将两个函数组合在一起形成组合屏障证书，以证明所考虑的安全属性，而其中的任何一个都不能单独用作屏障证书，即使根据任何放松条件也不行。本文的另一个贡献是我们讨论了如何通过SDP从一般放松条件中发现证书。具体而言，我们专注于如何避免由于SDP与符号检查导致的数值误差引起的不准确性。
作者：Liyun Dai and Ting Gan and Bican Xia and Naijun Zhan
论文ID：1310.6481
分类：Systems and Control
分类简称：cs.SY
提交时间：2013-10-25