2026-07-23T07:03:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17077 2024-03-06T10:58:41Z ddc:004 open_access

History-Deterministic Timed Automata Henzinger, Thomas A. Lehtinen, Karoliina Totzke, Patrick Timed Automata History-determinism Good-for-games fair simulation synthesis We explore the notion of history-determinism in the context of timed automata (TA). History-deterministic 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 history-deterministic specifications allow for game-based verification without an expensive determinization step. We show yet another characterisation of history-determinism in terms of fair simulation, at the general level of labelled transition systems: a system is history-deterministic precisely if and only if it fairly simulates all language smaller systems. For timed automata over infinite timed words it is known that universality is undecidable for Büchi TA. We show that for history-deterministic TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis all remain decidable and are ExpTime-complete. For the subclass of TA with safety or reachability acceptance, we show that checking whether such an automaton is history-deterministic is decidable (in ExpTime), and history-deterministic TA with safety acceptance are effectively determinizable without introducing new automata states. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas A. Henzinger and Karoliina Lehtinen and Patrick Totzke 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.14 urn:nbn:de:0030-drops-170778 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.14 eng https://creativecommons.org/licenses/by/4.0/legalcode