On Alternating-time Temporal Logic, Hyperproperties, and Strategy Sharing

要約

交互時間時相論理 (ATL$^*$) は、マルチエージェント システムに関する形式的推論のための十分に確立されたフレームワークです。
ただし、ATL$^*$ はエージェントの戦略的能力について推論することができますが (たとえば、ある連合 $A$ は最終的に目標を達成できることを保証できます)、複数の戦略的相互作用を比較したり、複数のエージェントに目標に従うように要求したりすることはできません。
同じ戦略。
たとえば、連合 $A$ が他の連合 $A’$ よりも早く (またはより頻繁に) 目標を達成できるとは言えません。
この論文では、ATL$^*$ の拡張である HyperATLS$^*_S$ を提案します。これにより、(1) 複数の戦略的相互作用の結果を比較できます。
ハイパープロパティ、つまり複数のパスを同時に参照するプロパティ、および (2) 一部のエージェントが同じ戦略を共有することを強制します。
HyperATL$^*_S$ は、既存のロジックでは届かなかった重要な AI 関連のプロパティをキャプチャする豊富な仕様言語であることを示します。
同時ゲーム構造上での HyperATL$^*_S$ のモデル チェックが決定可能であることを証明します。
私たちは、HyMASMC と呼ばれるツールにモデル チェック アルゴリズムを実装し、さまざまなベンチマークで評価します。

要約(オリジナル)

Alternating-time temporal logic (ATL$^*$) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL$^*$ can reason about the strategic ability of agents (e.g., some coalition $A$ can ensure that a goal is reached eventually), we cannot compare multiple strategic interactions, nor can we require multiple agents to follow the same strategy. For example, we cannot state that coalition $A$ can reach a goal sooner (or more often) than some other coalition $A’$. In this paper, we propose HyperATLS$^*_S$, an extension of ATL$^*$ in which we can (1) compare the outcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., a property that refers to multiple paths at the same time, and (2) enforce that some agents share the same strategy. We show that HyperATL$^*_S$ is a rich specification language that captures important AI-related properties that were out of reach of existing logics. We prove that model checking of HyperATL$^*_S$ on concurrent game structures is decidable. We implement our model-checking algorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google