Electronic Systems Design Seminar

 Rupak Majumdar

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)


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.


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.

©2002-2018 U.C. Regents