基于障碍证书的近似不透明性验证

本文的动机源于信息物理系统日益增长的安全担忧。在此，我们针对一类离散时间控制系统，开发了一种无离散化的验证方案，用于验证一种称为近似初始状态不透明性的信息流安全属性。我们提出了所谓的增广控制障碍证书的概念，并结合刻画系统初始集与秘密集的指定感兴趣区域。基于所提障碍证书的存在性，给出了离散时间控制系统（不具备）近似初始状态不透明性的充分条件。我们进一步通过将障碍证书的条件转化为平方和规划问题，提出了一种高效的计算方法。所提结果的有效性通过两个数值算例加以说明。