When we reason about strategic games, implicitly we need to reason about arbitrary strategy profiles and how players can improve from each profile. This structure is exponential in the number of players. Hence it is natural to look for subclasses of succinct games for which we can reason directly by interpreting formulas on the (succinct) game description rather than on the associated improvement structure. Priority separable games are one of such subclasses: payoffs are specified for pairwise interactions, and from these, (...) payoffs are computed for strategy profiles. We show that equilibria in such games can be described in Monadic Least Fixed Point Logic (MLFP). We then extend the description to games over arbitrarily many players, but using the monadic least fixed point extension of existential second order logic. (shrink)

Reasoning about equilibria in normal form games involves the study of players’ incentives to deviate unilaterally from any profile. In the case of large anonymous games, the pattern of reasoning is different. Payoffs are determined by strategy distributions rather than strategy profiles. In such a game each player would strategise based on expectations of what fraction of the population makes some choice, rather than respond to individual choices by other players. A player may not even know how many players there (...) are in the game. Logicising such strategisation involves many challenges as the set of players is potentially unbounded. This suggests a logic of quantification over player variables and modalities for player deviation, but such a logic is easily seen to be undecidable. Instead, we propose a propositional modal logic using player types as names and implicit quantification over players. With modalities for player deviation and transitive closure, the logic can be used to specify game equilibrium and interesting patterns of reasoning in large games. We show that the logic is decidable and present a complete axiomatisation of the valid formulas. (shrink)

In large anonymous games, payoffs are determined by strategy distributions rather than strategy profiles. If half the players choose a strategy a, all of them get a certain payoff, whereas if only one-third of the players choose that strategy, the players choosing may get a different payoff. Strategizing in such a game by a player involves reasoning about not who does what but what fraction of the population makes the same choice as that player.We present a simple modal logic to (...) reason about such strategization in large games. Since actual numbers are irrelevant, a player need not even know how many others are in the game, thus leading to the consideration of games with unboundedly many players. The logic we consider is the propositional modal fragment of a first order modal logic. We show that it has a bounded agent property, giving us a decision procedure for satisfiability. We also present a complete axiomatization of the valid formulas. The logic admits a natural model checking algorithm and bisimulation characterization. The logic with quantification over players is more appropriate, but is undecidable. (shrink)