论文标题
定时游戏和确定性的可分离性
Timed games and deterministic separability
论文作者
论文摘要
我们将Büchilandweber游戏的概括为定时设置。获胜条件是由具有Epsilon过渡的非确定性定时自动机指定的，唯一的玩家我才能过去。我们表明，对于固定数量的时钟和最大数值常数可供玩家II，是否使用这些资源有获胜的定时控制器是可以决定的。更有趣的是，我们还表明，即使没有提前指定最大数值常数，这是问题仍然可以决定的，这是先前有关定时游戏的文献中不存在的重要技术新颖性。当未固定播放器II的时钟数时，我们通过表现出不可证明的性能来补充这两个可决定性结果。作为定时游戏的应用，以及我们研究它们的主要动机，我们表明它们可以用来解决通过Epsilon过渡的非确定定时自动机的确定性可分离性问题。这是关于定时自动机的一个新的决策问题，以前尚未研究过。我们表明，当固定分离自动机的时钟数并且最大常数不是时，可分离性是可决定的。是否可以在不限制分离器的时钟数量的情况下可分离性仍然是一个有趣的开放问题。
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on timed games. We complement these two decidability result by showing undecidability when the number of clocks available to Player II is not fixed. As an application of timed games, and our main motivation to study them, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata with epsilon transitions. This is a novel decision problem about timed automata which has not been studied before. We show that separability is decidable when the number of clocks of the separating automaton is fixed and the maximal constant is not. The problem whether separability is decidable without bounding the number of clocks of the separator remains an interesting open problem.
