|
Electronic
Systems Design Seminar
|
|
Quantitative Games in Verification
|
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.