Rational verification in Iterated Electric Boolean Games

Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational elimination and rational construction of Nash equilibria by a supervising authority are PSPACE-complete problems.

• Publication year

  2016

• Venue

  SR

• Publication date

  2016-04-13

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.4204/EPTCS.218.4arXiv 1604.03773
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• MCMAS: an open-source model checker for the verification of multi-agent systems

  2017cited by this paper
• MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives

  2015cited by this paper
• Electric Boolean Games: Redistribution Schemes for Resource-Bounded Agents

  2015influential reference
• Non-Zero Sum Games for Reactive Synthesis

  2015cited by this paper
• Repairing Multi-Player Games

  2015cited by this paper
• Iterated Boolean games

  2013cited by this paper
• Multiplayer Cost Games with Simple Nash Equilibria

  2012cited by this paper
• Strategy synthesis for multi-dimensional quantitative objectives

  2012cited by this paper
• Energy parity games☆

  2010cited by this paper
• Argumentation and CP-Boolean Games

  2010cited by this paper
• Compact preference representation and Boolean games

  2009cited by this paper
• MCMAS: A Model Checker for the Verification of Multi-Agent Systems

  2009cited by this paper
• Principles of model checking

  2008cited by this paper
• Cooperative Boolean games

  2008cited by this paper
• Dependencies between players in Boolean games

  2007cited by this paper
• Boolean Games Revisited

  2006cited by this paper
• Mean-payoff parity games

  2005cited by this paper
• On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems

  1999cited by this paper
• MOCHA: Modularity in Model Checking

  1998cited by this paper
• An Automata-Theoretic Approach to Linear Temporal Logic

  1996cited by this paper
• Symbolic Controller Synthesis for Discrete and Timed Systems

  1994cited by this paper
• Detecting cycles in dynamic graphs in polynomial time

  1988cited by this paper
• Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence Incentive Engineering for Boolean Games ∗

  year unknowncited by this paper
• Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence Manipulating Boolean Games Through Communication

  year unknowncited by this paper

• Endogenous Energy Reactive Modules Games: Modelling Side Payments among Resource-Bounded Agents

  2024cites this paper