History-deterministic timed automata Bose, Sougata Henzinger, Thomas A ; https://orcid.org/0000-0002-2985-7724 Lehtinen, Karoliina Schewe, Sven Totzke, Patrick ddc:000 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. EPI Sciences 2024 info:eu-repo/semantics/article doc-type:Article Article http://purl.org/coar/resource_type/c_2df8fbb1 https://research-explorer.ista.ac.at/record/18530 https://research-explorer.ista.ac.at/download/18530/18532 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> eng info:eu-repo/semantics/altIdentifier/doi/10.46298/lmcs-20(4:1)2024 info:eu-repo/semantics/altIdentifier/e-issn/1860-5974 info:eu-repo/semantics/altIdentifier/wos/001332466900002 info:eu-repo/semantics/altIdentifier/arxiv/2304.03183 info:eu-repo/semantics/openAccess