Guy Avni - Formal Methods Meets Algorithmic Game Theory

The goal in formal methods is to formally reason about systems. Game theory is an important tool in formal methods. A prominent application is synthesis, where we automatically construct a correct system from a given specification. Synthesis is reduced to solving a two-player game between a system player and an adversarial environment. Indeed, a correct system can be viewed as a strategy that guarantees that the specification is satisfied, no matter how the environment behaves. As part of the effort to develop the theoretical tools that are required to reduce synthesis to practice, there is a need to reason about richer quantitative games with richer solution concepts. Algorithmic Game Theory (AGT, for short) is a growing field in the intersection between Computer Science and Economics. The games studied in AGT are typically different from the ones studied in formal methods; e.g., while traditionally, the games in formal methods are two-player, qualitative,  zero-sum, and ongoing, the games in AGT are multi-player, quantitative, non-zero-sum, one-shot games. An exchange of ideas and concepts between AGT and formal methods is a promising approach to cope with challenges in both fields. 

 The talk surveys games on the boarder between formal methods and AGT. It focuses on infinite-duration bidding games, which are two-player infinite-duration graph games (like the ones used in synthesis) in which, rather than alternating turns, an auction determines which player moves in each turn.