使用障碍证书与条件均值嵌入的数据驱动分布式鲁棒安全性验证

对现实系统满足安全性和其他时序要求进行算法验证，一直受限于所采用形式化方法较差的可扩展性。为了设计具有严格保证的系统，许多方法仍然依赖于底层系统的精确模型。由于这一假设在实践中难以满足，模型必须从测量数据中推断或被完全绕过。前者通常要求事先已知模型结构并拥有海量数据，而后者则引发了对未知动力学的诸多限制性数学假设。为了在不将问题转化为不切实际假设的情况下开发可扩展的形式化验证算法，我们采用了障碍证书的概念，该证书可以保证系统的安全性，并直接从一组紧凑的系统轨迹中学习该证书。我们使用条件均值嵌入将系统数据嵌入到再生核希尔伯特空间（RKHS）中，并构建一个 RKHS 歧义集，该集合可被扩充以针对一组合理的转移核鲁棒化结果。我们展示了如何使用平方和优化和高斯过程包络高效求解所得规划。我们的方法免除了对系统动力学和不确定性的限制性假设，并在一项测试案例研究中表明，与最先进方法相比，验证系统安全性的样本复杂度有所改善。