Reachability-Time Games on Timed Automata

d Abstract) Marcin Jurdzi´nski and Ashutosh Trivedi Department of Computer Science, University of Warwick, UK 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.

• Type: Conference
• Year: 2007
• Where: ICALP
• Authors: Marcin Jurdzinski, Ashutosh Trivedi
• Keywords: ICALP 2007, Non-Zeno Timed Automata, Reachability-time Games, Strategy Improvement Algorithm, Theoretical Computer Science