{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:24Z","timestamp":1753894404706,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We explore the notion of history-determinism in the context of timed automata\n(TA) over infinite timed words. History-deterministic (HD) automata are those\nin which nondeterminism can be resolved on the fly, based on the run\nconstructed thus far. History-determinism is a robust property that admits\ndifferent game-based characterisations, and HD specifications allow for\ngame-based verification without an expensive determinization step.\n  We show that the class of timed $\\omega$-languages recognized by HD timed\nautomata strictly extends that of deterministic ones, and is strictly included\nin those recognised by fully non-deterministic TA.\n  For non-deterministic timed automata it is known that universality is already\nundecidable for safety\/reachability TA. For history-deterministic TA with\narbitrary parity acceptance, we show that timed universality, inclusion, and\nsynthesis all remain decidable and are EXPTIME-complete.\n  For the subclass of TA with safety or reachability acceptance, one can decide\n(in EXPTIME) whether such an automaton is history-deterministic. If so, it can\neffectively determinized without introducing new automaton states.<\/jats:p>","DOI":"10.46298\/lmcs-20(4:1)2024","type":"journal-article","created":{"date-parts":[[2024,10,10]],"date-time":"2024-10-10T11:53:15Z","timestamp":1728561195000},"source":"Crossref","is-referenced-by-count":1,"title":["History-deterministic Timed Automata"],"prefix":"10.46298","volume":"Volume 20, Issue 4","author":[{"given":"Sougata","family":"Bose","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Karoliina","family":"Lehtinen","sequence":"additional","affiliation":[]},{"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Totzke","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,10,2]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/14429\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/14429\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,10]],"date-time":"2024-10-10T11:53:15Z","timestamp":1728561195000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/11166"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,2]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(4:1)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2304.03183v5","asserted-by":"subject"},{"id-type":"arxiv","id":"2304.03183v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2304.03183v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2304.03183","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2304.03183","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,10,2]]},"article-number":"11166"}}