History-deterministic Timed Automata

TL;DR

This work introduces and analyzes history-determinism for timed automata over infinite timed words, establishing HD as a middle ground between deterministic and fully nondeterministic TA. It shows that for safety and reachability, HD TA are determinizable and that key verification tasks (including language inclusion and synthesis) become EXPTIME-decidable without full determinization, while coBüchi HD TA are not determinizable and HD parity TA are strictly less expressive than non-deterministic TA. The authors connect HD to fair simulation and timed games, deriving a game-based framework for verification and synthesis and providing a complete decision procedure for deciding history-determinism in the safety/reachability setting. They also provide a spectrum of expressivity results and plausible directions for extending HD concepts to Büchi and concurrent timed games, highlighting practical implications for scalable timed-system verification.

Abstract

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.

Figures (5)

• Figure 1: A history-deterministic timed reachability automaton where a resolver must distinguish between valuations where $x>y$ (go to $q_3$) and those where $x\le y$ (go to $q_2$).
• Figure 2: A history-deterministic timed co-Büchi automaton for $L$. The state $q'$ has priority $0$, i.e. is accepting, while the state $q$ has priority $1$.
• Figure 3: Blocks $b_{i,1}$, $b_{i,2}$, and $b_{i,3}$ within a unit time interval are displayed in blue, red and green respectively. Each block $b_{i,j}$ has equally spaced out events $f_{i,j,0}\ldots f_{i,j,r}$ where $r$ is at most the number of regions.
• Figure 4: A history-deterministic timed co-Büchi automaton for $L\cup Z$ (the double edges are rejecting, all other accepting).
• Figure 5: A non-deterministic timed reachability automaton for $L'$.

Theorems & Definitions (45)

• Proposition 2.1
• proof : Proof sketch
• Definition 3.1: History-determinism
• Definition 3.2: Letter game
• Proposition 3.3
• Theorem 3.4
• proof : Proof (\ref{['triangle-hd']})$\implies$(\ref{['triangle-sim']})
• Definition 4.1: Run-trees
• proof
• Lemma 4.2