Secure Equilibria and Assume-guarantee Synthesis

October 30, 2006
Krishnendu Chatterjee | UC Berkeley

Dynamic games played on game graphs with ω-regular winning conditions provide the theoretical framework for controller synthesis and multi-process verification. The strictly competitive (zero-sum) game formulation is appropriate for controller synthesis, but is too strong for multi-process verification. This is because the environment for a process is typically other processes with their own specifications. On the other hand, the notion of Nash equilibria, that captures the notion of rational behavior in absence of external criteria, is too weak for multi-process verification. In this talk we will present a new notion of equilibrium, which we call secure equilibrium. We will show how the new notion of equilibrium is more appropriate for multi-process verification, discuss the existence and computation of such equilibrium for graph games with ω-regular winning conditions. We will also present how the new notion of equilibria extend the assume-guarantee style reasoning from graphs to the game theoretic framework.

Speaker Details

Krishnendu Chatterjee received the B.Tech degree in Computer Science from the Indian Institute of Technology at Kharagpur in 2001. He joined UC Berkeley in 2002 and received MS from UC Berkeley in 2004. He is currently working as a PhD student under the guidance of Prof. Thomas A. Henzinger and is expected to graduate in May 2007. His research interests include verification and control of reactive systems, probabilistic model checking, game theoretic problems in verification, logic and automata theory and stochastic game theory. He received the President’s Gold Medal from IIT, Kharagpur.