A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata

TL;DR

This work extends classical Myhill-Nerode theory to one-clock deterministic timed automata ($1$-DTA) by introducing a machine-independent reset function and half-integral words. It proves that $1$-DTA languages are fully determined by their half-integral word set $ ext{HI}(L)$ and the syntactic reset function $oldsymbol{R}^{L}$, enabling a canonical strict $K_L$-acceptor $ ext{A}_{(oldsymbol{R}^{L}, oughly^{L})}$. The authors establish a Myhill-Nerode style characterization and show minimality within the strict-acceptor class, then present Angluin-style $L^*$-type learning algorithms that recover the canonical acceptor using observation tables and controlled reset guessing. This yields a practical framework for learning $1$-DTA languages and highlights a principled way to compare different canonical representations arising from different resets.

Abstract

We present a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata (1-DTA). Although there is only one clock, distinct automata may reset it differently along the same word. This adds a significant challenge in the search for a canonical automaton. Our characterization is based on a new perspective of 1-DTAs in terms of "half-integral" words that they accept, along with the reset information encoded by them. We apply our results to develop L* style algorithms that learn the canonical 1-DTA.

Figures (4)

• Figure 1: Top: minimal acceptor for $L=\{(1\cdot a)(t_{1}\cdot b)(t_{2}\cdot c)\mid t_{1}\in (0,1) \text{~and~}t_{1}+t_{2}=1\}\cup\{(t_{1}\cdot d)(t_{2}\cdot c)\mid t_{1}\in (1,2) \text{~and~}t_{1}+t_{2}=2\}$. Bottom: $\mathcal{A}_{(\mathbf{R}^{L}, \approx^L)}$. This example shows that $\mathcal{A}_{(\mathbf{R}^{L}, \approx^L)}$ is not necessarily minimal among all acceptors. For readability, sink states are omitted from the figure, though they are always assumed to be present in our reasoning.
• Figure 2: Two minimal non isomorphic acceptors with different reset functions accepting the same language (sink states are omitted).
• Figure 3: Conjectures for Example \ref{['example:sm']}.
• Figure 4: Conjectures for Example \ref{['example:badbranch']}.

Theorems & Definitions (61)

• definition 1: Syntactic reset function
• theorem 1
• remark 1
• proposition 1
• theorem 2
• proof
• lemma 1
• definition 2: monotonic, $L$-preserving
• proposition 2
• proposition 3