---
res:
bibo_abstract:
- '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 sometimes 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 winning conditions, which include the games
that arise in verification, there may be several Nash equilibria, but there is
always a unique maximal payoff profile of a secure equilibrium. We show how this
equilibrium can be computed in the case of ω-regular winning conditions, and we
characterize the memory requirements of strategies that achieve the equilibrium.@eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Krishnendu Chatterjee
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Marcin
foaf_name: Jurdziński, Marcin
foaf_surname: Jurdziński
bibo_doi: 10.1016/j.tcs.2006.07.032
bibo_issue: 1-2
bibo_volume: 365
dct_date: 2006^xs_gYear
dct_publisher: Elsevier@
dct_title: Games with secure equilibria@
...