論文の概要: Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions

• arxiv url: http://arxiv.org/abs/2311.09786v1
• Date: Thu, 16 Nov 2023 11:03:54 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-17 14:41:36.063437
• Title: Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions
• Title（参考訳）: 形式的抽象化による確率的・不確実な力学モデルの正しい構成制御
• Authors: Thom Badings (Radboud University), Nils Jansen (Radboud University), Licio Romao (University of Oxford), Alessandro Abate (University of Oxford)
• Abstract要約: 我々は、様々なモデリングの前提の下でこの問題を解決するために使用できる抽象フレームワークを開発する。 我々は、与えられた仕様を満たすための保証とともに、iMDPの最適ポリシーを計算するために最先端の検証技術を使用します。 そして、このポリシーを構築によって、これらの保証が動的モデルに受け継がれるフィードバックコントローラに改良できることを示します。
• 参考スコア（独自算出の注目度）: 44.99833362998488
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated synthesis of correct-by-construction controllers for autonomous systems is crucial for their deployment in safety-critical scenarios. Such autonomous systems are naturally modeled as stochastic dynamical models. The general problem is to compute a controller that provably satisfies a given task, represented as a probabilistic temporal logic specification. However, factors such as stochastic uncertainty, imprecisely known parameters, and hybrid features make this problem challenging. We have developed an abstraction framework that can be used to solve this problem under various modeling assumptions. Our approach is based on a robust finite-state abstraction of the stochastic dynamical model in the form of a Markov decision process with intervals of probabilities (iMDP). We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model. In this short paper, we survey our recent research in this area and highlight two challenges (related to scalability and dealing with nonlinear dynamics) that we aim to address with our ongoing research.
• Abstract（参考訳）: 自律システムのための正しい構成制御器の自動合成は、安全クリティカルなシナリオへの展開に不可欠である。 このような自律システムは自然に確率力学モデルとしてモデル化される。 一般的な問題は、確率論的時相論理仕様として表される与えられたタスクを確実に満足するコントローラを計算することである。 しかし、確率的不確実性、不正確なパラメータ、ハイブリッド特徴などの要因がこの問題を難しくしている。 我々は,様々なモデリング仮定の下でこの問題を解決するための抽象化フレームワークを開発した。 我々のアプローチは確率的力学モデルの頑健な有限状態抽象化を確率の間隔(iMDP)を持つマルコフ決定過程の形で基礎としている。 我々は、与えられた仕様を満たすための保証とともに、iMDPの最適ポリシーを計算するために最先端の検証技術を使用する。 次に、このポリシーを設計することで、これらの保証が動的モデルに受け継がれるフィードバックコントローラに洗練することができることを示す。 本稿では,本分野における最近の研究を概観し,現在進行中の研究に対処することを目的とした2つの課題(スケーラビリティと非線形力学への対応)を取り上げる。

関連論文リスト

• 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)
• Reduced order modeling of parametrized systems through autoencoders and SINDy approach: continuation of periodic solutions [0.0]
  本研究は,ROM構築と動的識別の低減を組み合わせたデータ駆動型非侵入型フレームワークを提案する。 提案手法は、非線形力学(SINDy)のパラメトリックスパース同定によるオートエンコーダニューラルネットワークを利用して、低次元力学モデルを構築する。 これらは、システムパラメータの関数として周期的定常応答の進化を追跡し、過渡位相の計算を避け、不安定性と分岐を検出することを目的としている。
  論文  参考訳（メタデータ） (2022-11-13T01:57:18Z)
• Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty [68.00748155945047]
  複雑な力学系のモデルにおける不確実性を捉えることは、安全なコントローラの設計に不可欠である。 いくつかのアプローチでは、安全と到達可能性に関する時間的仕様を満たすポリシーを形式的な抽象化を用いて合成する。 我々の貢献は、ノイズ、不確実なパラメータ、外乱を含む連続状態モデルに対する新しい抽象的制御法である。
  論文  参考訳（メタデータ） (2022-10-12T07:57:03Z)
• Sample Complexity of Robust Reinforcement Learning with a Generative Model [0.0]
  本稿では,モデルに基づく強化学習(RL)アルゴリズムを提案する。 我々は,全変動距離,カイ二乗発散,KL発散の3種類の不確実性集合を考察した。 この結果に加えて,ロバストポリシの利点に関する公式な分析的議論も提示する。
  論文  参考訳（メタデータ） (2021-12-02T18:55:51Z)
• Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems [8.833548357664606]
  我々は、離散時間マルコフ連鎖(DTMC)として定義されるシステムにおける対向的堅牢性のための公式な枠組みを開発する。 我々は、元の遷移確率の周囲に$varepsilon$ボールで制約された、敵がシステム遷移を摂動できる脅威モデルのクラスを概説する。
  論文  参考訳（メタデータ） (2021-10-05T15:52:47Z)
• Probabilistic robust linear quadratic regulators with Gaussian processes [73.0364959221845]
  ガウス過程(GP)のような確率モデルは、制御設計に続く使用のためのデータから未知の動的システムを学ぶための強力なツールです。 本稿では、確率的安定性マージンに関して堅牢なコントローラを生成する線形化GPダイナミクスのための新しいコントローラ合成について述べる。
  論文  参考訳（メタデータ） (2021-05-17T08:36:18Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。