一句话：证明历史确定性时间自动机严格介于确定性与非确定性之间，并使其 universality、inclusion 与 synthesis 判定为 EXPTIME 完全。
论文将历史确定性（HD）概念推广到无限时间字上的时间自动机。HD 自动机允许在运行过程中根据已构造路径即时消解非确定性，具有稳健的博弈刻画，可避免昂贵的确定化。作者证明 HD 时间自动机识别的 timed ω-语言严格包含确定性时间自动机且严格包含于完全非确定性时间自动机。对于具有任意 parity 接受条件的 HD 时间自动机，时间 universality、inclusion 与 synthesis 仍可判定，且均为 EXPTIME-complete；对 safety/reachability 接受子类，可在 EXPTIME 内判定历史确定性，若成立可有效确定化且不增加状态数。
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 recognized 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 safety/reachability 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 automaton states.
@article{paperbot2721,
title = {History-deterministic Timed Automata},
author = {Sougata Bose and Thomas A. Henzinger and Karoliina Lehtinen and Sven Schewe and Patrick Totzke},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:1)2024}
}