Reachability-time games on timed automata

TL;DR

This paper introduces a strategy improvement algorithm for reachability-time games on timed automata, generalizing previous results and establishing EXPTIME-completeness for automata with two or more clocks.

Contribution

It provides a new strategy improvement algorithm that solves reachability-time games on all timed automata, extending prior work and analyzing computational complexity.

Findings

Algorithm solves reachability-time games on all timed automata.

Decidability is extended beyond strongly non-Zeno automata.

Problem is EXPTIME-complete for automata with two or more clocks.

Abstract

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.