Learning Deterministic Multi-Clock Timed Automata

TL;DR

This work addresses the challenge of actively learning deterministic timed automata with multiple clocks by reducing the timed-language learning problem to a reset-clocked language learning problem. It introduces a Myhill–Nerode–style equivalence on reset-clocked words and builds two Angluin-style learning algorithms: one with a powerful teacher that can reveal clock-reset information, and a normal-teacher version that guesses resets. A timed observation table over region words drives hypothesis construction, with a partition function translating table data into a DTA (CTA) model. The authors prove termination and correctness for both settings and show exponential complexity in the number of clocks due to reset guessing. Experiments reveal that the method can yield compact multi-clock DTAs, often significantly smaller than existing approaches, albeit with exponential-scaling behavior in practice.

Abstract

We present an algorithm for active learning of deterministic timed automata with multiple clocks. The algorithm is within the querying framework of Angluin's $L^*$ algorithm and follows the idea proposed in existing work on the active learning of deterministic one-clock timed automata. We introduce an equivalence relation over the reset-clocked language of a timed automaton and then transform the learning problem into learning the corresponding reset-clocked language of the target automaton. Since a reset-clocked language includes the clock reset information which is not observable, we first present the approach of learning from a powerful teacher who can provide reset information by answering reset information queries from the learner. Then we extend the algorithm in a normal teacher situation in which the learner can only ask standard membership query and equivalence query while the learner guesses the reset information. We prove that the learning algorithm terminates and returns a correct deterministic timed automaton. Due to the need of guessing whether the clocks reset at the transitions, the algorithm is of exponential complexity in the size of the target automaton.

Figures (10)

• Figure 1: A DTA $\mathcal{A}$ (left) and its corresponding CTA (right). The initial location $l_0$ is indicated by 'start’ and the accepting location $l_1$ is doubly cycled.
• Figure 2: An example of the observation table.
• Figure 3: Example of making the observation table consistent.
• Figure 4: Target DTA unbalanced:2 in waga2023active (left) and the learnt DTA by DTAL_powerful (right). The "sink" location is omitted.
• Figure 5: A copy of Fig. \ref{['fig:observationtable']} for the ease of reading.

Theorems & Definitions (26)

• definition 1: Timed automata AlurD94
• definition 2: Deterministic timed automata
• definition 3: Region equivalence AlurD94
• definition 4: Symbolic state AlurD94
• definition 5: Right congruence relation $\sim_{\mathcal{L}}$
• theorem 1: Myhill-Nerode Theorem
• definition 6: Region word
• lemma 1
• definition 7: Valid successor
• lemma 2