We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed $\omega$-languages recognised by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for B\"uchi TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automata states.

翻译：我们探讨了无限时间词上的时间自动机（TA）中历史确定性的概念。历史确定性（HD）自动机是指那些能够基于已构建的运行过程在线解决非确定性的自动机。历史确定性是一个稳健的性质，它允许不同的基于博弈的刻画，并且HD规约支持无需昂贵确定化步骤的基于博弈的验证。我们证明了HD时间自动机识别的时间ω语言类严格扩展了确定性子类，并且严格包含于完全非确定性TA所识别的语言类中。对于非确定性时间自动机，已知Büchi TA的普适性已经不可判定。对于具有任意奇偶接受条件的HD时间自动机，我们证明了时间普适性、包含性以及综合问题均可判定且为EXPTIME完全。对于具有安全性或可达性接受条件的TA子类，可以在EXPTIME内判定此类自动机是否为历史确定性的。若是，则可在不引入新自动机状态的情况下有效实现其确定化。