Discounting in Strategy Logic

要約

戦略と時間を考慮する限り、割引はマルチエージェント システムにおいて重要な側面です。
これは、遠い将来は近い将来ほど重要ではないという直観を捉えるため、経済学において重要な側面です。
従来の検証手法では、エージェントのグループにとって勝利する戦略があるかどうかを確認できますが、より早く目標を達成することと、長時間待ってから目標を達成することは異なるという事実が考慮されていません。
この論文では、SLdisc[D] で示される一連の割引関数 D に対する将来の割引を使用して戦略ロジックを強化します。
割引関数を使用した「until」演算子を検討します。SLdisc[D] の仕様の満足値は [0, 1] の値であり、要件を満たすのに時間がかかるほど満足値は小さくなります。
ゲーム理論の古典的な例を使用してアプローチを動機付け、モデルチェック SLdisc[D] 式の複雑さを研究します。

要約(オリジナル)

Discounting is an important dimension in multi-agent systems as long as we want to reason about strategies and time. It is a key aspect in economics as it captures the intuition that the far-away future is not as important as the near future. Traditional verification techniques allow to check whether there is a winning strategy for a group of agents but they do not take into account the fact that satisfying a goal sooner is different from satisfying it after a long wait. In this paper, we augment Strategy Logic with future discounting over a set of discounted functions D, denoted SLdisc[D]. We consider ‘until’ operators with discounting functions: the satisfaction value of a specification in SLdisc[D] is a value in [0, 1], where the longer it takes to fulfill requirements, the smaller the satisfaction value is. We motivate our approach with classical examples from Game Theory and study the complexity of model-checking SLdisc[D]-formulas.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google