On the Counting of Strategies

In game theory, a classic qualitative question is to check whether a designated set of players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be possibly used in case of some fault. In this paper, we introduce 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 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.