Quantitative Verification in Rational Environments

We study optimal equilibrium in turn based multiplayer mean-payoff games. Nash equilibrium are a standard way to define rational behaviour of different players in multi-player games. These equilibrium treat all players equally. We study settings where a leader has additional power over the game: she has the power to assign strategies to all participating players, including herself. We argue that a leader who assign the strategies, may not want to comply with the common restrictions imposed by Nash equilibrium. This setting provides the basis for the quantitative analysis of the distributed systems, where the leader can take the role of a controller or an adversary, while the other players form a rational environment. We show that the leader always has an optimal strategy in this setting, and that no Nash equilibrium can be superior to it. Finding this equilibrium is NP-complete and, for a fixed number of players, there is a polynomial time reduction to solving two player mean-payoff games.

Authors

• Anshul Gupta
• Sven Schewe

Keywords

• Games
• Nash equilibrium
• Polynomials
• Automata
• Complexity theory
• Model checking
• Strategies In Settings
• Optimal Equilibrium
• Infinity
• Linear Programming
• Decision Problem
• Interested Parties
• Reward Function
• Evaluation Phase
• Critical Resources
• Mixed Strategy
• Stable Strategy
• Starting State
• Existence Of Equilibrium
• Outgoing Edges
• Sum Of Rewards
• Existence Of Nash Equilibrium
• Nash equilibria
• Leader equilibria
• Mean pay-off games
• Optimal strategy profiles
• Two-player mean pay-off games