Extended Graded Modalities in Strategy Logic

TL;DR

This paper introduces Graded Strategy Logic (GradedSL), an extension of Strategy Logic with graded quantifiers, proving its model-checking decidability and analyzing the complexity of its fragments, with applications to counting Nash and subgame-perfect equilibria.

Contribution

It presents GradedSL, extending Strategy Logic with graded quantifiers, and establishes decidability and complexity results for model-checking, including applications to equilibrium counting.

Findings

Model-checking of GradedSL is decidable.

Complexity of finite-graded fragments is non-elementary.

Counting Nash and subgame-perfect equilibria can be done in 2ExpTime.

Abstract

Strategy Logic (SL) is a logical formalism for strategic reasoning in multi-agent systems. Its main feature is that it has variables for strategies that are associated to specific agents with a binding operator. We introduce Graded Strategy Logic (GradedSL), an extension of SL by graded quantifiers over tuples of strategy variables, i.e., "there exist at least g different tuples (x_1,...,x_n) of strategies" where g is a cardinal from the set N union {aleph_0, aleph_1, 2^aleph_0}. We prove that the model-checking problem of GradedSL is decidable. We then turn to the complexity of fragments of GradedSL. When the g's are restricted to finite cardinals, written GradedNSL, the complexity of model-checking is no harder than for SL, i.e., it is non-elementary in the quantifier rank. We illustrate our formalism by showing how 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.