|
|
Quantitative Games in Verification
Rupak Majumdar
Electrical
Engineering and Computer Sciences
University of California at Berkeley
Monday,
September 15th,
2003, 4pm - 5pm
540A/B Cory Hall (D.O.P. Center Classroom)
|
Abstract
Open systems, or
components interacting with a reactive environment, are studied
naturally as two person infinite games on transition structures with
winning conditions given by omega-regular sets on traces. While
traditionally full information games have received the most attention,
recently there has been a lot of interest in concurrent interactions in
synchronous systems. These interactions are modeled
as concurrent games on transition structures. Concurrent games have
imperfect information: at each stage, the players simultaneously and
independently choose a move, and the game moves to a new state based on
the current state and the choice of moves.
In this talk we describe algorithms and fixpoint characterizations for
solving concurrent games with omega-regular winning conditions, and
also some recent results on the existence of Nash equilibria in special
cases.
Speaker
Rupak Majumdar is a
graduate student in the
CAD Group at UC Berkeley (advisor
Tom Henzinger). His research interests are computer-aided verification
and control
of reactive, real-time, hybrid, and probabilistic systems, logic, and
automata theory. He will join UCLA as
an assistant professor starting January 2004.
|
