Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria

Strategy Logic (SL) is a well established formalism for strategic reasoning in multi-agent systems. In a nutshell, SL is built over LTL and treats strategies as first-order objects that can be associated with agents by means of a binding operator. In this work we introduce Graded Strategy Logic (Graded-SL), an extension of SL by graded quantifiers over tuples of strategy variables such as "there exist at least g different tuples (x1, ..., xn) of strategies". We study the model-checking problem of Graded-SL and prove that it is no harder than for SL, i.e., it is non-elementary in the quantifier rank. We show that Graded-SL allows one to count the number of different strategy profiles that are Nash equilibria (NE), or subgame-perfect equilibria (SPE). By analyzing the structure of the specific formulas involved, we conclude that the important problems of checking for the existence of a unique NE or SPE can both be solved in 2ExpTime, which is not harder than merely checking for the existence of such equilibria.