Jurdzinski/Trivedi:Reachabiltiy-Time Games on Timed Automata.

Reachabiltiy-Time Games on Timed Automata.

Marcin Jurdzinski and Ashutosh Trivedi

In a reachability-time game, players Min and Max choose moves so that the time to reach a final state in a timed automaton is minimised or maximised, respectively. Asarin and Maler showed decidability of reachability-time games on strongly non-Zeno timed automata using a value iteration algorithm. This paper complements their work by providing a strategy improvement algorithm for the problem. It also generalizes their decidability result because the proposed strategy improvement algorithm solves reachability-time games on all timed automata. The exact computational complexity of solving reachability-time games is also established: the problem is EXPTIME-complete for timed automata with at least two clocks.

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