Secure Equilibria and Assume-guarantee Synthesis

Опубликовано 7 сентября 2016, 16:34

Dynamic games played on game graphs with \omega-regular winning conditions provide the theoretical framework for controller synthesis and multi-process verification. The strictly competitive (zero-sum) game formulation is appropriate for controller synthesis, but 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. In this talk 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 with \omega-regular winning conditions. We will also present how the new notion of equilibria extend the assume-guarantee style reasoning from graphs to the game theoretic framework.