屏障证书再探

屏障证书可以根据待验证的安全属性，将所考虑的混合系统 (HS) 的状态空间划分为安全部分和不安全部分。因此，这一概念已广泛应用于 HS 的验证中。对屏障证书施加更强的条件意味着可以综合出表达能力较弱的屏障证书。另一方面，综合表达能力更强的屏障证书通常意味着高复杂度。在文献 [9] 中，Kong 等人考虑了如何在保持屏障证书凸性的同时放宽其条件，以便利用半定规划 (SDP) 高效地综合出表达能力更强的屏障证书。在本文中，我们首先讨论如何以一般方式放宽屏障证书的条件，同时保持其凸性。特别是，人们可以灵活地利用不同的较弱条件，通过 SDP 高效地综合出具有更强表达能力的各类屏障证书。这些屏障为验证所考虑的系统提供了更多机会。我们还展示了如何将两个函数组合在一起形成组合屏障证书，以证明所考虑的安全属性，而这两个函数中的任何一个即使根据任何放宽的条件也无法单独用作屏障证书。本文的另一贡献是讨论了如何通过 SDP 从一般放宽条件中发现证书。特别是，我们重点关注如何通过符号检查避免因 SDP 引起的数值误差导致的不可靠性。