Marcin Jurdzinski (University of Warwick), Time Average Games

An average time game is played on the infinite graph of configurations of a finite timed automaton. The two players, Min and Max, construct an infinite run of the automaton by taking turns to perform a timed transition. Player Min wants to minimize the average time per transition and player Max wants to maximize it. In this work optimality equations are formulated for the values of average time games and the strategy improvement algorithm for average payoff games on finite graphs is generalized to solving optimality equations for average time games. A direct consequence is an elementary proof of determinacy for average time games. This generalizes results of Asarin and Maler for optimal time reachability games and it partially solves a problem posed by Bouyer et al., to design an algorithm for solving average payoff games on priced timed automata.

(Joint work with Ashutosh Trivedi.)