## Minimum-Time Reachability in Timed Games

*Thomas Brihaye,
Thomas A. Henzinger,
Vinayak Prabhu, and Jean-Francois Raskin*

We consider the minimum-time reachability problem in concurrent
two-player timed automaton game structures. We show how to compute
the minimum time needed by a player to reach a target location against
all possible choices of the opponent. We do not put any syntactic
restriction on the game structure, nor do we require any player to
guarantee time divergence. We only require players to use receptive
strategies which do not block time. The minimal time is computed in
part using a fixpoint expression, which we show can be evaluated on
equivalence classes of a non-trivial extension of the clock-region
equivalence relation for timed automata.

*Proceedings of the
34th International Colloquium on Automata, Languages, and Programming*
(ICALP),
Lecture Notes in Computer Science 4596,
Springer, 2007, pp. 825-837.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2007 Springer.