On the counting of strategies

In game-theory, a classic qualitative question is to check whether a designed set of the players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be used in case of some fault. By establishing how many different strategies a game admits, one can grade its resilience. In this paper, we introduce and study Graded Strategy Logic (GSL), an extension of Strategy Logic (SL) along 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) f, one can state that at least g strategies satisfy f. Dually, via the universal construct <<x ≥ g>>φ one can enforce that there exist at least g strategies satisfying φ. Dually, via the universal construct [[x< g]]φ one can ensure that all but less than g strategies satisfy φ. As different strategies may induce the same outcome, although looking different, they need to be counted as one. While this interpretation is natural, it heavily complicates the definition and thus the reasoning about GSL. In order to accomplish this specific way of counting, we formally introduce a suitable equivalence relation over profiles based on the strategic behavior they induce. To give evidence of GSL usability, we investigate basic questions of one of its vanilla fragment, namely GSL[1G]. In particular, we report on positive results about the determinacy of games and the related model-checking problem, which we show to be PTIME-COMPLETE.