論文の概要: Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning

• arxiv url: http://arxiv.org/abs/2004.00273v2
• Date: Wed, 22 Apr 2020 02:21:22 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-17 18:01:14.530074
• Title: Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning
• Title（参考訳）: 強化学習によるマルコフ決定過程におけるpctl仕様の統計的モデル検証
• Authors: Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir E. Dullerud
• Abstract要約: 我々は,その誤差を証明可能な保証付き統計モデル検査法(SMC)を開発した。 具体的には、まず、上限密度バウンド(UCB)ベースのQラーニングを用いて、有界時間PCTL仕様のためのSMCアルゴリズムを設計する。 次に、このアルゴリズムを未有有界時間仕様に拡張し、適切なトランケーション時間を特定する。
• 参考スコア（独自算出の注目度）: 3.9908690878308684
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model checking PCTL specifications statistically on Markov Decision Processes (MDPs) by sampling, e.g., checking whether there exists a feasible policy such that the probability of reaching certain goal states is greater than a threshold. We use reinforcement learning to search for such a feasible policy for PCTL specifications, and then develop a statistical model checking (SMC) method with provable guarantees on its error. Specifically, we first use upper-confidence-bound (UCB) based Q-learning to design an SMC algorithm for bounded-time PCTL specifications, and then extend this algorithm to unbounded-time specifications by identifying a proper truncation time by checking the PCTL specification and its negation at the same time. Finally, we evaluate the proposed method on case studies.
• Abstract（参考訳）: PCTL(Probabilistic Computation Tree Logic)は、確率的到達可能性や安全性などの制御目的を正式に指定するために頻繁に使用される。 本研究は,マルコフ決定過程(MDP)を統計的に検証し,例えば,ある目標状態に達する確率がしきい値より大きいような実行可能なポリシーが存在するかどうかを確認することに焦点を当てる。 我々は強化学習を用いてPCTL仕様に対するそのような実行可能なポリシーを探索し、その誤りを証明可能な保証付き統計モデル検査(SMC)手法を開発する。 具体的には、まず、上位信頼度(UCB)ベースのQラーニングを用いて、有界時間PCTL仕様のためのSMCアルゴリズムを設計し、PCTL仕様と否定を同時に確認することで、適切なトランケーション時間を特定することにより、このアルゴリズムを非有界時間仕様に拡張する。 最後に,本提案手法をケーススタディで評価する。

関連論文リスト

• Probabilistic Model Checking of Stochastic Reinforcement Learning Policies [5.923818043882103]
  本稿では,強化学習(RL)ポリシーを検証する手法を提案する。 このアプローチは、アルゴリズムとその対応する環境がMarkovプロパティに一括して準拠する限り、任意のRLアルゴリズムと互換性がある。 その結果,本手法はRLポリシーの検証に適していることがわかった。
  論文  参考訳（メタデータ） (2024-03-27T16:15:21Z)
• Learning Algorithms for Verification of Markov Decision Processes [20.5951492453299]
  マルコフ決定過程(MDP)の検証に学習アルゴリズムを適用するための一般的な枠組みを提案する。 提案するフレームワークは,検証における中核的な問題である確率的到達性に重点を置いている。
  論文  参考訳（メタデータ） (2024-03-14T08:54:19Z)
• Score Matching-based Pseudolikelihood Estimation of Neural Marked Spatio-Temporal Point Process with Uncertainty Quantification [59.81904428056924]
  我々は、不確実な定量化を伴うmarkPsを学習するためのスコアMAtching推定器であるSMASHを紹介する。 具体的には,スコアマッチングによるマークPsの擬似的類似度を推定することにより,正規化自由度を推定する。 提案手法の優れた性能は、事象予測と不確実性定量化の両方において広範な実験によって実証される。
  論文  参考訳（メタデータ） (2023-10-25T02:37:51Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。 まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。 我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
  論文  参考訳（メタデータ） (2023-01-04T10:40:30Z)
• Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes [4.279881803310469]
  Signal Temporal Logic (STL) で与えられたプロセスと豊富な仕様をサポートする最初のPM法である textitquantitative predictive monitoring (QPM) を導入する。 QPMは、$phi$の量的(いわゆる頑健な)STLセマンティクスを予測することで満足度を定量的に測定する。 合成式を扱うために,我々のモニタをどのように構成的に組み合わせることができるかを示す。
  論文  参考訳（メタデータ） (2022-11-04T11:08:29Z)
• Robust Anytime Learning of Markov Decision Processes [8.799182983019557]
  データ駆動型アプリケーションでは、限られたデータから正確な確率を導き出すと統計的エラーが発生する。 不確実なMDP(uMDP)は正確な確率を必要としないが、遷移においていわゆる不確実性集合を用いる。 本稿では,ベイズ的推論スキームとロバストポリシーの計算を組み合わせた,頑健な任意の時間学習手法を提案する。
  論文  参考訳（メタデータ） (2022-05-31T14:29:55Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  雑音分布の明示的な表現に依存しない新しい計画法を提案する。 まず、連続系を離散状態モデルに抽象化し、状態間の確率的遷移によってノイズを捕捉する。 いわゆる区間マルコフ決定過程(iMDP)の遷移確率区間におけるこれらの境界を捉える。
  論文  参考訳（メタデータ） (2021-10-25T06:18:55Z)
• Model-Free Learning of Safe yet Effective Controllers [11.876140218511157]
  私達はまた有効な安全な制御方針を学ぶ問題を研究します。 まず,安全を確保する確率を最大化する方針を学習するモデルフリー強化学習アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2021-03-26T17:05:12Z)
• Identification of Unexpected Decisions in Partially Observable Monte-Carlo Planning: a Rule-Based Approach [78.05638156687343]
  本稿では,POMCPポリシーをトレースを検査して分析する手法を提案する。 提案手法は, 政策行動の局所的特性を探索し, 予期せぬ決定を識別する。 我々は,POMDPの標準ベンチマークであるTigerに対するアプローチと,移動ロボットナビゲーションに関する現実の問題を評価した。
  論文  参考訳（メタデータ） (2020-12-23T15:09:28Z)
• Amortized Conditional Normalized Maximum Likelihood: Reliable Out of Distribution Uncertainty Estimation [99.92568326314667]
  本研究では,不確実性推定のための拡張性のある汎用的アプローチとして,償却条件正規化最大値(ACNML)法を提案する。 提案アルゴリズムは条件付き正規化最大度(CNML)符号化方式に基づいており、最小記述長の原理に従って最小値の最適特性を持つ。 我々は、ACNMLが、分布外入力のキャリブレーションの観点から、不確実性推定のための多くの手法と好意的に比較することを示した。
  論文  参考訳（メタデータ） (2020-11-05T08:04:34Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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