論文の概要: Formal Methods for Autonomous Systems
- arxiv url: http://arxiv.org/abs/2311.01258v1
- Date: Thu, 2 Nov 2023 14:18:43 GMT
- ステータス: 処理完了
- システム内更新日: 2023-11-03 13:10:00.373307
- Title: Formal Methods for Autonomous Systems
- Title（参考訳）: 自律システムのための形式的手法
- Authors: Tichakorn Wongpiromsarn, Mahsa Ghasemi, Murat Cubuktepe, Georgios
Bakirtzis, Steven Carr, Mustafa O. Karabag, Cyrus Neary, Parham Gohari, Ufuk
Topcu
- Abstract要約: 形式的手法は安全クリティカルシステムの正当性を確立する上で重要な役割を果たしてきた。
形式的なメソッドの主なビルディングブロックはモデルと仕様です。
様々な定式化の下で, 正しい構成合成を考察する。
- 参考スコア（独自算出の注目度）: 21.989467515686858
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal methods refer to rigorous, mathematical approaches to system
development and have played a key role in establishing the correctness of
safety-critical systems. The main building blocks of formal methods are models
and specifications, which are analogous to behaviors and requirements in system
design and give us the means to verify and synthesize system behaviors with
formal guarantees.
This monograph provides a survey of the current state of the art on
applications of formal methods in the autonomous systems domain. We consider
correct-by-construction synthesis under various formulations, including closed
systems, reactive, and probabilistic settings. Beyond synthesizing systems in
known environments, we address the concept of uncertainty and bound the
behavior of systems that employ learning using formal methods. Further, we
examine the synthesis of systems with monitoring, a mitigation technique for
ensuring that once a system deviates from expected behavior, it knows a way of
returning to normalcy. We also show how to overcome some limitations of formal
methods themselves with learning. We conclude with future directions for formal
methods in reinforcement learning, uncertainty, privacy, explainability of
formal methods, and regulation and certification.
- Abstract（参考訳）: 形式的手法はシステム開発に対する厳密で数学的アプローチであり、安全クリティカルシステムの正確性を確立する上で重要な役割を果たしてきた。
形式的手法の主な構成要素はモデルと仕様であり、それはシステム設計における振る舞いや要求に類似しており、形式的保証付きシステム動作の検証と合成の手段を与えてくれる。
このモノグラフは、自律システム領域における形式的手法の適用に関する現在の技術に関する調査を提供する。
我々は, 閉じたシステム, 反応性, 確率的設定など, 様々な定式化の下で正しい構成合成を考える。
既知の環境におけるシステムを合成するだけでなく、不確実性の概念と形式的手法を用いた学習を取り入れるシステムの振る舞いについても論じる。
さらに,監視によるシステム合成,予測行動から逸脱したシステムが正常な状態に戻る方法を知っていることを保証するための緩和手法について検討する。
また,形式的手法自体の制限を学習によって克服する方法を示す。
我々は、強化学習、不確実性、プライバシー、形式的手法の説明可能性、規制と認定における形式的手法の今後の方向性を結論づける。
関連論文リスト
- Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳（メタデータ） (2024-03-15T17:32:02Z) - Towards Formal Fault Injection for Safety Assessment of Automated
Systems [0.0]
本稿では,開発ライフサイクルを通じてこれら2つのテクニックを融合したフォーマルなフォールトインジェクションを紹介する。
我々は,形式的手法と断層注入の相互支援の5つの領域を同定し,より密着的なアプローチを提唱する。
論文 参考訳（メタデータ） (2023-11-16T11:34:18Z) - Interactive System-wise Anomaly Detection [66.3766756452743]
異常検出は様々なアプリケーションにおいて基本的な役割を果たす。
既存のメソッドでは、インスタンスがデータとして容易に観察できないシステムであるシナリオを扱うのが難しい。
システム埋め込みを学習するエンコーダデコーダモジュールを含むエンドツーエンドアプローチを開発する。
論文 参考訳（メタデータ） (2023-04-21T02:20:24Z) - Learning-Based Optimal Control with Performance Guarantees for Unknown Systems with Latent States [4.4820711784498]
本稿では,潜在状態を持つ未知非線形系に対する最適入力軌道の計算法を提案する。
提案手法の有効性を数値シミュレーションで示す。
論文 参考訳（メタデータ） (2023-03-31T11:06:09Z) - Recursively Feasible Probabilistic Safe Online Learning with Control
Barrier Functions [63.18590014127461]
本稿では,CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
本研究では,ロバストな安全クリティカルコントローラの実現可能性について検討する。
次に、これらの条件を使って、イベントトリガーによるオンラインデータ収集戦略を考案します。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。
本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
論文 参考訳（メタデータ） (2022-01-28T16:53:56Z) - Structure-Preserving Learning Using Gaussian Processes and Variational
Integrators [62.31425348954686]
本稿では,機械系の古典力学に対する変分積分器と,ガウス過程の回帰による残留力学の学習の組み合わせを提案する。
我々は、既知のキネマティック制約を持つシステムへのアプローチを拡張し、予測の不確実性に関する公式な境界を提供する。
論文 参考訳（メタデータ） (2021-12-10T11:09:29Z) - A Review of Formal Methods applied to Machine Learning [0.6853165736531939]
機械学習システムの検証の新たな分野に適用される最先端の形式的手法を検討します。
我々はまず,安全クリティカルな分野であるavionic softwareにおいて確立された形式的手法とその現状を思い出す。
次に、機械学習のためにこれまでに開発された形式的手法を包括的かつ詳細にレビューし、その強みと限界を強調します。
論文 参考訳（メタデータ） (2021-04-06T12:48:17Z) - Proceedings Second Workshop on Formal Methods for Autonomous Systems [0.0]
FMASの目標は、正式な方法で自律システムの課題に取り組む先進的な研究者を集結させることだ。
私たちは、自律システムやロボットシステムを特定し、モデル化し、検証するための正式な方法を使うことに興味があります。
論文 参考訳（メタデータ） (2020-12-02T13:08:57Z) - Evaluating the Safety of Deep Reinforcement Learning Models using
Semi-Formal Verification [81.32981236437395]
本稿では,区間分析に基づく半形式的意思決定手法を提案する。
本手法は, 標準ベンチマークに比較して, 形式検証に対して比較結果を得る。
提案手法は, 意思決定モデルにおける安全性特性を効果的に評価することを可能にする。
論文 参考訳（メタデータ） (2020-10-19T11:18:06Z) - Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
状態遷移が既知の状態-作用対の特徴埋め込みに線形に依存する非線形力学系のクラスについて検討する。
そこで本稿では, トラジェクティブ・プランニング, トラジェクティブ・トラッキング, システムの再推定という3つのステップを繰り返すことで, この問題を解決するためのアクティブ・ラーニング・アプローチを提案する。
本手法は, 非線形力学系を標準線形回帰の統計速度と同様, パラメトリック速度で推定する。
論文 参考訳（メタデータ） (2020-06-18T04:54:11Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。