Algorithmic verification of realistic systems to satisfy safety and other temporal requirements has suffered from poor scalability of the employed formal approaches. To design systems with rigorous guarantees, many approaches still rely on exact models of the underlying systems. Since this assumption can rarely be met in practice, models have to be inferred from measurement data or are bypassed completely. Whilst former usually requires the model structure to be known a-priori and immense amounts of data to be available, latter gives rise to a plethora of restrictive mathematical assumptions about the unknown dynamics. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates, which can guarantee safety of the system, and learn the certificate directly from a compact set of system trajectories. We use conditional mean embeddings to embed data from the system into a reproducing kernel Hilbert space (RKHS) and construct an RKHS ambiguity set that can be inflated to robustify the result w.r.t. a set of plausible transition kernels. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope. Our approach lifts the need for restrictive assumptions on the system dynamics and uncertainty, and suggests an improvement in the sample complexity of verifying the safety of a system on a tested case study compared to a state-of-the-art approach.

翻译：实际系统满足安全性及其他时序需求的形式化验证算法受限于形式化方法自身的可扩展性差。为设计具有严格保证的系统，许多方法仍依赖系统精确模型。由于该假设在实践中几乎无法满足，模型必须从测量数据推断或完全绕过。前者通常要求先验已知模型结构且数据量庞大，后者则对未知动力学引入大量限制性数学假设。为开发可扩展的验证算法同时避免将问题转嫁于不切实际的假设，本文采用障碍证书概念（可保证系统安全性），并直接从紧凑的系统轨迹集合中学习障碍证书。我们利用条件均值嵌入将系统数据嵌入再生核希尔伯特空间（RKHS），并构建可膨胀的RKHS模糊集，以增强结果对一组合理转移核的鲁棒性。我们展示了如何通过平方和优化与高斯过程包络高效求解所得规划。该方法消除了对系统动力学和不确定性的限制性假设需求，并在测试案例中证明：与现有最优方法相比，本方法在系统安全验证所需的样本复杂度方面有所改善。