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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Jurdziński, M., & Trivedi, A. (2007). Reachability-time games on timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4596 LNCS, pp. 838–849). Springer Verlag. https://doi.org/10.1007/978-3-540-73420-8_72
Mendeley helps you to discover research relevant for your work.