論文の概要: Formal Verification of Unknown Dynamical Systems via Gaussian Process
Regression
- arxiv url: http://arxiv.org/abs/2201.00655v1
- Date: Fri, 31 Dec 2021 05:10:05 GMT
- ステータス: 処理完了
- システム内更新日: 2022-01-04 15:18:02.418315
- Title: Formal Verification of Unknown Dynamical Systems via Gaussian Process
Regression
- Title(参考訳): ガウス過程回帰による未知力学系の形式的検証
- Authors: John Jackson, Luca Laurenti, Eric Frew, and Morteza Lahijanian
- Abstract要約: 本研究では,部分観測可能な離散時間力学系を検証するためのフレームワークを開発する。
連続空間系を有限状態で不確実なマルコフ決定過程として抽象化する。
フレームワークの複雑さはデータセットのサイズと離散的な抽象化にあることを示す。
- 参考スコア(独自算出の注目度): 3.674863913115432
- 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 article, we develop a framework for
verifying partially-observable, discrete-time dynamical systems with unmodelled
dynamics against temporal logic specifications from a given input-output
dataset. The verification framework employs Gaussian process (GP) regression to
learn the unknown dynamics from the dataset and abstract 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 to the underlying partially-observable 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。