Optimal Strategies in Priced Timed Game Automata

Franck Cassez
CNRS, Nantes
Friday, 28 May, 2004 (All day)

Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove that it is decidable whether there is an optimal strategy in which case an optimal strategy can be computed. Our results extend previous decidability result which require the underlying game automata to be acyclic. Finally, our results are encoded in a first prototype in HyTech which is applied on a small case-study.