Discounting in Strategy Logic

In recent years, there has been growing interest in formal strategic reasoning about multi-agent systems. Traditional verification techniques allow one to check whether there is a winning strategy for a group of agents (and possibly synthesize it) but they do not take into account the fact that satisfying a goal sooner is different from satisfying it after a long wait. Discounting is a key paradigm in economics that captures the intuition that the far-away future is not as important as the near future. In this paper, we augment Strategy Logic with future discounting, 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 eventuality requirements, the smaller the satisfaction value is. We motivate our approach with examples from Game Theory and study the complexity of model-checking SL[D]-formulas.