論文の概要: The Alternating-Time \mu-Calculus With Disjunctive Explicit Strategies
- arxiv url: http://arxiv.org/abs/2305.18795v1
- Date: Tue, 30 May 2023 07:16:59 GMT
- ステータス: 処理完了
- システム内更新日: 2023-05-31 17:50:43.555566
- Title: The Alternating-Time \mu-Calculus With Disjunctive Explicit Strategies
- Title（参考訳）: 断続的明示的戦略を持つ交互時間 \mu-calculus
- Authors: Merlin Humml, Lutz Schr\"oder, Dirk Pattinson
- Abstract要約: 同時ゲーム構造におけるエージェントの連立の戦略能力について検討する。
論理の重要な要素は、あるエージェントの連立が与えられた目標を強制するための共同戦略を持つことを示す経路定量化器である。
我々は, ATLES を固定点演算子と戦略解離で拡張し, 明示的な戦略で時相の $mu$-calculus に到達する。
- 参考スコア（独自算出の注目度）: 1.7725414095035827
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Alternating-time temporal logic (ATL) and its extensions, including the
alternating-time $\mu$-calculus (AMC), serve the specification of the strategic
abilities of coalitions of agents in concurrent game structures. The key
ingredient of the logic are path quantifiers specifying that some coalition of
agents has a joint strategy to enforce a given goal. This basic setup has been
extended to let some of the agents (revocably) commit to using certain named
strategies, as in ATL with explicit strategies (ATLES). In the present work, we
extend ATLES with fixpoint operators and strategy disjunction, arriving at the
alternating-time $\mu$-calculus with disjunctive explicit strategies (AMCDES),
which allows for a more flexible formulation of temporal properties (e.g.
fairness) and, through strategy disjunction, a form of controlled
nondeterminism in commitments. Our main result is an ExpTime upper bound for
satisfiability checking (which is thus ExpTime-complete). We also prove upper
bounds QP (quasipolynomial time) and NP $\cap$ coNP for model checking under
fixed interpretations of explicit strategies, and NP under open interpretation.
Our key technical tool is a treatment of the AMCDES within the generic
framework of coalgebraic logic, which in particular reduces the analysis of
most reasoning tasks to the treatment of a very simple one-step logic featuring
only propositional operators and next-step operators without nesting; we give a
new model construction principle for this one-step logic that relies on a
set-valued variant of first-order resolution.
- Abstract（参考訳）: 交互時間時間論理(英語版)(atl)とその拡張(交互時間$\mu$-calculus (amc)を含む)は、並行ゲーム構造におけるエージェントの連立の戦略的能力の仕様を提供する。
論理の鍵となる要素は、あるエージェントの連立が与えられた目標を強制するための共同戦略を持つことを示す経路量化器である。
この基本的な設定は、ATLの明示的な戦略(ATLES)のように、一部のエージェントが特定の名前の戦略を使用するように(無効に)コミットするように拡張されている。
本研究は, ATLES を固定点演算子と戦略解法で拡張し, 時間的特性(公正性など)のより柔軟な定式化と, コミットメントにおける制御された非決定論の一形態を実現するために, AMCDES (Disjunctive explicit Strategy) と交互に$\mu$-calculus に到達する。
私たちの主な成果は、満足度チェックのためのExpTimeアッパーバウンド(つまりExpTime完全)です。
また、明示的戦略の一定の解釈の下でのモデル検査における上限QP (quasipolynomial time) と NP $\cap$ coNP を、オープン解釈で NP を証明した。
提案手法は,提案演算子のみを特徴とする非常に単純な一段階論理と,ネストを伴わない次段階演算子のみを特徴とする単純な一段階論理の処理に,多くの推論タスクの分析を特に還元する,石炭代数論理の汎用的枠組みにおけるamcdesの処理である。
関連論文リスト
- Last-Iterate Global Convergence of Policy Gradients for Constrained Reinforcement Learning [62.81324245896717]
我々はC-PGと呼ばれる探索非依存のアルゴリズムを導入し、このアルゴリズムは(弱)勾配支配仮定の下でのグローバルな最終点収束を保証する。
制約付き制御問題に対して,我々のアルゴリズムを数値的に検証し,それらを最先端のベースラインと比較する。
論文 参考訳（メタデータ） (2024-07-15T14:54:57Z) - Break the Chain: Large Language Models Can be Shortcut Reasoners [18.047917626825548]
CoT(Chain-of-Thought)推論は複雑なモジュールを利用するが、高いトークン消費、適用可能性の制限、思考上の課題によって妨げられる。
本稿では、複雑な論理的および常識的推論タスクを含む算術を超えて、CoTプロンプトの批判的評価を行う。
そこで我々は,「チェーンを破る」戦略を通じて,人型やショートカットを言語モデル(LM)に統合することを提案する。
論文 参考訳（メタデータ） (2024-06-04T14:02:53Z) - Hyper Strategy Logic [4.726777092009553]
戦略論理(SL)は、マルチエージェントシステムにおける戦略的推論を可能にする強力な時間論理である。
ハイパー戦略論理(HyperSL)は、複数の戦略プロファイルの結果をハイパープロパティで比較できる戦略論理である。
本稿では,非干渉,定量的なナッシュ均衡,最適対向計画,不完全な情報に基づく推論など,SLで表現できない重要な特性をHyperSLで捉えることができることを示す。
論文 参考訳（メタデータ） (2024-03-20T16:47:53Z) - Natural Strategic Ability in Stochastic Multi-Agent Systems [6.685412769221565]
本稿では,自然戦略下での確率論的時間論理PATLとPATL*について考察する。
我々は,MASにおいて,能動連立が決定論的戦略に制限されている場合,NatPATLモデルチェックはNP完全であることを示す。
論文 参考訳（メタデータ） (2024-01-22T18:04:26Z) - Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes [5.471640959988549]
まず、部分的に観測可能なマルコフ決定過程に対する最適制御理論を導入する。
累積報酬を最大化するポリシを合成するための構造化手法を提供する。
次に、論理的に制約されたマルチエージェント設定のための最適制御フレームワークを設計するために、このアプローチを構築します。
論文 参考訳（メタデータ） (2023-05-24T05:15:36Z) - Policy Optimization with Linear Temporal Logic Constraints [37.27882290236194]
本稿では,線形時間論理制約を用いた政策最適化の問題点について考察する。
我々は,タスク満足度とコスト最適性の両方を保証するために,サンプル複雑性分析を楽しむモデルベースアプローチを開発した。
論文 参考訳（メタデータ） (2022-06-20T02:58:02Z) - Revisiting GANs by Best-Response Constraint: Perspective, Methodology,
and Application [49.66088514485446]
ベストレスポンス制約(Best-Response Constraint、BRC)は、ジェネレータのディスクリミネータへの依存性を明示的に定式化する一般的な学習フレームワークである。
モチベーションや定式化の相違があっても, フレキシブルBRC法により, 様々なGANが一様に改善できることが示される。
論文 参考訳（メタデータ） (2022-05-20T12:42:41Z) - Understanding Robust Generalization in Learning Regular Languages [85.95124524975202]
我々は、リカレントニューラルネットワークを用いて正規言語を学習する文脈における堅牢な一般化について研究する。
この問題に対処するための構成戦略を提案する。
構成戦略がエンド・ツー・エンド戦略よりもはるかに優れていることを理論的に証明する。
論文 参考訳（メタデータ） (2022-02-20T02:50:09Z) - Universal Online Convex Optimization Meets Second-order Bounds [74.0120666722487]
ユニバーサルオンライン凸最適化のための簡単な戦略を提案する。
主要なアイデアは、オリジナルのオンライン機能を処理するための専門家のセットを構築し、線形化された損失に対してメタアルゴリズムをデプロイすることである。
このようにして、私たちはブラックボックスの専門家として、既成のオンライン問題解決者をプラグインして、問題依存の後悔の限界を提供することができます。
論文 参考訳（メタデータ） (2021-05-08T11:43:49Z) - Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。
我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。
主アルゴリズムの正確性と収束性を保証する。
論文 参考訳（メタデータ） (2021-02-01T01:13:03Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。