Title: Secure Equilibria and Assume-guarantee Synthesis
Speaker: Krishnendu Chatterjee
Dynamic games played on game graphs with winning conditions specified as
automata provide the theoretical framework for the study of controller
synthesis and multi-process verification. We consider the problem of
multi-process verification and argue that the zero-sum formulation 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. 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.
We also show the relation of the new notion of equilibrium and the
assume-guarantee style reasoning for games.
This seminar is part of the CS280G seminar series.