Sougata Bose ; Thomas A. Henzinger ; Karoliina Lehtinen ; Sven Schewe ; Patrick Totzke - History-deterministic Timed Automata

lmcs:11166 - Logical Methods in Computer Science, October 2, 2024, Volume 20, Issue 4 - https://doi.org/10.46298/lmcs-20(4:1)2024
History-deterministic Timed AutomataArticle

Authors: Sougata Bose ; Thomas A. ~Henzinger ; Karoliina Lehtinen ; Sven Schewe ; Patrick Totzke

    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.


    Volume: Volume 20, Issue 4
    Published on: October 2, 2024
    Accepted on: August 1, 2024
    Submitted on: April 7, 2023
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 601 times.
    This article's PDF has been downloaded 297 times.