Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression

要約

セーフティクリティカルなシナリオで自律システムを活用するには、システムのダイナミクスに影響を与える不確実性やブラックボックスコンポーネントが存在する中での自律システムの動作を検証する必要があります。
この研究では、入出力データセットからの時相論理仕様に対して、モデル化されていないダイナミクスとノイズの多い測定値を含む離散時間動的システムを検証するためのフレームワークを開発します。
この検証フレームワークは、ガウス過程 (GP) 回帰を採用してデータセットから未知のダイナミクスを学習し、連続空間システムを有限状態の不確実なマルコフ決定プロセス (MDP) として抽象化します。
この抽象化は、再現可能なカーネル ヒルベルト空間解析を使用して GP 回帰の誤差による不確実性と離散化によって引き起こされる不確実性を捉える空間の離散化と遷移確率間隔に依存しています。
このフレームワークは、既存のモデル検査ツールを利用して、特定の時相論理仕様に対して不確実な MDP 抽象化を検証します。
ノイズを含む測定から作成された抽象化に関する検証結果を基礎となるシステムに拡張することの正確性を確立します。
フレームワークの計算の複雑さは、データセットのサイズと離散抽象化において多項式であることを示します。
複雑さの分析は、検証結果の品質と、より大きなデータセットとより細かい抽象化を処理するための計算負荷との間のトレードオフを示します。
最後に、線形、非線形、およびスイッチ動的システムを使用したいくつかのケーススタディで、学習および検証フレームワークの有効性を実証します。

要約(オリジナル)

Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties and black-box components that influence the system dynamics. In this work, we develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements against temporal logic specifications from an input-output dataset. The verification framework employs Gaussian process (GP) regression to learn the unknown dynamics from the dataset and abstracts the continuous-space system as a finite-state, uncertain Markov decision process (MDP). This abstraction relies on space discretization and transition probability intervals that capture the uncertainty due to the error in GP regression by using reproducible kernel Hilbert space analysis as well as the uncertainty induced by discretization. The framework utilizes existing model checking tools for verification of the uncertain MDP abstraction against a given temporal logic specification. We establish the correctness of extending the verification results on the abstraction created from noisy measurements to the underlying system. We show that the computational complexity of the framework is polynomial in the size of the dataset and discrete abstraction. The complexity analysis illustrates a trade-off between the quality of the verification results and the computational burden to handle larger datasets and finer abstractions. Finally, we demonstrate the efficacy of our learning and verification framework on several case studies with linear, nonlinear, and switched dynamical systems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google