論文の概要: On the Complexity of Rational Verification

• arxiv url: http://arxiv.org/abs/2207.02637v1
• Date: Wed, 6 Jul 2022 12:56:22 GMT
• ステータス: 処理完了
• システム内更新日: 2022-07-07 19:31:35.777958
• Title: On the Complexity of Rational Verification
• Title（参考訳）: 合理検証の複雑さについて
• Authors: Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge
• Abstract要約: 合理的検証とは、同時マルチエージェントシステムの時間論理特性が保持する問題を指す。 合理的な検証の複雑さは仕様によって大幅に低減できることを示す。 平均支払ユーティリティ関数によって与えられるプレイヤーの目標を考慮した場合、合理的な検証のための改善された結果を提供する。
• 参考スコア（独自算出の注目度）: 5.230352342979224
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system, under the assumption that agents in the system choose strategies that form a game-theoretic equilibrium. Rational verification can be understood as a counterpart to model checking for multiagent systems, but while classical model checking can be done in polynomial time for some temporal logic specification languages such as CTL, and polynomial space with LTL specifications, rational verification is much harder: the key decision problems for rational verification are 2EXPTIME-complete with LTL specifications, even when using explicit-state system representations. Against this background, our contributions in this paper are threefold. First, we show that the complexity of rational verification can be greatly reduced by restricting specifications to GR(1), a fragment of LTL that can represent a broad and practically useful class of response properties of reactive systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space and even in polynomial time. Second, we provide improved complexity results for rational verification when considering players' goals given by mean-payoff utility functions; arguably the most widely used approach for quantitative objectives in concurrent and multiagent systems. Finally, we consider the problem of computing outcomes that satisfy social welfare constraints. To this end, we consider both utilitarian and egalitarian social welfare and show that computing such outcomes is either PSPACE-complete or NP-complete.
• Abstract（参考訳）: 合理的検証とは、システム内のエージェントがゲーム理論平衡を形成する戦略を選択するという仮定の下で、時間論理特性が同時マルチエージェントシステムのどの部分を保持するかをチェックする問題を指す。 有理性検証はマルチエージェントシステムのモデル検査と対応するものとして理解することができるが、古典的モデル検査は、ctlのようないくつかの時相論理仕様言語やltl仕様を持つ多項式空間に対して多項式時間で行うことができるが、有理性検証は、非常に難しい: 有理性検証のための重要な決定問題は、明示的な状態のシステム表現を使用しても、2exptime-complete with ltl仕様である。 この背景に対して、本稿での私たちの貢献は3倍です。 まず, LTL の断片である GR(1) に仕様を限定することで, 合理的検証の複雑さを大幅に低減できることを示す。 特に,関連する多くの設定において,多項式空間や多項式時間においても有理的検証が可能であることを示す。 第2に、平均支払ユーティリティ関数によって与えられるプレイヤーの目標を考えると、合理的な検証のために、複雑性が向上し、並列およびマルチエージェントシステムにおいて、最も広く使われているアプローチである。 最後に,社会福祉の制約を満たす計算結果の問題を考える。 この目的のために、実用的社会福祉と平等的社会福祉の両方を検討し、計算結果がPSPACE完全かNP完全かを示す。

関連論文リスト

• Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes [5.471640959988549]
  まず、部分的に観測可能なマルコフ決定過程に対する最適制御理論を導入する。 累積報酬を最大化するポリシを合成するための構造化手法を提供する。 次に、論理的に制約されたマルチエージェント設定のための最適制御フレームワークを設計するために、このアプローチを構築します。
  論文  参考訳（メタデータ） (2023-05-24T05:15:36Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  このような問題に対する一般的なフレームワークとして,第2レベル代数モデルカウント (2AMC) を導入している。 KC(Knowledge Compilation)に基づく第1レベルのテクニックは、変数順序制約を課すことで、特定の2AMCインスタンスに適応している。 2AMC問題の論理構造を利用して、これらの制約の一部を省略し、負の効果を制限できることが示される。
  論文  参考訳（メタデータ） (2022-05-16T08:10:40Z)
• Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
  本稿では,プラットフォームに依存しない論理ゲート定義の必要性から,普遍的なフォールトトレラント論理の枠組みを提案する。 資源オーバーヘッドを改善するユニバーサル論理の新しいスキームについて検討する。 境界のない計算に好適な論理誤差率を動機として,新しい計算手法を提案する。
  論文  参考訳（メタデータ） (2021-12-22T19:00:03Z)
• Rational Verification for Probabilistic Systems [2.4254101826561847]
  我々は確率的システムにおける合理的な検証の理論とアルゴリズムを開発する。 複雑なマルチエージェント環境における不確実性とランダム性をモデル化するための並列ゲーム(CSG)に焦点を当てる。
  論文  参考訳（メタデータ） (2021-07-19T19:24:16Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。 我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。 主アルゴリズムの正確性と収束性を保証する。
  論文  参考訳（メタデータ） (2021-02-01T01:13:03Z)
• Joint Contrastive Learning with Infinite Possibilities [114.45811348666898]
  本稿では,新しい確率論的モデリングによるコントラスト学習における最近の発展の有用性について考察する。 コントラスト学習(Joint Contrastive Learning, JCL)という,コントラスト学習の特定の形態を導出する。
  論文  参考訳（メタデータ） (2020-09-30T16:24:21Z)
• Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games [5.230352342979224]
  マルチエージェントシステムにおいて、合理的な検証問題は、システム内でどの時相論理特性が保持されるかをチェックすることである。 パリティゲームの集合の解に有理検証問題を還元する手法を提案する。
  論文  参考訳（メタデータ） (2020-08-13T01:43:31Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
  論文  参考訳（メタデータ） (2020-06-05T10:56:52Z)
• On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach [3.9461038686072847]
  計算木論理(CTL)における忘れ書きに基づくアプローチを導入する。 本研究では, 与えられたモデルの下で, 与えられたシグネチャ上で, 最強必要条件 (SNC) と最弱十分条件 (WSC) を計算できることを示す。 また, その理論的性質について考察し, 忘れることの概念が, 知識を忘れることの本質的な仮定を満足させることを示す。
  論文  参考訳（メタデータ） (2020-03-13T21:51:59Z)
• Public Bayesian Persuasion: Being Almost Optimal and Almost Persuasive [57.47546090379434]
  i) 任意の状態空間, (ii) 任意の行動空間, (iii) 任意の送信者のユーティリティ関数を用いて, 一般の状況下での公衆の説得問題を考察する。 任意の公的な説得問題に対して準多項式時間ビクテリア近似アルゴリズムを提案し、特定の設定でQPTASを出力する。
  論文  参考訳（メタデータ） (2020-02-12T18:59:18Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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