Certifying safety in dynamical systems is crucial, but barrier certificates - widely used to verify that system trajectories remain within a safe region - typically require explicit system models. When dynamics are unknown, data-driven methods can be used instead, yet obtaining a valid certificate requires rigorous uncertainty quantification. For this purpose, existing methods usually rely on full-state measurements, limiting their applicability. This paper proposes a novel approach for synthesizing barrier certificates for unknown systems with latent states and polynomial dynamics. A Bayesian framework is employed, where a prior in state-space representation is updated using input-output data via a targeted marginal Metropolis-Hastings sampler. The resulting samples are used to construct a candidate barrier certificate through a sum-of-squares program. It is shown that if the candidate satisfies the required conditions on a test set of additional samples, it is also valid for the true, unknown system with high probability. The approach and its probabilistic guarantees are illustrated through a numerical simulation.
翻译:在动态系统中验证安全性至关重要,但广泛用于确保系统轨迹保持在安全区域内的屏障证书通常需要显式的系统模型。当系统动态未知时,可采用数据驱动方法,但获得有效证书需要严格的不确定性量化。为此,现有方法通常依赖于全状态测量,限制了其适用性。本文提出了一种新颖方法,用于为具有隐状态和多项式动态的未知系统合成屏障证书。该方法采用贝叶斯框架,通过定向边缘Metropolis-Hastings采样器,利用输入-输出数据更新状态空间表示中的先验分布。所得样本通过平方和规划用于构建候选屏障证书。研究表明,若候选证书在额外样本的测试集上满足所需条件,则该证书以高概率对真实未知系统同样有效。通过数值模拟展示了该方法及其概率保证。