时间自动机上的可达时间对策
Reachability-time games on timed automata
摘要：
在可达性-时间博弈中，玩家Min和Max选择移动，使得在时间自动机中到达最终状态的时间分别最小化或最大化。Asarin和Maler使用值迭代算法证明了强非Zeno时间自动机上可达时间博弈的可判定性。本文补充他们的工作，提供了一个战略改进算法的问题。由于所提出的策略改进算法解决了所有时间自动机上的可达时间博弈，因此也推广了他们的可判定性结果。精确的计算复杂性解决可达时间游戏也建立：问题是EXPTIME完全的时间自动机至少有两个时钟。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
