Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria

Abstract

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 GSLT and prove that it is no harder than for SL, i.e., it is non-elementary in the quantifier rank. We show that GSLT 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.