Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings

要約

安全性やその他の時間的要件を満たすための現実的なシステムのアルゴリズム検証は、採用されている形式的なアプローチのスケーラビリティが低いという問題に悩まされてきました。
厳密な保証を備えたシステムを設計するために、多くのアプローチは依然として基礎となるシステムの正確なモデルに依存しています。
実際にはこの仮定が満たされることはほとんどないため、モデルは測定データから推測するか、完全にバイパスする必要があります。
前者では通常、モデルの構造が事前にわかっていて、膨大な量のデータが利用可能であることが必要ですが、後者では、未知のダイナミクスに関する大量の制限的な数学的仮定が生じます。
問題を非現実的な仮定に移すことなく、スケーラブルな形式的検証アルゴリズムの開発を追求するために、システムの安全性を保証できるバリア証明書の概念を採用し、コンパクトなシステム軌跡のセットから証明書を直接学習します。
条件付き平均埋め込みを使用して、システムからのデータを再生カーネル ヒルベルト空間 (RKHS) に埋め込み、インフレートして結果を確実に強化できる RKHS 曖昧性セットを構築します。
妥当な遷移カーネルのセット。
二乗和最適化とガウス プロセス エンベロープを使用して、結果として得られるプログラムを効率的に解く方法を示します。
私たちのアプローチは、システムのダイナミクスと不確実性に関する限定的な仮定の必要性を取り除き、最先端のアプローチと比較して、テストされたケーススタディでシステムの安全性を検証するサンプルの複雑さが改善されることを示唆しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google