論文の概要: Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression
- arxiv url: http://arxiv.org/abs/2201.00655v2
- Date: Tue, 16 Jul 2024 17:33:04 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-18 00:37:39.500628
- Title: Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression
- Title（参考訳）: ガウス過程回帰による未知の力学系の形式的検証
- Authors: John Skovbekk, Luca Laurenti, Eric Frew, Morteza Lahijanian,
- Abstract要約: 安全クリティカルなシナリオにおける自律システムの活用には、不確実性の存在下での行動を検証する必要がある。
本研究では,非モデル化された力学と雑音測定を用いた離散時間力学システムの検証フレームワークを開発した。
- 参考スコア（独自算出の注目度）: 11.729744197698718
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 安全クリティカルなシナリオにおける自律システムの活用には、システムのダイナミクスに影響を与える不確実性やブラックボックスコンポーネントの存在下での行動を検証する必要がある。
本研究では,インプット・アウトプット・データセットから,時間論理仕様に対する非モデル化された力学と雑音測定による離散時間力学システムの検証を行うフレームワークを開発する。
検証フレームワークはガウス過程(GP)回帰を用いてデータセットから未知のダイナミクスを学習し、連続空間システムを有限状態で不確実なマルコフ決定過程(MDP)として抽象化する。
この抽象化は、再現可能なカーネルヒルベルト空間解析を用いて、GP回帰の誤差による不確かさを捉える空間の離散化と遷移確率間隔、および離散化によって引き起こされる不確かさに依存する。
このフレームワークは、既存のモデルチェックツールを使用して、特定の時間論理仕様に対して不確実なMDP抽象化を検証する。
ノイズ測定結果から基礎システムへの抽象化結果の拡張の正当性を確立した。
フレームワークの計算複雑性は、データセットのサイズと離散抽象の多項式であることを示す。
複雑性分析は、検証結果の品質と、より大きなデータセットとより詳細な抽象化を扱うための計算負荷との間のトレードオフを示している。
最後に,線形・非線形・切替力学系を用いたいくつかのケーススタディにおいて,学習・検証フレームワークの有効性を実証した。
関連論文リスト
- NonSysId: A nonlinear system identification package with improved model term selection for NARMAX models [2.6684288899870543]
本稿では,非線形システム識別のためのオープンソースソフトウェアパッケージであるNonSysIdを紹介する。
このソフトウェアには、シミュレーション(フリーラン)の精度を優先する高度な項選択手法が組み込まれている。
NonSysIdは、構造的健康モニタリング、故障診断、バイオメディカル信号処理などのリアルタイムアプリケーションに特に適している。
論文 参考訳（メタデータ） (2024-11-25T15:19:19Z) - InVAErt networks: a data-driven framework for model synthesis and
identifiability analysis [0.0]
inVAErtは物理システムのデータ駆動分析と合成のためのフレームワークである。
これは、前方および逆写像を表す決定論的デコーダ、系の出力の確率分布を捉える正規化フロー、入力と出力の間の単射性の欠如についてコンパクトな潜在表現を学ぶ変分エンコーダを使用する。
論文 参考訳（メタデータ） (2023-07-24T07:58:18Z) - Bayesian Spline Learning for Equation Discovery of Nonlinear Dynamics
with Quantified Uncertainty [8.815974147041048]
本研究では,非線形(時空間)力学の擬似的支配方程式を,定量化された不確実性を伴うスパースノイズデータから同定する枠組みを開発した。
提案アルゴリズムは、正準常微分方程式と偏微分方程式によって制御される複数の非線形力学系に対して評価される。
論文 参考訳（メタデータ） (2022-10-14T20:37:36Z) - A Causality-Based Learning Approach for Discovering the Underlying
Dynamics of Complex Systems from Partial Observations with Stochastic
Parameterization [1.2882319878552302]
本稿では,部分的な観測を伴う複雑な乱流系の反復学習アルゴリズムを提案する。
モデル構造を識別し、観測されていない変数を復元し、パラメータを推定する。
数値実験により、新しいアルゴリズムはモデル構造を同定し、多くの複雑な非線形系に対して適切なパラメータ化を提供することに成功した。
論文 参考訳（メタデータ） (2022-08-19T00:35:03Z) - Capturing Actionable Dynamics with Structured Latent Ordinary
Differential Equations [68.62843292346813]
本稿では,その潜在表現内でのシステム入力の変動をキャプチャする構造付き潜在ODEモデルを提案する。
静的変数仕様に基づいて,本モデルではシステムへの入力毎の変動要因を学習し,潜在空間におけるシステム入力の影響を分離する。
論文 参考訳（メタデータ） (2022-02-25T20:00:56Z) - A Priori Denoising Strategies for Sparse Identification of Nonlinear
Dynamical Systems: A Comparative Study [68.8204255655161]
本研究では, 局所的およびグローバルな平滑化手法の性能と, 状態測定値の偏差について検討・比較する。
一般に,測度データセット全体を用いたグローバルな手法は,局所点の周辺に隣接するデータサブセットを用いる局所的手法よりも優れていることを示す。
論文 参考訳（メタデータ） (2022-01-29T23:31:25Z) - Leveraging the structure of dynamical systems for data-driven modeling [111.45324708884813]
トレーニングセットとその構造が長期予測の品質に与える影響を考察する。
トレーニングセットのインフォームドデザインは,システムの不変性と基盤となるアトラクションの構造に基づいて,結果のモデルを大幅に改善することを示す。
論文 参考訳（メタデータ） (2021-12-15T20:09:20Z) - Structure-Preserving Learning Using Gaussian Processes and Variational
Integrators [62.31425348954686]
本稿では,機械系の古典力学に対する変分積分器と,ガウス過程の回帰による残留力学の学習の組み合わせを提案する。
我々は、既知のキネマティック制約を持つシステムへのアプローチを拡張し、予測の不確実性に関する公式な境界を提供する。
論文 参考訳（メタデータ） (2021-12-10T11:09:29Z) - Stochastically forced ensemble dynamic mode decomposition for
forecasting and analysis of near-periodic systems [65.44033635330604]
本稿では,観測力学を強制線形系としてモデル化した新しい負荷予測手法を提案する。
固有線型力学の利用は、解釈可能性やパーシモニーの観点から、多くの望ましい性質を提供することを示す。
電力グリッドからの負荷データを用いたテストケースの結果が提示される。
論文 参考訳（メタデータ） (2020-10-08T20:25:52Z) - Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
状態遷移が既知の状態-作用対の特徴埋め込みに線形に依存する非線形力学系のクラスについて検討する。
そこで本稿では, トラジェクティブ・プランニング, トラジェクティブ・トラッキング, システムの再推定という3つのステップを繰り返すことで, この問題を解決するためのアクティブ・ラーニング・アプローチを提案する。
本手法は, 非線形力学系を標準線形回帰の統計速度と同様, パラメトリック速度で推定する。
論文 参考訳（メタデータ） (2020-06-18T04:54:11Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。