Rational verification and checking for Nash and subgame-perfect equilibria in graph games

TL;DR

This paper analyzes the computational complexity of verifying rational strategy profiles and rational responses in multiplayer graph games, focusing on Nash and subgame-perfect equilibria across various payoff functions.

Contribution

It provides complexity results for checking and rational verification problems in multiplayer graph games for key equilibrium concepts and payoff classes.

Findings

Complexity results for Nash and subgame-perfect equilibria verification.

Analysis across five major classes of payoff functions.

Decidability and complexity classifications for the problems.

Abstract

We study two natural problems about rational behaviors in multiplayer non-zero-sum sequential infinite duration games played on graphs: checking problems, that consist in deciding whether a strategy profile, defined by a Mealy machine, is rational; and rational verification, that consists in deciding whether all the rational answers to a given strategy satisfy some specification. We give the complexities of those problems for two major concepts of rationality: Nash equilibria and subgame-perfect equilibria, and for five major classes of payoff functions: parity, mean-payoff, quantitative reachability, energy, and discounted-sum.