Author(s):

Chatterjee, Krishnendu; Henzinger, Thomas A; Jurdziński, Marcin

Title: 
Games with secure equilibria

Title Series: 
LNCS

Affiliation 

Abstract: 
In 2player nonzerosum 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 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 omegaregular winning conditions, and we characterize the memory requirements of strategies that achieve the equilibrium.

Conference Title:

FMCO: Formal Methods for Components and Objects

Volume: 
3657

Conference Dates:

November 2 – 5, 2004

Conference Location:

Leiden, The Netherlands

ISBN:

3540291318

Publisher:

Springer

Location:

Berlin, Heidelberg

Date Published:

20050919

Start Page: 
141

End Page:

161

Sponsor: 
This research was supported in part by the ONR grant N000140210671, the AFOSR MURI grant F496200010327, and the NSF grant CCR0225610.

DOI: 
10.1007/11561163_7

Notes: 
This is an extended version of the paper “Games with Secure Equilibria” that appeared in the proceedings of Logic in Computer Science (LICS), 2004.

Open access: 
no 