## Invited Talk

#
On optimal timed strategies

# Jean-Francois Raskin

### University Libre de Bruxelles

### Abstract

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 |