# Discounting in Strategy Logic

arXiv: https://arxiv.org/abs/2305.15256 · HTML: https://mlsanity.com/paper/2305.15256/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 94 references that are in the map.
- First posted on arXiv 24 May 2023.

## Builds on (most cited first, 9 of 9)

- [A Survey of Smart Contract Formal Specification and Verification](https://mlsanity.com/paper/2008.02712/) (2020)
- [Online Approval Committee Elections](https://mlsanity.com/paper/2202.06830/) (2022)
- [Discounting in LTL](https://mlsanity.com/paper/1406.4249/) (2014)
- [Strategy Logic with Imperfect Information](https://mlsanity.com/paper/1805.12592/) (2018)
- [Reasoning about Quality and Fuzziness of Strategic Behaviours](https://mlsanity.com/paper/1905.11537/) (2019)
- [Natural Strategic Abilities in Voting Protocols](https://mlsanity.com/paper/2007.12424/) (2020)
- [Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources](https://mlsanity.com/paper/1504.06766/) (2015)
- [Equilibria for Games with Combined Qualitative and Quantitative Objectives](https://mlsanity.com/paper/2008.05643/) (2020)
- [Budget-Constrained Coalition Strategies with Discounting](https://mlsanity.com/paper/2105.04692/) (2021)

## Abstract (arXiv)

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.