Colloquium Details
Stochastic Games in Synthesis and Verification.
Speaker: Krishnendu Chatterjee, University of California, Santa Cruz
Location: Warren Weaver Hall 1302
Date: March 6, 2009, 11:30 a.m.
Host: Michael Overton
Synopsis:
Dynamic games played on game graphs with winning conditions specified as automata provide the theoretical framework for the study of controller synthesis and many problems related to formal verification. Besides synthesis and verification, these games have been used in several other contexts such as checking interface compatibility, modular reasoning, checking receptiveness.
In this talk we first present different game models, that are suited to different applications, and the canonical winning conditions that can be specified as auotmata. We first consider the strictly competitive (zero-sum) game formulation that is appropriate for controller synthesis. We present a brief overview of the field, summarizing the classical results, and then present our results that significantly improve the complexity for several classes of games. We also present practical algorithms for analysis of several classes of such games.
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.
Notes:
In-person attendance only available to those with active NYU ID cards.