A logical description of priority separable games
摘要
A major drawback of strategic games is that the representation is not compact: an explicit representation of the payoff functions is exponential in the number of players. Separable games are succinct: payoffs are specified for pairwise interactions, and from these, payoffs are computed for strategy profiles. We consider such games, but with qualitative payoffs, and use priority orderings on players to specify the net payoff for a player from the payoffs in pairwise subgames. We show that checking existence of Nash equilibrium in priority separable games is NP-complete. We describe these equilibria in Monadic Least Fixed Point Logic (MLFP). We then extend the description to games over arbitrarily many players using second order relational variables, but restrict their use in a parameterised form giving us a model checking procedure that is also NP-complete.