Guest Talk: Guy Avni: Graph games in Shielding and in Bidding

Tuesday, May 28, 2019, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Guy Avni (IST Austria)

 

Abstract:

I will survey two projects that study different aspects of graph games. In the first part, I will describe the problem of synthesizing quantitative “shields”. A shield is a device that can be seen as a proxy for a “controller”: in each time point, the “plant” under control outputs its state, the controller reads it and issues an action, and the shield reads the action and can choose to alter it before assigning it to the plant, who then outputs a state, and so on. Thus, the shield acts as a monitor for the controller that is allowed to change actions. We treat the controller as a black box and in our experiments, we use a controller that was trained using machine-learning techniques. Our goal is to synthesize a shield offline with the goal of (1) interfering with the controller as little as possible, and (2) ensuring optimal plant performance. We reduce the shield-synthesis problem to the problem of solving a quantitative graph game. We experimentally show how shields are useful at overcoming limitations of machine-learning techniques.

In the second part of the talk, I will survey our work on infinite-duration “bidding” games, which combine graph games with auctions: in a bidding game, both players have budgets. In each turn, an auction is held in order to determine which player moves next. I will describe several concrete bidding mechanisms and how they affect the properties of the game. The central problem that is studied in qualitative bidding games is the existence of a necessary and sufficient initial budget to guarantee winning the game. The quantitative games we study are mean-payoff games, where the question that we study is what is the optimal payoff a player can guarantee with a given initial budget. I will describe surprising connections between bidding games and a class of stochastic games that is called “random-turn based” games in which in each turn, we toss a coin to determine which player moves.