Formal Methods meets Algorithmic Game Theory

The goal of this fellowship is to transfer concepts and ideas between two areas in theoretical computer science that have different takes on game theory; formal methods and algorithmic game theory (AGT, for short). The goal in formal methods is to formally reason about systems; e.g., prove formally that a system satisfies its specification or generate a correct by design system from a given specification. Game theory is popular in formal methods as it is convenient to model the interaction of a system with its environment as a two-player game that is played on a graph. The synthesis problem then reduces to finding a winning strategy for the player that models the system. AGT is a rapidly growing field that lies in the intersection between computer science and economics. Unlike the games in formal methods, which are typically zero-sum games, i.e., one player is the winner and the other player loses, the games in AGT are typically multi-valued, and the questions typically concern the stability of the game. My Ph.D. thesis studied a transfer of concepts and ideas between formal methods and network games, which constitutes a well-studied class of games in AGT. I am not aware of any other attempt to bridge between these fields though the connection is recognized as important. This fellowship broadens and deepens the connection that was previously established by studying meeting points between formal methods and auction theory, which is a core topic in AGT. An auction is the process of selling items on sale to bidders. It is a very general concept with many applications. I will build on recent results in which we studied graph games in which, rather than alternating turns, the players bid for the right to move; in each turn a bidding takes place in which the players simultaneously submit bids, the higher bidder wins, pays the other player, and decides how the game continues. The players have conflicting objectives, e.g., reaching a position in the graph. By moving, a player tries to force his objective to be met and thus win the game. The questions we studied include how much initial budget suffices for winning. Bidding for moving is an extremely general concept, which opens an exciting connection between these two fields. The main aim of this fellowship is to study it extensively. Theoretically, I will study various graph games as well as alternative bidding rules, and I will study applications of this concept that arise from viewing a bidding game as a game between processes in a concurrent system, and relating a process`s bid to quantifying the importance of being scheduled; the higher it bids the more it needs to be scheduled.

"Graph games" constitute an important class of games that is relevant for several subfields in Computer Science. The game proceeds by placing a token on one of the vertices of the graph and allowing the players to move the token to a neighboring vertex to produce an infinite path through the graph. Traditionally, the players alternate turns in moving the token. We consider "bidding games", in which both players have budgets, and in each turn, we hold an auction to determine who gets to move. The question we studied was: how do changes to the bidding mechanism influence the properties of the game? We illustrate one of our results. In the concrete bidding mechanism we used, the two players write, on a piece of paper, how much they are willing to pay to make the next move, they reveal their "bids" by simultaneously flipping their papers, and the higher bidder moves. In "Richman bidding", the higher bidder pays the lower bidder, and in "poorman bidding", the bid is paid to the "bank" and the money is lost. Even though this change in the payment scheme seems minor, it has a drastic influence on the properties of the game. We showed that in "infinite-duration" bidding games, with Richman bidding, the initial budgets do not matter and a player's utility is determined only by the graph structure. With poorman bidding, the budgets do matter: the higher the initial budget, the higher the utility a player can obtain. In addition, we studied other payment schemes as well as the following two orthogonal properties of the bidding mechanisms. First, we studied "all-pay" bidding in which both players pay their bids. Beyond the interesting theoretical properties of this mechanism, it gives rise to practical applications by thinking of the budgets as bounded resources with little or no inherent value that need to be invested dynamically in order to achieve a goal. For example, settings like political lobbying or campaigning are naturally modelled by these games. Second, motivated again by practical applications, we studied discrete bidding games, in which the budgets are given in coins, thus the minimal positive bid a player can make is one coin. The results obtained in this fellowship constitute a first significant step in the study of this model since the 90s. They demonstrate the usefulness of the combination with "formal methods" from which the concept of studying "infinite-duration" games comes. And, they leave plenty of room for a continued study of the elegant model of bidding games.