基于障碍证书的不确定动力系统超性质验证

超性质是需要对系统多条执行轨迹进行量化的系统性质。超性质能够表达信息物理系统中若干令人关注的规范——如不透明性、鲁棒性与非干涉性——这些无法用线性时序性质表达。本文首次提出一种无离散化方法，用于针对超性质对离散时间不确定动力系统进行形式化验证。所提方法通过利用对应于原规范补码的基于自动机结构，将复杂超性质分解为若干验证条件。随后通过综合所谓增广障碍证书来消解这些验证条件，其为底层系统提供特定安全保证。对于具有多项式型动力学的系统，我们将问题归约为平方和优化，给出综合多项式型增广障碍证书的一个可靠过程。我们在两个物理案例研究上针对两个重要超性质——初态不透明性与初态鲁棒性——展示了所提方法的有效性。