Discounting in Strategy Logic
This work addresses the problem of reasoning about time-sensitive strategies in multi-agent systems, particularly in economics and game theory, by extending existing verification techniques to account for discounting, though it is incremental as it builds on Strategy Logic.
The paper introduces Strategy Logic with discounting (SLdisc[D]) to incorporate the importance of time in multi-agent systems, enabling the evaluation of strategies based on how quickly goals are satisfied, and analyzes the complexity of model-checking for this logic.
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.