論文の概要: Formal Verification of Stochastic Systems with ReLU Neural Network
Controllers
- arxiv url: http://arxiv.org/abs/2103.05142v1
- Date: Mon, 8 Mar 2021 23:53:13 GMT
- ステータス: 処理完了
- システム内更新日: 2021-03-10 14:43:38.635542
- Title: Formal Verification of Stochastic Systems with ReLU Neural Network
Controllers
- Title（参考訳）: ReLUニューラルネットワークコントローラによる確率システムの形式的検証
- Authors: Shiqi Sun, Yan Zhang, Xusheng Luo, Panagiotis Vlantis, Miroslav Pajic
and Michael M. Zavlanos
- Abstract要約: reluニューラルネットワーク(nn)コントローラを備えたサイバーフィジカルシステムの形式的安全性検証の問題に対処する。
私たちの目標は、所定の自信を持って、システムが安全でない構成に達しない初期状態のセットを見つけることです。
- 参考スコア（独自算出の注目度）: 22.68044012584378
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this work, we address the problem of formal safety verification for
stochastic cyber-physical systems (CPS) equipped with ReLU neural network (NN)
controllers. Our goal is to find the set of initial states from where, with a
predetermined confidence, the system will not reach an unsafe configuration
within a specified time horizon. Specifically, we consider discrete-time LTI
systems with Gaussian noise, which we abstract by a suitable graph. Then, we
formulate a Satisfiability Modulo Convex (SMC) problem to estimate upper bounds
on the transition probabilities between nodes in the graph. Using this
abstraction, we propose a method to compute tight bounds on the safety
probabilities of nodes in this graph, despite possible over-approximations of
the transition probabilities between these nodes. Additionally, using the
proposed SMC formula, we devise a heuristic method to refine the abstraction of
the system in order to further improve the estimated safety bounds. Finally, we
corroborate the efficacy of the proposed method with simulation results
considering a robot navigation example and comparison against a
state-of-the-art verification scheme.
- Abstract（参考訳）: 本研究では、ReLUニューラルネットワーク(NN)コントローラを備えた確率的サイバー物理システム(CPS)の安全性検証に関する問題に対処する。
私たちの目標は、所定の自信を持って、システムが指定された時間圏内に安全でない構成に達しない初期状態のセットを見つけることです。
具体的には、ガウス雑音を持つ離散時間LTIシステムについて検討し、適切なグラフで抽象化する。
次に、SMC(Satisfiability Modulo Convex)問題を定式化し、グラフ内のノード間の遷移確率上の上限を推定します。
この抽象化を用いて、ノード間の遷移確率の過剰な近似にもかかわらず、このグラフにおけるノードの安全性確率の厳密な境界を計算する手法を提案する。
さらに,提案したSMC式を用いて,システムの抽象化を改良するヒューリスティック手法を考案し,推定安全境界をさらに改善する。
最後に,提案手法の有効性と,ロボットナビゲーションの例と最新の検証手法との比較を検討したシミュレーション結果とを相関させる。
関連論文リスト
- Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳（メタデータ） (2024-03-15T17:32:02Z) - Sub-linear Regret in Adaptive Model Predictive Control [56.705978425244496]
本稿では,STT-MPC (Self-Tuning tube-based Model Predictive Control) について述べる。
システム力学を最初に認識したアルゴリズムと比較して,アルゴリズムの後悔を解析する。
論文 参考訳（メタデータ） (2023-10-07T15:07:10Z) - Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal
Abstractions [59.605246463200736]
雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。
まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。
我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
論文 参考訳（メタデータ） (2023-01-04T10:40:30Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。
本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。
本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文 参考訳（メタデータ） (2022-12-01T17:36:30Z) - Risk Verification of Stochastic Systems with Neural Network Controllers [0.0]
ニューラルネットワーク(NN)コントローラを用いた動的システムのリスク検証のための,データ駆動型フレームワークを提案する。
制御システム,NNコントローラ,トレースロバスト性の概念を備えた仕様が与えられた場合,システムからトラジェクトリを収集する。
NNコントローラが仕様を満たさないリスクを推定するために、これらのロバストネス値のリスクメトリクスを計算します。
論文 参考訳（メタデータ） (2022-08-26T20:09:55Z) - Large-Scale Sequential Learning for Recommender and Engineering Systems [91.3755431537592]
本稿では,現在の状況に適応してパーソナライズされたランキングを提供する自動アルゴリズムの設計に焦点を当てる。
前者はSAROSと呼ばれる新しいアルゴリズムを提案し,インタラクションの順序を学習するためのフィードバックの種類を考慮に入れている。
提案手法は, 電力網の故障検出に対する初期アプローチと比較して, 統計的に有意な結果を示す。
論文 参考訳（メタデータ） (2022-05-13T21:09:41Z) - Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian
Noise [59.47042225257565]
雑音分布の明示的な表現に依存しない新しい計画法を提案する。
まず、連続系を離散状態モデルに抽象化し、状態間の確率的遷移によってノイズを捕捉する。
いわゆる区間マルコフ決定過程(iMDP)の遷移確率区間におけるこれらの境界を捉える。
論文 参考訳（メタデータ） (2021-10-25T06:18:55Z) - Correct-by-construction reach-avoid control of partially observable
linear stochastic systems [7.912008109232803]
離散時間線形時間不変系のリーチエイド制御のための頑健なフィードバックコントローラを定式化する。
問題は、必要となる証明状態の抽象化問題を満たすコントローラを計算することである。
論文 参考訳（メタデータ） (2021-03-03T13:46:52Z) - Gaussian Process-based Min-norm Stabilizing Controller for
Control-Affine Systems with Uncertain Input Effects and Dynamics [90.81186513537777]
本稿では,この問題の制御・アフィン特性を捉えた新しい化合物カーネルを提案する。
この結果の最適化問題は凸であることを示し、ガウス過程に基づく制御リャプノフ関数第二次コーンプログラム(GP-CLF-SOCP)と呼ぶ。
論文 参考訳（メタデータ） (2020-11-14T01:27:32Z) - Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural
Network Controllers via Semidefinite Programming [19.51345816555571]
本稿では,ニューラルネットワークを用いた線形時間変化システムの安全性検証のための新しいフォワードリーチビリティ解析手法を提案する。
半有限計画法を用いて、これらの近似到達可能な集合を計算できることが示される。
提案手法は,まずディープニューラルネットワークを用いて非線形モデル予測制御器を近似し,その解析ツールを用いて閉ループシステムの有限時間到達性と制約満足度を証明した。
論文 参考訳（メタデータ） (2020-04-16T18:48:25Z) - Closed-loop Parameter Identification of Linear Dynamical Systems through
the Lens of Feedback Channel Coding Theory [0.0]
本稿では,ガウス過程雑音を伴う線形スカラー系の閉ループ同定の問題について考察する。
学習速度は,対応するAWGNチャネルの容量によって基本的に上界にあることを示す。
フィードバックポリシの最適設計は依然として難しいが、上限が達成される条件を導出する。
論文 参考訳（メタデータ） (2020-03-27T17:30:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。