論文の概要: Learning Algorithms for Verification of Markov Decision Processes
- arxiv url: http://arxiv.org/abs/2403.09184v3
- Date: Tue, 05 Nov 2024 09:51:16 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-11-06 14:55:47.684112
- Title: Learning Algorithms for Verification of Markov Decision Processes
- Title（参考訳）: マルコフ決定過程の検証のための学習アルゴリズム
- Authors: Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Křetínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, Mateusz Ujma,
- Abstract要約: マルコフ決定過程(MDP)の検証に学習アルゴリズムを適用するための一般的な枠組みを提案する。
提案するフレームワークは,検証における中核的な問題である確率的到達性に重点を置いている。
- 参考スコア（独自算出の注目度）: 20.5951492453299
- License:
- Abstract: We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{\'{a}}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.
- Abstract（参考訳）: 本稿では,マルコフ決定過程(MDP)の検証に学習アルゴリズムとヒューリスティックガイダンスを適用するための一般的なフレームワークを提案する。
我々の技術の主な目的は、状態空間の徹底的な探索を避けることによる性能向上であり、代わりにヒューリスティックスによって導かれるシステムの特に関連する領域に焦点を当てることである。
我々の研究は、Br{\'{a}}zdil et al の以前の結果に基づいており、それを著しく拡張し、いくつかの詳細を精査し、エラーを修正しました。
提案するフレームワークは,検証における中核的な問題である確率的到達性に注目し,二つの異なるシナリオでインスタンス化される。
第一に、MDPの完全な知識、特に正確な遷移確率が利用できると仮定する。
モデルに対するヒューリスティック駆動による部分探索を行い、要求される確率の正確な下限と上限を導出する。
2つ目は、正確な遷移ダイナミクスを知らずにMDPをサンプリングできるケースに取り組みます。
ここでは、下界と上界の両方の観点からも確率的保証を得、近似の効率的な停止基準を提供する。
特に後者は、MDPの非有界特性に対する統計モデル検査(SMC)の拡張である。
他の関連するアプローチとは対照的に、時間有界(有限水平)や割引特性への注意を制限したり、MDPの特定の構造特性を仮定したりしない。
関連論文リスト
- Sound Heuristic Search Value Iteration for Undiscounted POMDPs with Reachability Objectives [16.101435842520473]
本稿では,POMDPにおける最大到達可能性確率問題(indefinite-horizon)と呼ばれる問題について検討する。
割引問題に対するポイントベース手法の成功に触発され,MRPPへの拡張について検討した。
本稿では,これらの手法の強みを有効活用し,信念空間を効率的に探索するアルゴリズムを提案する。
論文 参考訳（メタデータ） (2024-06-05T02:33:50Z) - What Are the Odds? Improving the foundations of Statistical Model Checking [3.789219860006095]
マルコフ決定プロセス(MDP)は不確実性の下での意思決定の基本的なモデルである。
従来の検証アルゴリズムは、MDPの振る舞いを管理する確率の正確な知識を前提としている。
我々はMDPの知識を活用する専門的なアプローチを提案する。
論文 参考訳（メタデータ） (2024-04-08T11:47:46Z) - Efficient Model-Free Exploration in Low-Rank MDPs [76.87340323826945]
低ランクマルコフ決定プロセスは、関数近似を持つRLに対して単純だが表現力のあるフレームワークを提供する。
既存のアルゴリズムは、(1)計算的に抽出可能であるか、または(2)制限的な統計的仮定に依存している。
提案手法は,低ランクMPPの探索のための最初の実証可能なサンプル効率アルゴリズムである。
論文 参考訳（メタデータ） (2023-07-08T15:41:48Z) - Provably Efficient UCB-type Algorithms For Learning Predictive State
Representations [55.00359893021461]
逐次決定問題は、予測状態表現(PSR)によってモデル化された低ランク構造が認められる場合、統計的に学習可能である
本稿では,推定モデルと実モデル間の全変動距離を上限とする新しいボーナス項を特徴とする,PSRに対する最初のUCB型アプローチを提案する。
PSRに対する既存のアプローチとは対照的に、UCB型アルゴリズムは計算的トラクタビリティ、最優先の準最適ポリシー、モデルの精度が保証される。
論文 参考訳（メタデータ） (2023-07-01T18:35:21Z) - PAC Statistical Model Checking of Mean Payoff in Discrete- and
Continuous-Time MDP [0.34410212782758043]
我々は,未知のMDPにおいて,平均ペイオフをほぼ正確に計算する最初のアルゴリズムを提供する。
状態空間に関する知識は一切必要とせず、最小遷移確率の低い境界のみである。
提案アルゴリズムは, ほぼ正しいPAC境界を提供するだけでなく, 標準ベンチマークで実験を行うことにより, その実用性を実証する。
論文 参考訳（メタデータ） (2022-06-03T09:13:27Z) - Reinforcement Learning with a Terminator [80.34572413850186]
我々は, TerMDP のパラメータを学習し, 推定問題の構造を活用し, 状態ワイドな信頼境界を提供する。
我々はこれらを用いて証明可能な効率のよいアルゴリズムを構築し、終端を考慮し、その後悔を抑える。
論文 参考訳（メタデータ） (2022-05-30T18:40:28Z) - Regret Analysis in Deterministic Reinforcement Learning [78.31410227443102]
本稿では,最適学習アルゴリズムの分析と設計の中心となる後悔の問題を考察する。
本稿では,システムパラメータに明示的に依存する対数問題固有の後悔の下位境界について述べる。
論文 参考訳（メタデータ） (2021-06-27T23:41:57Z) - Minimum-Delay Adaptation in Non-Stationary Reinforcement Learning via
Online High-Confidence Change-Point Detection [7.685002911021767]
非定常環境におけるポリシーを効率的に学習するアルゴリズムを導入する。
これは、リアルタイム、高信頼な変更点検出統計において、潜在的に無限のデータストリームと計算を解析する。
i) このアルゴリズムは, 予期せぬ状況変化が検出されるまでの遅延を最小限に抑え, 迅速な応答を可能にする。
論文 参考訳（メタデータ） (2021-05-20T01:57:52Z) - Incremental Verification of Fixed-Point Implementations of Neural
Networks [0.19573380763700707]
インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
論文 参考訳（メタデータ） (2020-12-21T10:03:44Z) - Amortized Conditional Normalized Maximum Likelihood: Reliable Out of
Distribution Uncertainty Estimation [99.92568326314667]
本研究では,不確実性推定のための拡張性のある汎用的アプローチとして,償却条件正規化最大値(ACNML)法を提案する。
提案アルゴリズムは条件付き正規化最大度(CNML)符号化方式に基づいており、最小記述長の原理に従って最小値の最適特性を持つ。
我々は、ACNMLが、分布外入力のキャリブレーションの観点から、不確実性推定のための多くの手法と好意的に比較することを示した。
論文 参考訳（メタデータ） (2020-11-05T08:04:34Z) - Adaptive Sampling for Best Policy Identification in Markov Decision
Processes [79.4957965474334]
本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。
最先端アルゴリズムの利点を論じ、解説する。
論文 参考訳（メタデータ） (2020-09-28T15:22:24Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。