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 output data via a targeted marginal Metropolis-Hastings sampler. The resulting samples are used to construct a barrier certificate through a sum-of-squares program. Probabilistic guarantees for its validity with respect to the true, unknown system are obtained by testing on an additional set of posterior samples. The approach and its probabilistic guarantees are illustrated through a numerical simulation.
翻译:在动态系统中验证安全性至关重要,但广泛用于证明系统轨迹保持在安全区域内的屏障证书通常需要显式的系统模型。当动态特性未知时,可采用数据驱动方法替代,然而获得有效的证书需要进行严格的不确定性量化。为此,现有方法通常依赖于全状态测量,限制了其适用性。本文提出了一种针对具有隐状态和多项式动态的未知系统合成屏障证书的新方法。该方法采用贝叶斯框架,通过目标边缘Metropolis-Hastings采样器,利用输出数据更新状态空间表示中的先验分布。所得样本通过平方和规划程序用于构建屏障证书。通过在另一组后验样本上进行测试,获得了该证书相对于真实未知系统有效性的概率保证。通过数值模拟展示了该方法及其概率保证。