Reasoning about graded strategy quantifiers

In this paper we introduce and study Graded Strategy Logic (GSL), an extension of Strategy Logic (SL) with graded quantifiers. SL is a powerful formalism that allows to describe useful game concepts in multi-agent settings by explicitly quantifying over strategies treated as first-order citizens. In GSL, by means of the existential construct 《x≥g》φ one can enforce that there exist at least g strategies x satisfying φ. Dually, via the universal construct 〚x<g〛φ one can ensure that all but less than g strategies x satisfy φ. Strategies in GSL are counted semantically. This means that strategies inducing the same outcome, even though looking different, are counted as one. While this interpretation is natural, it requires a suitable machinery to allow for such a counting, as we do. Precisely, we introduce a non-trivial equivalence relation over strategy profiles based on the strategic behavior they induce. To give an evidence of GSL usability, we investigate some basic questions about the Vanilla GSL[1G] fragment, that is the vanilla restriction of the well-studied One-Goal Strategy Logic fragment of SL augmented with graded strategy quantifiers. We show that the model-checking problem for this logic is PTIME-COMPLETE. We also report on some positive results about the determinacy.