Weighted timed game automata extend timed game automata with costs on both locations and transitions. The reachability problem for weighted timed game asks, given a set of states G and a cost K, if player 1 has a strategy to force the game into G with cost less than K no matter how player 2 behaves. Recently, this problem has been formulated and studied independently by Alur et al and by Bouyer et al. In those two works, a semi-algorithm is proposed to solve the reachability problem. This semi-algorithm is only proved to terminate under conditions concerning the non-zenoness of cost. However, it was conjectured by the authors of the second paper that termination should hold for the entire class of weighted timed game automata. In this talk, we will show that, unfortunately, this conjecture can not hold as the problem is undecidable. Our undecidability result holds for weighted timed game automata with 5 clocks. On the positive side, we will show that if we restrict the number of clocks to one, then we can prove the termination of the semi-algorithm without making the hypothesis of non-zenoness of cost.
This is a joint work with Thomas Brihaye and Veronique Bruyere.
| rupak@cs.ucla.edu | Last updated: May 23, 2005 |