## Games with Secure Equilibria

*Krishnendu Chatterjee,
Thomas A. Henzinger*,
and Marcin Jurdzinski

In 2-player non-zero-sum games, Nash equilibria capture the options
for rational behavior if each player attempts to maximize her payoff.
In contrast to classical game theory, we consider lexicographic
objectives: first, each player tries to maximize her own payoff, and
then, the player tries to minimize the opponent's payoff. Such
objectives arise naturally in the verification of systems with
multiple components. There, instead of proving that each component
satisfies its specification no matter how the other components behave,
it often suffices to prove that each component satisfies its
specification provided that the other components satisfy their
specifications. We say that a Nash equilibrium is *secure* if it
is an equilibrium with respect to the lexicographic objectives of both
players. We prove that in graph games with Borel objectives, which
include the games that arise in verification, there may be several
Nash equilibria, but there is always a unique maximal payoff profile
of secure equilibria. We show how this equilibrium can be computed in
the case of omega-regular objectives, and we characterize the memory
requirements of strategies that achieve the equilibrium.

*Theoretical Computer Science* 365:67-82, 2006.
A preliminary version appeared in the
*Proceedings of the
19th Annual Symposium on Logic in Computer Science*
(LICS), IEEE Computer Society Press, 2004, pp. 160-169.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2004 IEEE,
2006 Springer.