Hyper Strategy Logic

要約

戦略ロジック (SL) は、マルチエージェント システムでの戦略的推論を可能にする強力な時相ロジックです。
SL は戦略に対する明示的な (一次) 定量化をサポートし、ナッシュ均衡やドミナント戦略などの多くの重要な特性を表現するための論理フレームワークを提供します。SL では同じ戦略を複数の戦略プロファイルで使用できますが、そのような各プロファイルは評価されます。
に関して。
パスプロパティ、つまり、特定の戦略的相互作用から生じる単一のパスを考慮するプロパティ。
このペーパーでは、複数の戦略プロファイルの結果を比較できる戦略ロジックであるハイパー戦略ロジック (HyperSL) を紹介します。
ハイパープロパティ、つまり複数のパスを関連付けるプロパティ。
我々は、HyperSL が、非干渉、定量的ナッシュ均衡、最適な敵対的計画、不完全な情報の下での推論など、SL では表現できない重要な特性を捕捉できることを示します。
アルゴリズムの側面では、決定可能なモデル チェックを備えた HyperSL の表現力豊かな断片を特定し、モデル チェック アルゴリズムを提示します。
私たちはアルゴリズムのプロトタイプ実装に貢献し、実験結果を奨励することについて報告します。

要約(オリジナル)

Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) quantification over strategies and provides a logical framework to express many important properties such as Nash equilibria, dominant strategies, etc. While in SL the same strategy can be used in multiple strategy profiles, each such profile is evaluated w.r.t. a path-property, i.e., a property that considers the single path resulting from a particular strategic interaction. In this paper, we present Hyper Strategy Logic (HyperSL), a strategy logic where the outcome of multiple strategy profiles can be compared w.r.t. a hyperproperty, i.e., a property that relates multiple paths. We show that HyperSL can capture important properties that cannot be expressed in SL, including non-interference, quantitative Nash equilibria, optimal adversarial planning, and reasoning under imperfect information. On the algorithmic side, we identify an expressive fragment of HyperSL with decidable model checking and present a model-checking algorithm. We contribute a prototype implementation of our algorithm and report on encouraging experimental results.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google