Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Stochastic Games in Synthesis and Verification
Krishnendu Chatterjee
Univeristy of California at Berkeley
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 24 February 2009
16:00
60 Minutes
E1 4
019
Saarbrücken
Abstract
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 automata. 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.
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 automata. 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.
Contact
Claudia Richter
688
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Carina Schmitt, 02/26/2009 17:40
Claudia Richter, 02/20/2009 13:01 -- Created document.
Claudia Richter, 02/20/2009 13:01 -- Created document.