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.

翻译：折扣是 Multi-Agent 系统中的一个重要维度，只要我们需要对策略和时间进行推理。它是经济学的核心概念，捕捉了“遥远的未来不如近期重要”这一直觉。传统验证技术允许检查一组智能体是否存在获胜策略，但未考虑“尽早满足目标”与“长期等待后满足目标”之间的区别。本文通过一组折扣函数 D 对未来折扣进行扩展，提出含折扣的策略逻辑 SLdisc[D]。我们考虑具有折扣函数的“直到”算子：SLdisc[D] 中描述的满意度值是一个 [0,1] 区间内的数值，其中满足需求所需时间越长，满意度值越小。我们通过博弈论中的经典实例阐述该方法的动机，并研究 SLdisc[D] 公式的模型检测复杂度。