Fugu-MT 論文翻訳(概要): Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*

論文の概要: Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*

arxiv url: http://arxiv.org/abs/2209.02672v1
Date: Tue, 6 Sep 2022 17:36:28 GMT
ステータス: 処理完了
システム内更新日: 2022-09-07 15:15:09.676976
Title: Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*
Title（参考訳）: HyperPCTL*を用いたマルチエージェントシステムのベイズ統計モデル検査
Authors: Spandan Das and Pavithra Prabhakar
Abstract要約: 本稿では,離散時間マルコフ連鎖(DTMC)上のHyperPCTL*論理で定義された確率的ハイパープロパティの統計モデルチェック(SMC)のためのベイズ的手法を提案する。提案アルゴリズムは,与えられたHyperPCTL*の公式の満足度を推定するために必要なサンプル数と検証時間の両方において,より優れた性能を発揮する。
参考スコア（独自算出の注目度）: 6.574517227976925
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: In this paper, we present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs). While SMC of HyperPCTL* using sequential probability ratio test (SPRT) has been explored before, we develop an alternative SMC algorithm based on Bayesian hypothesis testing. In comparison to PCTL*, verifying HyperPCTL* formulae is complex owing to their simultaneous interpretation on multiple paths of the DTMC. In addition, extending the bottom-up model-checking algorithm of the non-probabilistic setting is not straight forward due to the fact that SMC does not return exact answers to the satisfiability problems of subformulae, instead, it only returns correct answers with high-confidence. We propose a recursive algorithm for SMC of HyperPCTL* based on a modified Bayes' test that factors in the uncertainty in the recursive satisfiability results. We have implemented our algorithm in a Python toolbox, HyProVer, and compared our approach with the SPRT based SMC. Our experimental evaluation demonstrates that our Bayesian SMC algorithm performs better both in terms of the verification time and the number of samples required to deduce satisfiability of a given HyperPCTL* formula.
Abstract（参考訳）: 本稿では,離散時間マルコフ連鎖(DTMC)上のHyperPCTL*論理で定義された確率的ハイパープロパティの統計モデル検査(SMC)について述べる。逐次確率比検定(SPRT)を用いたHyperPCTL*のSMCはこれまで検討されてきたが,ベイズ仮説を用いた代替SMCアルゴリズムを開発した。 PCTL*と比較して、DTMCの複数の経路を同時に解釈するため、HyperPCTL*式を検証することは複雑である。さらに、非確率的な設定のボトムアップモデルチェックアルゴリズムを拡張することは、smcがsubformulaeの充足可能性問題に対して正確な答えを返さないため、その代わりに、高い信頼度で正しい答えを返すだけである。本稿では,再帰的満足度の結果の不確かさを考慮に入れたベイズ試験に基づくHyperPCTL*のSMC再帰的アルゴリズムを提案する。我々はPythonのツールボックスHyProVerにアルゴリズムを実装し、SPRTベースのSMCと比較した。実験により, ベイジアンSMCアルゴリズムは, 与えられたHyperPCTL*の公式の満足度を推定するために必要なサンプル数と検証時間の両方において, 良好な性能を示すことが示された。

関連論文リスト

Online Variational Sequential Monte Carlo [49.97673761305336]
我々は,計算効率が高く正確なモデルパラメータ推定とベイジアン潜在状態推定を提供する変分連続モンテカルロ法(VSMC)を構築した。オンラインVSMCは、パラメータ推定と粒子提案適応の両方を効率よく、完全にオンザフライで実行することができる。
論文参考訳（メタデータ） (2023-12-19T21:45:38Z)
Bayesian Quantum State Tomography with Python's PyMC [0.0]
我々は,Python-3 のオープンソース PyMC 確率型プログラミングパッケージを用いて,複雑でない QST 最適化問題を単純な形式に変換する方法を示す。我々は,Python-3 のオープンソース PyMC 確率型プログラミングパッケージを用いて,複雑でない QST 最適化問題を単純な形式に変換する方法を示す。
論文参考訳（メタデータ） (2022-12-20T21:16:28Z)
Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文参考訳（メタデータ） (2022-12-01T17:36:30Z)
Fully Stochastic Trust-Region Sequential Quadratic Programming for Equality-Constrained Optimization Problems [62.83783246648714]
目的と決定論的等式制約による非線形最適化問題を解くために,逐次2次プログラミングアルゴリズム(TR-StoSQP)を提案する。アルゴリズムは信頼領域半径を適応的に選択し、既存の直線探索StoSQP方式と比較して不確定なヘッセン行列を利用することができる。
論文参考訳（メタデータ） (2022-11-29T05:52:17Z)
Convex Optimization for Parameter Synthesis in MDPs [19.808494349302784]
確率論的モデル検査は、マルコフ決定プロセスが時間論理の仕様を満たすかどうかを証明することを目的としている。我々は、局所最適実行時ソリューションを反復的に得る2つのアプローチを開発する。数十万のパラメータを持つ衛星パラメータ合成問題に対するアプローチと,その拡張性を,広く使用されているベンチマーク上で実証する。
論文参考訳（メタデータ） (2021-06-30T21:23:56Z)
Stochastic Gradient MCMC with Multi-Armed Bandit Tuning [2.2559617939136505]
本稿では,SGMCMCハイパーパラメータを調整し,後部近似の精度を最大化するバンディットに基づく新しいアルゴリズムを提案する。シミュレーションと実データの両方で実験を行い,本手法が広範囲の応用分野に適用可能であることを確認した。
論文参考訳（メタデータ） (2021-05-27T11:00:31Z)
Adaptive Sequential SAA for Solving Two-stage Stochastic Linear Programs [1.6181085766811525]
大規模2段階線形プログラムを解くための適応的逐次SAA(sample average approximation)アルゴリズムを提案する。提案アルゴリズムは,品質の確率論的保証が与えられた解を返すために,有限時間で停止することができる。
論文参考訳（メタデータ） (2020-12-07T14:58:16Z)
Efficient semidefinite-programming-based inference for binary and multi-class MRFs [83.09715052229782]
分割関数やMAP推定をペアワイズMRFで効率的に計算する手法を提案する。一般のバイナリMRFから完全多クラス設定への半定緩和を拡張し、解法を用いて再び効率的に解けるようなコンパクトな半定緩和を開発する。
論文参考訳（メタデータ） (2020-12-04T15:36:29Z)
Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。最先端アルゴリズムの利点を論じ、解説する。
論文参考訳（メタデータ） (2020-09-28T15:22:24Z)
Planning in Markov Decision Processes with Gap-Dependent Sample Complexity [48.98199700043158]
マルコフ決定過程における計画のための新しいトラジェクトリに基づくモンテカルロ木探索アルゴリズム MDP-GapE を提案する。我々は, MDP-GapE に要求される生成モデルに対する呼び出し回数の上限を証明し, 確率の高い準最適動作を同定する。
論文参考訳（メタデータ） (2020-06-10T15:05:51Z)

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

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