Formal Methods Meets Algorithmic Game Theory

Many problems in computer science, math, and economics can naturally be described as a game. As a result, various sub-fields in these disciplines study different types of games. The tutorial describes useful and interesting recent connections between formal methods and algorithmic game theory (AGT, for short). The goal in formal methods is to formally reason about systems. The traditional games that are studied in formal methods are called graph games and they model the interaction between a reactive system and its hostile environment. These are typically ongoing two-player zero-sum games of infinite duration. On the other hand, AGT lies in the intersection between computer science and economics. The games studied in AGT are typically multi-player, non-zero-sum, and one-shot games. We will focus on two meeting points between the two fields. The first is “bidding games”, which are graph games in which in each turn, an auction is held in order to determine which player moves next. We study the effect of using different bidding mechanisms on the properties of the game, and reveal an intriguing connection between bidding games and a fragment of stochastic games called “random-turn games”. In the the second meeting point, we will focus on “network games” (sometimes called “congestion games”), and describe various ways of enriching studies of network games in the AGT community by practical considerations that are well-studied in the formal-method community. This includes, for example, network games with rich specifications, ones with real-time and ongoing behaviors, as well as algorithms for handling network games with huge state spaces.

Authors

• Guy Avni University of Haifa

Keywords

No keywords are indexed for this paper.