Average-Time Games

Abstract

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.
  A solution of average-time games is presented using a reduction to
  average-price game on a finite graph.
  A direct consequence is an elementary proof of determinacy for 
  average-time games.
  This complements our results for reachability-time games and 
  partially solves a problem posed by Bouyer et al., to design an
  algorithm for solving average-price games on priced timed
  automata. 
  The paper also establishes the exact computational complexity of
  solving average-time games: the problem is EXPTIME-complete for
  timed automata with at least two clocks.