論文の概要: Convex Optimization for Parameter Synthesis in MDPs

• arxiv url: http://arxiv.org/abs/2107.00108v1
• Date: Wed, 30 Jun 2021 21:23:56 GMT
• ステータス: 処理完了
• システム内更新日: 2021-07-02 13:34:33.054479
• Title: Convex Optimization for Parameter Synthesis in MDPs
• Title（参考訳）: MDPにおけるパラメータ合成のための凸最適化
• Authors: Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu
• Abstract要約: 確率論的モデル検査は、マルコフ決定プロセスが時間論理の仕様を満たすかどうかを証明することを目的としている。 我々は、局所最適実行時ソリューションを反復的に得る2つのアプローチを開発する。 数十万のパラメータを持つ衛星パラメータ合成問題に対するアプローチと,その拡張性を,広く使用されているベンチマーク上で実証する。
• 参考スコア（独自算出の注目度）: 19.808494349302784
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Probabilistic model checking aims to prove whether a Markov decision process (MDP) satisfies a temporal logic specification. The underlying methods rely on an often unrealistic assumption that the MDP is precisely known. Consequently, parametric MDPs (pMDPs) extend MDPs with transition probabilities that are functions over unspecified parameters. The parameter synthesis problem is to compute an instantiation of these unspecified parameters such that the resulting MDP satisfies the temporal logic specification. We formulate the parameter synthesis problem as a quadratically constrained quadratic program (QCQP), which is nonconvex and is NP-hard to solve in general. We develop two approaches that iteratively obtain locally optimal solutions. The first approach exploits the so-called convex-concave procedure (CCP), and the second approach utilizes a sequential convex programming (SCP) method. The techniques improve the runtime and scalability by multiple orders of magnitude compared to black-box CCP and SCP by merging ideas from convex optimization and probabilistic model checking. We demonstrate the approaches on a satellite collision avoidance problem with hundreds of thousands of states and tens of thousands of parameters and their scalability on a wide range of commonly used benchmarks.
• Abstract（参考訳）: 確率論的モデル検査は、マルコフ決定プロセス(MDP)が時間論理仕様を満たすかどうかを証明することを目的としている。 基礎となる手法は、MDPが正確に知られているというしばしば非現実的な仮定に依存している。 その結果、パラメトリックMDP(pMDP)は、不特定パラメータ上の関数である遷移確率でMDPを拡張する。 パラメータ合成問題は、その結果のMDPが時間論理仕様を満たすように、これらの未特定パラメータのインスタンス化を計算することである。 パラメータ合成問題を2次制約付き二次プログラム(QCQP)として定式化する。 局所最適解を反復的に得る2つのアプローチを開発する。 第一のアプローチは、いわゆる凸凹法(CCP)を利用し、第二のアプローチはシーケンシャル凸計画法(SCP)を用いる。 この技術は、凸最適化と確率モデルチェックのアイデアを融合させることにより、ブラックボックスCCPやSCPと比較して、ランタイムとスケーラビリティを桁違いに改善する。 我々は,数十万の状態と数万のパラメータを持つ衛星衝突回避問題に対するアプローチと,その拡張性について,広く使用されるベンチマークで実証する。

関連論文リスト

• Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting [5.552645730505715]
  2つの中核的な課題は、DPアルゴリズムの分布の表現的でコンパクトで効率的な符号化を見つけることである。 プライバシーと正確性に縛られた合成法を開発することで、最初の課題に対処する。 DPアルゴリズムに固有の対称性を活用するためのフレームワークを開発する。
  論文  参考訳（メタデータ） (2024-02-26T19:29:46Z)
• Fast, Scalable, Warm-Start Semidefinite Programming with Spectral Bundling and Sketching [53.91395791840179]
  我々は、大規模なSDPを解くための、証明可能な正確で高速でスケーラブルなアルゴリズムであるUnified Spectral Bundling with Sketching (USBS)を提案する。 USBSは、20億以上の決定変数を持つインスタンス上で、最先端のスケーラブルなSDP解決器よりも500倍のスピードアップを提供する。
  論文  参考訳（メタデータ） (2023-12-19T02:27:22Z)
• QSlack: A slack-variable approach for variational quantum semi-definite programming [5.0579795245991495]
  量子コンピュータは、最もよく知られた古典的アルゴリズムのスピードアップを提供することができる。 半定値および線形プログラムを含む最適化問題の解法を示す。 これらの問題に対する予備問題と双対問題の両方の実装が、基礎的真理に近づいていることが示される。
  論文  参考訳（メタデータ） (2023-12-06T19:00:01Z)
• Numerical Methods for Convex Multistage Stochastic Optimization [86.45244607927732]
  最適化プログラミング(SP)、最適制御(SOC)、決定プロセス(MDP)に焦点を当てる。 凸多段マルコフ問題の解決の最近の進歩は、動的プログラミング方程式のコスト対ゴー関数の切断面近似に基づいている。 切削平面型法は多段階問題を多段階的に扱えるが、状態(決定)変数は比較的少ない。
  論文  参考訳（メタデータ） (2023-03-28T01:30:40Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  マルコフジャンプ線形系に対する制御器の合成法を提案する。 本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。 本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
  論文  参考訳（メタデータ） (2022-12-01T17:36:30Z)
• Efficient semidefinite bounds for multi-label discrete graphical models [6.226454551201676]
  このようなモデルにおける主要なクエリの1つは、Posteri(MAP)ネットワークのコストに関するSDPWCSP関数を特定することである。 従来の二重化制約手法と,行ごとの更新に基づく専用SDP/Monteiroスタイルの手法を検討する。
  論文  参考訳（メタデータ） (2021-11-24T13:38:34Z)
• STRIDE along Spectrahedral Vertices for Solving Large-Scale Rank-One Semidefinite Relaxations [27.353023427198806]
  我々は、制約のない最適化問題(POP)の高次半定値プログラミング緩和を考察する。 POPから独立してSDPを解く既存のアプローチは、そのようなSDPの典型的な非エネルギー性のため、大きな問題にスケールできないか、あるいは緩やかな収束に苦しむことができない。 我々は SpecTrahedral vErtices (STRIDE) と呼ばれる新しいアルゴリズムフレームワークを提案する。
  論文  参考訳（メタデータ） (2021-05-28T18:07:16Z)
• Two-Stage Stochastic Optimization via Primal-Dual Decomposition and Deep Unrolling [86.85697555068168]
  2段階のアルゴリズム最適化は、様々な工学や科学的応用において重要な役割を果たす。 特に長期変数と短期変数が制約の中で結合されている場合、アルゴリズムは効率的ではない。 PDD-SSCAが既存のソリューションよりも優れたパフォーマンスを達成できることを示します。
  論文  参考訳（メタデータ） (2021-05-05T03:36:00Z)
• Parallel Stochastic Mirror Descent for MDPs [72.75921150912556]
  無限水平マルコフ決定過程(MDP)における最適政策学習の問題を考える。 リプシッツ連続関数を用いた凸プログラミング問題に対してミラー・ディクセントの変種が提案されている。 このアルゴリズムを一般の場合において解析し,提案手法の動作中に誤差を蓄積しない収束率の推定値を得る。
  論文  参考訳（メタデータ） (2021-02-27T19:28:39Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)

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

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