article published yes Sougata Bose author Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Karoliina Lehtinen author Sven Schewe author Patrick Totzke author ToHe department Vigilant Algorithmic Monitoring of Software project 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 ω -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. https://research-explorer.ista.ac.at/download/18530/18532/2024_LMCS_Bose.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ EPI Sciences2024 eng 1860-5974 2304.03183 00133246690000210.46298/lmcs-20(4:1)2024 2041-28 https://research-explorer.ista.ac.at/record/12508 S. Bose, T. A. Henzinger, K. Lehtinen, S. Schewe, and P. Totzke, “History-deterministic timed automata,” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4. EPI Sciences, pp. 1–28, 2024. S. Bose, T.A. Henzinger, K. Lehtinen, S. Schewe, P. Totzke, Logical Methods in Computer Science 20 (2024) 1–28. Bose, S., Henzinger, T. A., Lehtinen, K., Schewe, S., &#38; Totzke, P. (2024). History-deterministic timed automata. <i>Logical Methods in Computer Science</i>. EPI Sciences. <a href="https://doi.org/10.46298/lmcs-20(4:1)2024">https://doi.org/10.46298/lmcs-20(4:1)2024</a> Bose, Sougata, et al. “History-Deterministic Timed Automata.” <i>Logical Methods in Computer Science</i>, vol. 20, no. 4, EPI Sciences, 2024, pp. 1–28, doi:<a href="https://doi.org/10.46298/lmcs-20(4:1)2024">10.46298/lmcs-20(4:1)2024</a>. Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. 2024. History-deterministic timed automata. Logical Methods in Computer Science. 20(4), 1–28. Bose, Sougata, Thomas A Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. “History-Deterministic Timed Automata.” <i>Logical Methods in Computer Science</i>. EPI Sciences, 2024. <a href="https://doi.org/10.46298/lmcs-20(4:1)2024">https://doi.org/10.46298/lmcs-20(4:1)2024</a>. Bose S, Henzinger TA, Lehtinen K, Schewe S, Totzke P. History-deterministic timed automata. <i>Logical Methods in Computer Science</i>. 2024;20(4):1-28. doi:<a href="https://doi.org/10.46298/lmcs-20(4:1)2024">10.46298/lmcs-20(4:1)2024</a> 185302024-11-10T23:02:01Z2026-07-07T13:37:45Z