Speaker: Krishnendu Chatterjee
Monday February 25, 4pm, E2 Rm 352
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. These games have been used in several
other contexts such as checking interface compatibility, modular reasoning,
checking receptiveness. The strictly competitive (zero-sum) game formulation
is appropriate for controller synthesis. In this talk we first present the
different game models that have been studied with various canonical forms of
auotmata specified objectives. We give a overview of the field, summarizing the
main results in the field and also present our contributions.
We then 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.
Krishnendu Chatterjee recently graduated from UC Berkeley, where he worked on
games and verification problems during his PhD. Following his graduation, Chatterjee
has joined UCSC as a postdoctoral researcher.