Reachability-time games on timed automata
Computational Complexity
2020-01-16 v1 Data Structures and Algorithms
Computer Science and Game Theory
Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.0907.3414,
title = {Reachability-time games on timed automata},
author = {Marcin Jurdziński and Ashutosh Trivedi},
journal= {arXiv preprint arXiv:0907.3414},
year = {2020}
}