Discounting in Strategy Logic

Discounting in Strategy Logic

Munyque Mittelmann, Aniello Murano, Laurent Perrussel

Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence
Main Track. Pages 225-233. https://doi.org/10.24963/ijcai.2023/26

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 SL[D]. We consider “until” operators with discounting functions: the satisfaction value of a specification in SL[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 SL[D]-formulas.
Keywords:
Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis
Knowledge Representation and Reasoning: KRR: Computational complexity of reasoning
Knowledge Representation and Reasoning: KRR: Qualitative, geometric, spatial, and temporal reasoning