# Learning Deterministic Multi-Clock Timed Automata

Yu Teng  0000-0002-9434-1695 School of Software Engineering, Tongji
UniversityShanghaiChina<EMAIL_ADDRESS>,  Miaomiao Zhang
0000-0001-9179-0893 School of Software Engineering, Tongji
UniversityShanghaiChina<EMAIL_ADDRESS>and  Jie An
0000-0001-9260-9697 National Institute of InformaticsTokyoJapan
<EMAIL_ADDRESS>
(2024)

###### 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 clocks 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.

automata learning, active learning, deterministic multi-clock timed automata,
timed language, reset-clocked language

††journalyear: 2024††copyright: acmlicensed††conference: 27th ACM
International Conference on Hybrid Systems: Computation and Control; May
14–16, 2024; Hong Kong, Hong Kong††booktitle: 27th ACM International
Conference on Hybrid Systems: Computation and Control (HSCC ’24), May 14–16,
2024, Hong Kong, Hong Kong††doi: 10.1145/3641513.3650124††isbn:
979-8-4007-0522-9/24/05††ccs: Theory of computation Regular languages††ccs:
Computer systems organization Real-time languages††ccs: Theory of computation
Active learning

##  1\. Introduction

Automata learning (a.k.a. model learning) is a classic topic with an extensive
history, as a research intersection of formal methods (e.g. automata theory
(Hopcroft and Ullman, 1979)) and machine learning (e.g. computation learning
theory (Kearns and Vazirani, 1994)). In general, according to the choices of
the date set, it can be divided into two types. One is named _passive
learning_ , in which the learner has no control of the available data set. In
(Gold, 1978; Angluin, 1978), Gold and Angluin prove that the passive learning
problem of finding the smallest finite-state automaton consistent with a given
set of accepted words and rejected words is NP-complete. The other is named
_active learning_ , in contract, in which a mechanism is designed for the
learner to select the data set. In (Angluin, 1987), Angluin proposes the
famous $L^{*}$ algorithm and proves that the complexity of the learning
problem is polynomial under the active learning mechanism such that the
learner is allowed to ask membership queries and equivalence queries for a
teacher. In a membership query, the learner can ask whether a given word
belongs to the target regular language. In an equivalence query, the learner
provides a hypothesis automaton and asks whether it recognizes the target
regular language. The learning process will continue until returning the exact
model. Following Angulin’s approach, many efficient algorithms and tools have
been proposed for active learning of different kinds of automata. It has found
a wide range of applications in model checking (Peled et al., 2002; Leucker,
2006; Fiterau-Brostean et al., 2016), compositional verification (Alur et al.,
2005), legacy code analysis (Schuts et al., 2016), etc. We refer to the
surveys (Steffen et al., 2011; Vaandrager, 2017) for a comprehensive
introduction.

In recent decades, timed systems have received extensive attention. As we
know, timing constraints play a key role in the correctness and safety of
timed systems. Since finite-state automata are unable to describe the timing
behaviors, this yields a fundamental difference and makes learning formal
models of timed systems a challenging yet interesting problem.

In general, for timed systems, automata learning requires learning a timed
model from either passive observations or active tests of the system,
consisting of a collection of time-event sequences. The learned model should
describe these timing behaviors correctly. Timed automata (Alur and Dill,
1994), extending finite-state automata with clock variables, is one of the
most popular formal models of timed systems. However, there are several
obstacles to active learning of timed automata. Since the transitions of timed
automata contain both timing constraints that test the values of clocks and
resets that update the clocks, from the view of constructing a timed
automaton, we need to determine (i) the number of clocks, (ii) the reset
information, and (iii) the timing constraints, none of which are directly
observable from time-event sequences. The existing works consider timed
automata with different restrictions. Recently, an active learning algorithm
of deterministic timed automata is proposed in (Waga, 2023). However, the
number of locations in the learned automaton are highly increased compared to
the original automaton, thus lacking interpretations. More introduction can be
found in Section 7.

In this paper, following the idea in (An et al., 2020) on active learning of
deterministic one-clock timed automata, we extend the active learning method
for deterministic timed automata (DTA) with multi-clocks under continuous-time
semantics. Suppose that the number of clocks in the target DTA $\mathcal{A}$
is known before learning, i.e. we know that $\mathcal{A}$ has $m$ clocks, our
learning method can terminate and return an exact DTA $\mathcal{H}$ equipped
with $m$ clocks, i.e. the recognized timed languages of $\mathcal{A}$ and
$\mathcal{H}$ are equivalent.

The basic idea of our learning method is as follows. We define the reset-
clocked languages of timed automata and present an equivalence relation on the
reset-clocked languages. Based on the equivalence relation, we show that given
a DTA, its reset-clocked language has a finite number of equivalent classes.
Then, we prove that timed languages for two DTAs are equivalent if the reset-
clocked languages are equivalent, which reduces the problem of learning the
timed language of a DTA to that of learning a corresponding reset-clocked
language.

Since a reset-clocked language includes the reset information which is not
observable, we first consider a simple situation such that the learner learns
from a _powerful teacher_ who can answer three kinds of queries. In addition
to answering membership queries and equivalence queries, the powerful teacher
can provide the reset information on the transitions of target DTA by
answering _reset information queries_. By defining the reset information
query, we formalize the “powerful” teacher situation considered in (An et al.,
2020). Following $L^{*}$ framework, we design the timed observation table to
collect all membership queries and provide corresponding table operations.
Compared to (An et al., 2020), we need to consider the clock regions due to
the multiple clocks instead of clock valuations of a single clock. Moreover,
we record the reset information of every clock in the table. When transforming
an observation table into a hypothesis DTA, a two-step construction is
proposed. We first transform the table into a DFA and then we present a
partition function for recovering the timing constraints of each clock on each
transition from a list of clock valuations, and thus get a DTA as the
hypothesis in the following equivalence query.

After presenting learning DTA from a powerful teacher, we extend the learning
algorithm to the situation of learning from a _normal teacher_ who can only
answer membership query and equivalence query. The main difference is that the
learner now needs to guess the reset information instead of making reset
information queries. By guessing the reset information in the observation
table, every resulted possible table instance can be handled by the method in
the powerful teacher situation. However, due to these guesses, the number of
table instances is increased exponentially.

For both algorithms, we prove the termination and the correctness
respectively. Moreover, we give the complexity analysis in the numbers of
queries the learner needs to make.

In summary, our main contributions are as follows.

  * •

An equivalence relation over reset-clocked languages.

  * •

Two active learning algorithms for DTA with multi-clocks. One is learning from
the powerful teacher who can answer reset information queries in addition, and
the other is learning from the normal teacher who can only answer membership
queries and equivalence queries.

  * •

A preliminary implementation of the proposed method.

#### Structure

In what follows, Section 2 recalls the background on timed automata. The
equivalence relation over reset-clocked languages is presented in Section 3.
We then present the learning algorithms in the powerful teacher situation and
in the normal teacher situation in Section 4 and Section 5, respectively.
Section 6 reports the experimental results. Finally, Section 7 briefly
summarizes the related work and Section 8 concludes the paper.

##  2\. Preliminaries

Let $\mathbb{R}_{\geq 0}$ and $\mathbb{N}$ be the set of non-negative reals
and natural numbers, respectively. $\mathbb{B}=\\{\top,\bot\\}$ represents the
Boolean set, where $\top$ is true and $\bot$ is false. Let $\Sigma$ be the
fixed alphabet.

A _timed word_ is a finite sequence
$\omega=(\sigma_{1},t_{1})(\sigma_{2},t_{2})\cdots(\sigma_{n},t_{n})$
$\in(\Sigma\times\mathbb{R}_{\geq 0})^{*}$, where $t_{i}$ represents the delay
time length before taking action $\sigma_{i}$ for all $1\leq i\leq n$. An
equivalent definition is based on timestamps, i.e.
$\omega=(\sigma_{1},\tau_{1})(\sigma_{2},\tau_{2})\cdots(\sigma_{n},\tau_{n})$
where $\tau_{k}=\sum_{i=1}^{k}{t_{i}}$ for all $1\leq k\leq n$. We also call
such timed words as _delay-timed words_ and use $\epsilon$ to denote the
special empty word. A _timed language_ $\mathcal{L}$ is a set of timed words,
i.e. $\mathcal{L}\subseteq(\Sigma\times\mathbb{R}_{\geq 0})^{*}$.

_Timed Automata_ (Alur and Dill, 1994) is a kind of finite automata equipped
with a set of real-valued clocks. Let $\mathcal{C}$ be the set of clock
variables. A _clock constraint_ $\phi$ is a conjunctive formula of atomic
constraints of the form $c\sim n$, for $c\in\mathcal{C}$ and $n\in\mathbb{N}$,
where ${\sim}\in\\{\leq,\textless,\geq,\textgreater,=\\}$. We use
$\Phi(\mathcal{C})$ to denote the set of clock constraints. A _clock
valuation_ $\nu:\mathcal{C}\rightarrow\mathbb{R}_{\geq 0}$ is a function
assigning a non-negative real value to each clock $c\in\mathcal{C}$. We write
$\nu\in\phi$ if the clock valuation $\nu$ _satisfies_ the clock constraint
$\phi$, i.e. $\phi$ evaluates to true using the values given by $\nu$. For
$d\in\mathbb{R}_{\geq 0}$, let $\nu+d$ denote the clock valuation which maps
every clock $c\in\mathcal{C}$ to the value $\nu(c)+d$, and for a set
$\mathcal{B}\subseteq\mathcal{C}$, let $[\mathcal{B}\rightarrow 0]\nu$ denote
the clock valuation which resets all clock variables in $\mathcal{B}$ to $0$
and agrees with $\nu$ for other clocks in $\mathcal{C}\backslash\mathcal{B}$.

###### Definition 2.1 (Timed automata (Alur and Dill, 1994)).

A timed automaton is a tuple $\mathcal{A}=(\Sigma,L,l_{0},F,$
$\mathcal{C},\Delta)$, where

  * •

$\Sigma$ is the alphabet;

  * •

$L$ is a finite set of locations;

  * •

$l_{0}$ is the initial location;

  * •

$F\subseteq L$ is a set of accepting locations;

  * •

$\mathcal{C}$ is the set of clocks;

  * •

$\Delta\subseteq L\times\Sigma\times\Phi(\mathcal{C})\times
2^{\mathcal{C}}\times L$ is a finite set of transitions.

A transition $\delta=(l,\sigma,\phi,\mathcal{B},l^{\prime})$ in $\Delta$
represents a jump from the source location $l$ to the target location
$l^{\prime}$ by performing an action $\sigma\in\Sigma$ if the constraint
$\phi\in\Phi(\mathcal{C})$ is satisfied by current clock valuation. The set
$\mathcal{B}\subseteq\mathcal{C}$ gives the clocks to be reset with the
transition. We call _guards_ such transition constraints.

A _state_ $s$ of $\mathcal{A}$ is a pair $(l,\nu)$, where $l\in L$ is a
location and $\nu$ is a clock valuation. A _run_ $\rho$ of $\mathcal{A}$ over
a timed word
$\omega=(\sigma_{1},t_{1})(\sigma_{2},t_{2})\cdots(\sigma_{n},t_{n})$ is a
sequence $\rho=(l_{0},\nu_{0})\xrightarrow{t_{1},\sigma_{1}}(l_{1},\nu_{1})$
$\xrightarrow{t_{2},\sigma_{2}}\cdots\xrightarrow{t_{n},\sigma_{n}}(l_{n},\nu_{n})$,
satisfying the requirements: (1) $l_{0}$ is the initial location and
$\nu_{0}(c)=0$ for each clock $c\in\mathcal{C}$; (2) for all $1\leq i\leq n$,
there is a transition $(l_{i-1},\sigma_{i},\phi_{i},\mathcal{B}_{i},l_{i})$
such that $(\nu_{i-1}+t_{i})\in\phi_{i}$ and
$\nu_{i}=[\mathcal{B}_{i}\rightarrow 0](\nu_{i-1}+t_{i})$. The run $\rho$ is
an _accepting_ run if $l_{n}\in F$. For a run $\rho$ over a timed word
$\omega$, we define the _trace_ of $\rho$ as the corresponding timed word
$\textit{trace}(\rho)=\omega=(\sigma_{1},t_{1})(\sigma_{2},t_{2})\cdots(\sigma_{n},t_{n})\in(\Sigma\times\mathbb{R}_{\geq
0})^{*}$ if $\rho\neq(l_{0},\nu_{0})$ or the empty word
$\textit{trace}(\rho)=\epsilon$ if $\rho=(l_{0},\nu_{0})$. Given a timed
automaton $\mathcal{A}$, we define its (recognized) timed language
$\mathcal{L}(\mathcal{A})=\\{\textit{trace}(\rho)\,|\,\rho\text{ is an
accepting run}$ $\text{of }\mathcal{A}\\}$. We say two timed automata
$\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ are _equivalent_ if and only if
$\mathcal{L}(\mathcal{A}_{1})=\mathcal{L}(\mathcal{A}_{2})$.

Given a timed word
$\omega=(\sigma_{1},t_{1})(\sigma_{2},t_{2})\cdots(\sigma_{n},t_{n})$ and a
timed automaton $\mathcal{A}$, if there exists a run $\rho$, then by recording
the reset information along the run, we get a _reset-delay-timed word_
corresponding to $\omega$, denoted by
$\omega_{r}=\textit{trace}_{r}(\rho)=(\sigma_{1},t_{1},\mathbf{b}_{1})(\sigma_{2},t_{2},$
$\mathbf{b}_{2})\cdots(\sigma_{n},t_{n},\mathbf{b}_{n})$, where
$\mathbf{b}_{i}\in\mathbb{B}^{|\mathcal{C}|}$ is a $|\mathcal{C}|$-tuple
recording whether the corresponding transition resets the clocks or not when
taking the timed action $(\sigma_{i},t_{i})$. We have $\mathbf{b}_{i,j}=\top$
if the $j$-th clock $c_{j}$ is in $\mathcal{B}_{i}$, otherwise
$\mathbf{b}_{i,j}=\bot$, for all $c_{j}\in\mathcal{C}$ and $1\leq
j\leq|\mathcal{C}|$. For example, if there are $4$ clocks
$c_{1},c_{2},c_{3},c_{4}$, i.e., $|\mathcal{C}|=4$, and there is a transition
$(l_{i-1},\sigma_{i},\phi_{i},\\{c_{2},c_{3}\\},l_{i})$ taking the timed
action $(\sigma_{i},t_{i})$, then we have
$\mathbf{b}_{i}=(\bot,\top,\top,\bot)$. Similarly, the _(recognized) reset-
timed language_
$\mathcal{L}_{r}(\mathcal{A})=\\{\textit{trace}_{r}(\rho)\,|\,\rho$ is an
accepting run of $\mathcal{A}\\}$.

Additionally, based on the run $\rho$, we introduce the _clocked word_
$\gamma=(\sigma_{1},\mathbf{v}_{1})$
$(\sigma_{2},\mathbf{v}_{2})\cdots(\sigma_{n},\mathbf{v}_{n})$, where
$\mathbf{v}_{i}\in\mathbb{R}_{\geq 0}^{|\mathcal{C}|}$ records the clock value
for each clock when taking action $\sigma_{i}$, i.e.
$\mathbf{v}_{i,j}=\nu_{i-1}(c_{j})+t_{i}$ for all $c_{j}\in\mathcal{C}$ and
$1\leq j\leq|\mathcal{C}|$. After recording the reset information along the
run $\rho$, we get the _reset-clocked word_
$\gamma_{r}=(\sigma_{1},\mathbf{v}_{1},\mathbf{b}_{1})(\sigma_{2},\mathbf{v}_{2},\mathbf{b}_{2})\cdots(\sigma_{n},\mathbf{v}_{n},$
$\mathbf{b}_{n})$.

For a reset-clocked word $\gamma_{r}$, we define two functions:
$vw(\gamma_{r})$ returns the clocked word $\gamma=(\sigma_{1},\mathbf{v}_{1})$
$(\sigma_{2},\mathbf{v}_{2})\cdots(\sigma_{n},$ $\mathbf{v}_{n})$, and
$resets(\gamma_{r})=\mathbf{b}_{1},\mathbf{b}_{2},\cdots,\mathbf{b}_{n}$
extract the reset information of $\gamma_{r}$, which is a sequence from
$\mathbf{b}_{1}$ to $\mathbf{b}_{n}$.

We denote by $\preceq$ the _lexicographic order_ on the product of
$|\mathcal{C}|$ clocks. Thus, $\mathbf{v}_{1}\preceq\mathbf{v}_{2}$ means that
there exists $1\leq j\leq|\mathcal{C}|$ such that
$\mathbf{v}_{1,j}<\mathbf{v}_{2,j}$ and $\mathbf{v}_{1,i}=\mathbf{v}_{2,i}$
for all $1\leq i<j$, or specially $\mathbf{v}_{1}=\mathbf{v}_{2}$.

Given a system modelled by a timed automaton, a (delay) timed word can be
regarded as a system behavior from the view of the global clock outside of the
system. However, it is difficult to reflect the changing of the internal
logical clock variables $\mathcal{C}$ if the system is treated as a black box.
It is the main challenge for learning the transition constraints which all
correspond to the clock valuations rather than the global clock. While clocked
words contain clock valuations, they can be regarded as system behaviors from
the view of the internal logical clock variables and are more suitable for
learning transition constraints.

Moreover, if we know the reset information $\mathbf{b}_{i}$ along one run
$\rho$ over the timed word
$\omega=(\sigma_{1},t_{1})(\sigma_{2},t_{2})\cdots(\sigma_{n},t_{n})$, we can
transform $\omega$ to a clocked word
$\gamma=(\sigma_{1},\mathbf{v}_{1})(\sigma_{2},\mathbf{v}_{2})\cdots(\sigma_{n},\mathbf{v}_{n})$
by taking

(1) $\mathbf{v}_{i,j}=\begin{cases}t_{i},&\text{if}\ \ i=1\ \ \text{or}\ \
\mathbf{b}_{i-1,j}=\top\text{ for all }2\leq i\leq n;\\\
\mathbf{v}_{i-1,j}+t_{i},&\text{otherwise}.\end{cases}$

where $1\leq j\leq|\mathcal{C}|$. Here we define two functions $\Gamma_{\rho}$
and $\pi_{\rho}$ such that $\Gamma_{\rho}$ maps a (reset-)delay-timed word to
the (reset-)clocked counterpart and $\pi_{\rho}$ maps a clocked word $\gamma$
to its reset-clocked counterpart $\gamma_{r}$ according to a run $\rho$
respectively. When the run $\rho$ is determined, we omit the subscript
‘$\rho$’ and use $\Gamma$ and $\pi$ directly. Given a timed automaton
$\mathcal{A}$, the _recognized clocked language_ of $\mathcal{A}$ is given as
$\mathscr{L}(\mathcal{A})=\\{\Gamma_{\rho}(\textit{trace}(\rho))\,|\,\rho$ is
an accepting run of $\mathcal{A}\\}$ and the _recognized reset-clocked
language_ of $\mathcal{A}$ defined as
$\mathscr{L}_{r}(\mathcal{A})=\\{\Gamma_{\rho}(\textit{trace}_{r}(\rho))\,|\,\rho$
is an accepting run of $\mathcal{A}\\}$.

Given a timed automaton $\mathcal{A}$ with clocks $\mathcal{C}$, a clocked
word $\gamma\in(\Sigma\times\mathbb{R}_{\geq 0}^{|\mathcal{C}|})^{*}$ is a
_valid_ clocked word of $\mathcal{A}$ if there exists at least one run $\rho$
corresponding to $\gamma$, i.e. $\gamma=\Gamma_{\rho}(\textit{trace}(\rho))$.
Similarly, a reset-clocked word $\gamma_{r}\in(\Sigma\times\mathbb{R}_{\geq
0}^{|\mathcal{C}|}\times\mathbb{B}^{|\mathcal{C}|})^{*}$ is a _valid_ reset-
clocked word of $\mathcal{A}$ if there exists a run $\rho$ corresponding to
$\gamma_{r}$, i.e.
$\gamma_{r}=\Gamma_{\rho}(\textit{trace}_{r}(\rho))=\pi_{\rho}(\Gamma_{\rho}(\textit{trace}(\rho)))$.
Otherwise, it is _invalid_ w.r.t $\mathcal{A}$. Specially, we say a reset-
clocked word is _doomed_ if there is no timed automaton having a run
corresponding to it. That means it cannot be transformed into a timed word
according to Equation (1).

###### Definition 2.2 (Deterministic timed automata).

A timed automaton $\mathcal{A}$ is a deterministic timed automaton (DTA) if
and only if there is at most one run $\rho$ for any timed word $\omega$.

It means that, for all $l\in L$ and $\sigma\in\Sigma$, for every pair of
transitions of the form $(l,\sigma,\phi_{1},-,-)$ and
$(l,\sigma,\phi_{2},-,-)$ in $\Delta$, the clock constraints $\phi_{1}$ and
$\phi_{2}$ are mutually exclusive.

A _complete deterministic timed automaton_ (CTA) is that for any given timed
word $\omega$, there is exactly one run $\rho$. Given a DTA, it can be
transformed into a CTA accepting the same timed language in three steps: (1)
augment $L$ with a “sink” location which is not an accepting location; (2) for
every $l\in L$ and $\sigma\in\Sigma$, if there is no outgoing transition from
$l$ labelled with $\sigma$, introduce a transition resetting all clocks from
$l$ to “sink” with label $\sigma$ and guards $c\geq 0$ for each clock
$c\in\mathcal{C}$; (3) otherwise, let $\textit{Compl}_{l,\sigma}$ be the
subset of $\mathbb{R}_{\geq 0}^{|\mathcal{C}|}$ not covered by the guards of
transitions from $l$ with label $\sigma$. Write $\textit{Compl}_{l,\sigma}$ as
a union of guards $I_{1},\cdots,I_{k}$ in a minimal way, then introduce a
transition resetting all clocks from $l$ to “sink” with label $\sigma$ and
guard $I_{j}$ for each $1\leq j\leq k$. Fig. 1 depicts the transformation of
DTA $\mathcal{A}$ with $\Sigma=\\{a,b\\}$ and $\mathcal{C}=\\{c_{1},c_{2}\\}$
on the left into the CTA on the right by the above operation.

$l_{0}$start$l_{1}$$a,$$c_{1}>1\wedge c_{2}>1,$$\\{c_{2}\\}$$a,0\leq
c_{1}<3\wedge c_{2}>1,$$\\{c_{1},c_{2}\\}$$b,$$c_{1}\geq 0\wedge 0\leq
c_{2}<1,$$\\{c_{2}\\}$$l_{0}$start$l_{1}$$l_{2}$$a,$$c_{1}>1\wedge
c_{2}>1,$$\\{c_{2}\\}$$a,0\leq c_{1}<3\wedge
c_{2}>1,$$\\{c_{1},c_{2}\\}$$b,$$c_{1}\geq 0\wedge 0\leq
c_{2}<1,$$\\{c_{2}\\}$$a,c_{1}>1\wedge 0\leq c_{2}\leq
1,\\{c_{1},c_{2}\\}$$a,0\leq c_{1}\leq 1\wedge c_{2}\geq
0,\\{c_{1},c_{2}\\}$$b,c_{1}\geq 0\wedge c_{2}\geq
0,\\{c_{1},c_{2}\\}$$a,c_{1}\geq 0\wedge c_{2}\geq
0,$$\\{c_{1},c_{2}\\}$$b,c_{1}\geq 0\wedge c_{2}\geq
0,$$\\{c_{1},c_{2}\\}$$b,c_{1}\geq 0\wedge c_{2}\geq
1,\\{c_{1},c_{2}\\}$$a,c_{1}\geq 3\wedge c_{2}\geq
0,\\{c_{1},c_{2}\\}$$a,0\leq c_{1}<3\wedge c_{2}\leq 1,\\{c_{1},c_{2}\\}$

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.

Since every DTA can be transformed into a CTA, in order to present our
learning method clearly, we assume that we work with CTA in this paper.

According to the definition, a timed automaton has infinite states since the
clock values are in $\mathbb{R}_{\geq 0}$. In the theory of timed automata,
_clock region_ is an abstraction used to form a finite partition of the state
space. It will also be used in proving the termination of our learning
algorithm in this paper. Here we review the definitions of regions and
symbolic states of timed automata over regions introduced in (Alur and Dill,
1994).

###### Definition 2.3 (Region equivalence (Alur and Dill, 1994)).

Given a timed automaton $\mathcal{A}$, let $\kappa$ be a function, called a
clock ceiling, mapping each clock $c\in\mathcal{C}$ to the largest integer
appearing in the guards over $c$. For a real number $d$, let
$\textit{frac}(d)$ denote the fractional part of $d$, and $\lfloor d\rfloor$
denote its integer part. Two clock valuations $\nu$, $\nu^{\prime}$ are
region-equivalent, denoted by $\nu\sim\nu^{\prime}$, iff all the following
conditions hold:

  * •

for all $c\in\mathcal{C}$, either
$\lfloor\nu(c)\rfloor=\lfloor\nu^{\prime}(c)\rfloor$ or both
$\nu(c)\textgreater\kappa(c)$ and $\nu^{\prime}(c)\textgreater\kappa(c)$.

  * •

for all $c\in\mathcal{C}$, if $\nu(c)\leq\kappa(c)$ then
$\textit{frac}(\nu(c))=0$ iff $\textit{frac}(\nu^{\prime}(c))=0$ and

  * •

for all $c_{i},c_{j}\in\mathcal{C}$, if $\nu(c_{i})\leq\kappa(c_{i})$ and
$\nu(c_{j})\leq\kappa(c_{j})$ then
$\textit{frac}(\nu(c_{i}))\leq\textit{frac}(\nu(c_{j}))$ iff
$\textit{frac}(\nu^{\prime}(c_{i}))\leq\textit{frac}(\nu^{\prime}(c_{j}))$.

A clock region for $\mathcal{A}$ is an equivalence class induced by the
equivalence relation $\sim$. For a clock valuation $\nu$, we denote by
$\llbracket\nu\rrbracket$ the region containing it.

Given a timed automaton $\mathcal{A}$, there is only a finite number of
regions. We denote the set of regions by $\mathcal{R}$. According to the
definition of timed automata, given a transition constraint $\phi$ of
$\mathcal{A}$ if $\nu\sim\nu^{\prime}$ then $\nu\in\phi$ if and only if
$\nu^{\prime}\in\phi$. The number of clock regions $|\mathcal{R}|$ is bounded
by $|\mathcal{C}|!\cdot
2^{|\mathcal{C}|}\cdot\prod_{c\in\mathcal{C}}(2\kappa(c)+2)$ (Alur and Dill,
1994).

###### Definition 2.4 (Symbolic state (Alur and Dill, 1994)).

A symbolic state of timed automata
$\mathcal{A}=(L,l_{0},F,\mathcal{C},\Sigma,$ $\Delta)$ is a pair
$(l,\llbracket\nu\rrbracket)$, where $l\in L$ and $\llbracket\nu\rrbracket$ is
a clock region.

Therefore, the number of the symbolic states of $\mathcal{A}$ is bounded by
$|L|\cdot|\mathcal{C}|!\cdot
2^{|\mathcal{C}|}\cdot\prod_{c\in\mathcal{C}}(2\kappa(c)+2)$.

##  3\. Equivalence relation on reset-clocked words

In this section, we aim to build an equivalence relation on reset-clocked
words introduced in Section 2 and prove that it has a finite number of
equivalence classes. We first introduce the _region word_ , which is helpful
in presenting the equivalence relation.

###### Definition 3.1 (Region word).

Given a timed automaton $\mathcal{A}$, a region word $\xi$ is a finite
sequence of pairs $(\sigma,\llbracket\nu\rrbracket)$, where $\sigma\in\Sigma$
is an action of $\mathcal{A}$ and $\llbracket\nu\rrbracket$ represents a
region, i.e. $\llbracket\nu\rrbracket\in\mathcal{R}$.

For each clocked word $\gamma$ of $\mathcal{A}$, there must be a unique region
word $\xi$ corresponding to $\gamma$. We denote it by
$\xi=\llbracket\gamma\rrbracket$. For example, if
$\gamma=(a,\\{0,0\\})(a,\\{1.5,1.5\\})$, then
$\xi=\llbracket\gamma\rrbracket=(a,c_{1}=0\wedge c_{2}=0)(a,1<c_{1}<2\wedge
1<c_{2}<2\wedge c_{1}=c_{2})$.

###### Lemma 3.2.

Given a CTA $\mathcal{A}$, for all valid clocked words $\gamma$ and
$\gamma^{\prime}$ such that
$\llbracket\gamma\rrbracket=\llbracket\gamma^{\prime}\rrbracket$, they have
the same transition sequence of $\mathcal{A}$ and reach the same symbolic
state. Thus, the following two conclusions hold:

  * •

$\gamma\in\mathscr{L}(\mathcal{A})$ iff
$\gamma^{\prime}\in\mathscr{L}(\mathcal{A})$;

  * •

$resets(\gamma_{r})=resets(\gamma_{r}^{\prime})$, where $\gamma_{r}$ and
$\gamma_{r}^{\prime}$ are the reset-clocked words corresponding to $\gamma$
and $\gamma^{\prime}$, respectively.

The first conclusion shows that given a region word $\xi$, all valid clocked
words $\gamma$ with $\xi=\llbracket\gamma\rrbracket$ have the same accepting
result over $\mathcal{A}$. The second conclusion tells that such clocked words
witness the same reset information over the transitions of $\mathcal{A}$.

###### Definition 3.3 (Valid successor).

Given a CTA $\mathcal{A}$, a reset-clocked word $\gamma_{r}$ and a region word
$\xi$, we say a reset-clocked word $\gamma_{r}^{\prime}$ is a valid successor
of $\gamma_{r}$ corresponding to $\xi$ if it satisfies two conditions:

  * •

$\llbracket vw(\gamma_{r}^{\prime})\rrbracket=\xi$;

  * •

$\gamma_{r}\cdot\gamma_{r}^{\prime}$ is a valid reset-clocked word of
$\mathcal{A}$, i.e. there exists a run $\rho$ in $\mathcal{A}$ such that
$\gamma_{r}\cdot\gamma_{r}^{\prime}=\Gamma(\textit{trace}_{r}(\rho))$.

We denote the set of _valid successors_ of $\gamma_{r}$ corresponding to $\xi$
by $\textit{vs}_{\mathcal{A}}(\gamma_{r},\xi)$.

###### Example 3.4.

Consider the CTA $\mathcal{A}$ in Fig. 1. Given a valid reset-clocked word
$\gamma_{r}=(a,\\{1.1,$ $1.1\\},\\{\bot,\top\\})$ and a region word
$\xi=(b,1<c_{1}<2\wedge c_{2}=0)$,
$\gamma_{r}^{\prime}=(b,\\{1.1,0\\},\\{\bot,\top\\})$ is a valid successor of
$\gamma_{r}$ corresponding to $\xi$ since $\llbracket
vw(\gamma_{r}^{\prime})\rrbracket=\llbracket(b,\\{1.1,0\\})\rrbracket=\xi$ and
$\gamma_{r}\cdot\gamma_{r}^{\prime}$ corresponds to the run
$\rho=(l_{0},\\{0,0\\})\xrightarrow{a,1.1}(l_{1},\\{1.1,0\\})$
$\xrightarrow{b,0}(l_{1},\\{1.1,0\\})$. We denote it by
$\gamma_{r}^{\prime}\in\textit{vs}_{\mathcal{A}}(\gamma_{r},\xi)$.

###### Lemma 3.5.

Given a valid reset-clocked word $\gamma_{r}$ of a CTA $\mathcal{A}$ and a
region word $\xi$, for all
$\gamma_{r}^{\prime},\gamma_{r}^{\prime\prime}\in\textit{vs}_{\mathcal{A}}(\gamma_{r},\xi)$,
$\gamma_{r}\gamma_{r}^{\prime}$ and $\gamma_{r}\gamma_{r}^{\prime\prime}$
witness the same transition sequence of $\mathcal{A}$ and reach the same
symbolic state in the end.

###### Lemma 3.6.

Given two valid reset-clocked words $\gamma_{r1}$ and $\gamma_{r2}$ of
$\mathcal{A}$ and a region word $\xi$, if $\gamma_{r1}$ and $\gamma_{r2}$
reach the same symbolic state of $\mathcal{A}$, then for all
$\gamma_{r1}^{\prime}\in\textit{vs}_{\mathcal{A}}(\gamma_{r1},\xi)$ and
$\gamma_{r2}^{\prime}\in\textit{vs}_{\mathcal{A}}(\gamma_{r2},\xi)$, the
following two conditions hold:

  * •

$resets(\gamma_{r1}^{\prime})=resets(\gamma_{r2}^{\prime})$;

  * •

$\gamma_{r1}\gamma_{r1}^{\prime}$ and $\gamma_{r2}\gamma_{r2}^{\prime}$ reach
some same symbolic state.

Given a DTA $\mathcal{A}$, let $\Sigma$ be the finite alphabet and
$\mathcal{R}$ the finite set of regions of $\mathcal{A}$. We let
$\bm{\Sigma}=\Sigma\times\mathbb{R}_{\geq 0}^{|\mathcal{C}|}$ be the infinite
set of clocked actions, $\bm{\Sigma_{G}}=\Sigma\times\mathcal{R}$ be the
finite set of region actions, and
$\bm{\Sigma_{r}}=\Sigma\times\mathbb{R}_{\geq
0}^{|\mathcal{C}|}\times\mathbb{B}^{|\mathcal{C}|}$ be the infinite set of
reset-clocked actions. An equivalence relation over the reset-clocked language
$\mathscr{L}_{r}(\mathcal{A})$ is defined as follows.

###### Definition 3.7 (Equivalence relation).

Let $\mathscr{L}_{r}(\mathcal{A})$ be the reset-clocked language of a DTA
$\mathcal{A}$, two reset-clocked words
$\gamma_{r1},\gamma_{r2}\in\bm{\Sigma_{r}}^{*}$ are indistinguishable by
$\mathscr{L}_{r}(\mathcal{A})$, denoted by
$\gamma_{r1}\sim_{\mathscr{L}_{r}(\mathcal{A})}\gamma_{r2}$, if for all
$\gamma_{r1}^{\prime}\in\textit{vs}_{\mathcal{A}}(\gamma_{r1},\xi)$ and
$\gamma_{r2}^{\prime}\in\textit{vs}_{\mathcal{A}}(\gamma_{r2},\xi)$, the
following conditions holds for all $\xi\in\bm{\Sigma_{G}}^{*}$:

  * •

$\gamma_{r1}\gamma_{r1}^{\prime}\in\mathscr{L}_{r}(\mathcal{A})$ iff
$\gamma_{r2}\gamma_{r2}^{\prime}\in\mathscr{L}_{r}(\mathcal{A})$;

  * •

$resets(\gamma_{r1}^{\prime})=resets(\gamma_{r2}^{\prime})$.

###### Lemma 3.8.

If two valid reset-clocked words $\gamma_{r1},\gamma_{r2}$ of $\mathcal{A}$
reach the same symbolic state of $\mathcal{A}$, then
$\gamma_{r1}\sim_{\mathscr{L}_{r}(\mathcal{A})}\gamma_{r2}$.

###### Lemma 3.9.

All invalid reset-clocked words belong to the same equivalence class of
$\sim_{\mathscr{L}_{r}(\mathcal{A})}$.

###### Theorem 3.10.

Let $\mathscr{L}_{r}(\mathcal{A})$ be the reset-clocked language of a DTA
$\mathcal{A}$, and then $\sim_{\mathscr{L}_{r}(\mathcal{A})}$ has a finite
number of equivalence classes.

##  4\. Learning DTA from a powerful teacher

In this section, we present the algorithm for learning a DTA $\mathcal{A}$
from a powerful teacher. The basic idea is that we transform the learning
problem for the timed language of an underlying DTA $\mathcal{A}$ into the
learning problem for the reset-clocked language of $\mathcal{A}$. We first
introduce the basic idea and then describe the settings of the powerful
teacher. After presenting the details of the learning algorithm, we show its
correctness, termination and complexity.

###### Theorem 4.1.

Given two DTAs $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$, if
$\mathscr{L}_{r}(\mathcal{A}_{1})=\mathscr{L}_{r}(\mathcal{A}_{2})$, then
$\mathcal{L}(\mathcal{A}_{1})=\mathcal{L}(\mathcal{A}_{2})$.

According to Theorem 4.1, to construct a DTA that recognizes a target timed
language $\mathcal{L}=\mathcal{L}(\mathcal{A})$, it suffices to learn a
hypothesis DTA $\mathcal{H}$ such that
$\mathscr{L}_{r}(\mathcal{A})=\mathscr{L}_{r}(\mathcal{H})$. Instead of
checking directly if
$\mathscr{L}_{r}(\mathcal{A})=\mathscr{L}_{r}(\mathcal{H})$, the
contraposition of the theorem guarantees that we can still perform equivalence
queries over their timed languages: if
$\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{H})$, then $\mathcal{H}$
recognizes the target language already; otherwise, a counterexample making
$\mathcal{L}(\mathcal{A})\neq\mathcal{L}(\mathcal{H})$ also yields an evidence
for $\mathscr{L}_{r}(\mathcal{A})\neq\mathscr{L}_{r}(\mathcal{H})$.

There are two roles in the learning algorithm: a learner and a powerful
teacher. The teacher holds the underlying target DTA $\mathcal{A}$ and three
oracles to answer three kinds of queries: _reset information query_ ,
membership query and equivalence query from the learner. For a reset
information query, the learner asks the reset information along the run of a
valid clocked word $\gamma$. The teacher returns the reset information of the
clocks, and the learner gets a reset-clocked word. For a membership query, the
teacher receives a reset-clocked word $\gamma_{r}$ from the learner and
answers whether $\gamma_{r}\in\mathscr{L}_{r}(\mathcal{A})$. For an
equivalence query, the learner submits a hypothesis DTA $\mathcal{H}$ and the
teacher answers whether $\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{H})$.
If the answer is no, the powerful teacher returns a reset-delay-timed word
$\omega_{r}$ as a counterexample in addition. We denote the three oracles for
reset information query, membership query and equivalence query by RQ, MQ and
EQ, respectively.

Suppose that the DTA $\mathcal{A}$ is a complete DTA and the learner knows the
number of the clocks $|\mathcal{C}|$ in advance. We show more details as
follows.

###  4.1. Timed observation table, reset information query, and membership
query

Similar to the classic $L^{*}$ algorithm, we design an observation table to
collect the query results.

###### Definition 4.2 (Timed observation table for DTA).

A timed observation table for DTA is a tuple
$\mathbf{T}=(\Sigma,\bm{\Sigma_{G}},\bm{\Sigma_{r}},\bm{S},\bm{R},\bm{E},f,g)$,
where $\bm{S},\bm{R}\subset\bm{\Sigma_{r}}^{*}$ are finite sets of reset-
clocked words, named prefix set and boundary, respectively, and
$\bm{E}\subset\bm{\Sigma_{G}}^{*}$ is a finite set of region words, named
suffix set. Specifically,

  * •

$\bm{S}$ and $\bm{R}$ are disjoint, i.e.,
$\bm{S}\cup\bm{R}=\bm{S}\uplus\bm{R}$, and $\bm{S}\cup\bm{R}$ is prefix-
closed.

  * •

The empty word is, by default, both a prefix and a suffix, i.e.,
$\epsilon\in\bm{E}$ and $\epsilon\in\bm{S}$;

  * •

$f:\bm{S}\cup\bm{R}\times\bm{E}\rightarrow\\{+,-\\}$ is the classification
function such that for a reset-clocked word $\gamma_{r}\in\bm{S}\cup\bm{R}$
and a region word $e\in\bm{E}$, $f(\gamma_{r},e)=-$ if
$\textit{vs}_{\mathcal{A}}(\gamma_{r},e)=\emptyset$ or
$\mathsf{MQ}(\gamma_{r}e_{r})=-$ i.e.
$\gamma_{r}e_{r}\notin\mathscr{L}_{r}(\mathcal{A})$ where
$e_{r}\in\textit{vs}_{\mathcal{A}}(\gamma_{r},e)$, and $f(\gamma_{r},e)=+$ if
$\mathsf{MQ}(\gamma_{r}e_{r})=+$, i.e.
$\gamma_{r}e_{r}\in\mathscr{L}_{r}(\mathcal{A})$.

  * •

$g:\bm{S}\cup\bm{R}\times\bm{E}\rightarrow\\{\bot,\top\\}^{|e\in\bm{E}|\times|\mathcal{C}|}$
is a labelling function such that for a reset-clocked word
$\gamma_{r}\in\bm{S}\cup\bm{R}$ and a region word
$e\in\bm{E}\backslash\\{\epsilon\\}$, $g(\gamma_{r},e)=resets(e_{r})$ where
$e_{r}\in\textit{vs}_{\mathcal{A}}(\gamma_{r},e)$ if
$\textit{vs}_{\mathcal{A}}(\gamma_{r},e)\neq\emptyset$, otherwise
$g(\gamma_{r},e)=\\{\top\\}^{|e\in\bm{E}|\times|\mathcal{C}|}$.

Consider the classification function $f$. It records the results of the
membership queries i.e., whether $\gamma_{r}e_{r}$ is in
$\mathscr{L}_{r}(\mathcal{A})$. Depending on Lemma 3.5 and Lemma 3.8, $e_{r}$
can represent all other valid successors $e_{r}^{\prime}$ according to the
region word $e$ such that
$\gamma_{r}e_{r}\sim_{\mathscr{L}_{r}(\mathcal{A})}\gamma_{r}e_{r}^{\prime}$.
The function $g$ records the reset information in the valid successor $e_{r}$
and assigns all resets to $\top$ if there is no valid successor $e_{r}$.
However, according to Definition 3.3, the valid successor $e_{r}$ depends on a
known DTA $\mathcal{A}$. We claim that the learner can compute the valid
successors using reset information queries instead of knowing DTA
$\mathcal{A}$.

1

input : A reset-clocked word
$\gamma_{r}=(\sigma_{1},\mathbf{v}_{1},\mathbf{b}_{1})(\sigma_{2},\mathbf{v}_{2},\mathbf{b}_{2})\cdots(\sigma_{n},\mathbf{v}_{n},\mathbf{b}_{n})\in\bm{S}\cup\bm{R}$;

a region word
$e=(\sigma_{1}^{\prime},\llbracket\nu_{1}\rrbracket)(\sigma_{2}^{\prime},\llbracket\nu_{2}\rrbracket)\cdots(\sigma_{k}^{\prime},\llbracket\nu_{k}\rrbracket)\in\bm{E}$.

output : A valid successor $e_{r}\in\textit{vs}_{\mathcal{A}}(\gamma_{r},e)$.

2

3$e_{r}\leftarrow\epsilon$ ;

4 if  _$\gamma_{r}$ is doomed_ then

5 return $\bot$

6 else

7 if  _$\gamma_{r}=\epsilon$_ then

$\mathbf{v}_{n}\leftarrow 0;\mathbf{b}_{n}\leftarrow\top$ ;

// Set the initial clock valuation.

8

9 for  _$i\leftarrow 1$ to $k$_ do

10 for  _$j\leftarrow 1$ to $|\mathcal{C}|$_ do

11 if  _$\mathbf{b}_{n+i-1,j}=\top$_ then

12 $\mathbf{v}_{n+i,j}\leftarrow 0$;

13 else

14 $\mathbf{v}_{n+i,j}\leftarrow\mathbf{v}_{n+i-1,j}$;

15

16
$\textit{flag},d\leftarrow\textsf{Solve}(\llbracket\mathbf{v}_{n+i}+d\rrbracket=\llbracket\nu_{i}\rrbracket)$

17 if  _$\textit{flag}=\bot$_ then

18 return $\bot$;

19 else

20 $\mathbf{v}_{n+i}\leftarrow\mathbf{v}_{n+i}+d$;

21
$\mathbf{b}_{n+i}\leftarrow\textbf{RQ}(vw(\gamma_{r})\cdot(\sigma_{i}^{\prime},\mathbf{v}_{n+i}))$;

22 $e_{r}\leftarrow
e_{r}\cdot(\sigma_{i}^{\prime},\mathbf{v}_{n+i},\mathbf{b}_{n+i})$;

23
$\gamma_{r}\leftarrow\gamma_{r}\cdot(\sigma_{i}^{\prime},\mathbf{v}_{n+i},\mathbf{b}_{n+i})$;

24

25 return $e_{r}$;

26

Algorithm 1 FindValidSuccessor

Algorithm 1 shows the computation for a valid successor $e_{r}$. Given a
reset-clocked word $\gamma_{r}\in\bm{S}\cup\bm{R}$, we can use Equation 1 to
determine whether $\gamma_{r}$ is doomed. If it is doomed, then we stop the
computation as we know that there is no valid successor (Line 1). Otherwise,
we compute $e_{r}$ by considering the region actions in the region word
$e\in\bm{E}$ one by one. For the first region action
$(\sigma_{1}^{\prime},\llbracket\nu_{1}\rrbracket)$, depending on the last
reset information in $\gamma_{r}$, we can compute the clock values
$\mathbf{v}_{n+1}$. Then we find a delay time $d\in\mathbb{R}_{\geq 0}$ such
that $\mathbf{v}_{n+1}+d\in\llbracket\nu_{1}\rrbracket$ by the function
$Solve()$ and use $flag$ to represent whether there is such $d$ or not. If
there is no such $d$, it means that there is no clock valuation in
$\llbracket\nu_{1}\rrbracket$ that can form a valid successor. Otherwise, we
update $\mathbf{v}_{n+1}$ and get a clocked word
$(\sigma_{1}^{\prime},\mathbf{v}_{n+1})$. Then we make a reset information
query for $vw(\gamma_{r})\cdot(\sigma_{1}^{\prime},\mathbf{v}_{n+1})$ to get
the last reset information $\mathbf{b}_{n+1}$ (Line 1). After that, we update
$e_{r}$ and $\gamma_{r}$. The computation for other region actions in $e$ is
similar.

###### Example 4.3.

Fig. 2 shows an example of a timed observation table. Suppose that the CTA
$\mathcal{A}$ in Fig. 1 is the underlying target automaton. Consider
$\gamma_{r}=(a,\\{0,0\\},\\{\top,\top\\})$ and $e=(a,1<c_{1}<2\wedge
1<c_{2}<2\wedge c_{1}=c_{2})$, $n=1$ for the length of $\gamma_{r}$ and there
is only one region action in $e$. According to Algorithm 1, we get
$e_{r}=(a,\\{1.05,1.05\\},\\{\top,\top\\})\in\textit{vs}_{\mathcal{A}}(\gamma_{r},e)$.

|  $\epsilon$ |  $(a,1<c_{1}<2\wedge 1<c_{2}<2\wedge c_{1}=c_{2})$
---|---|---
$\epsilon$ |  $-$ |  $+,\bot,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})$ |  $+$ |  $-,\top,\top$
$(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{1.05,0\\},\\{\bot,\top\\})$ |  $+$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{2.05,1\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{0,0\\},\\{\top,\top\\})(a,\\{1.05,1.05\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{0,0\\},\\{\top,\top\\})(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{0,0\\},\\{\top,\top\\})(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$

Figure 2. An example of the observation table.

Similar to the $L^{*}$ algorithm, for the observation table, we also define a
function row mapping each $\gamma_{r}\in\bm{S}\cup\bm{R}$ to a vector indexed
by every $e\in\bm{E}$. Each element of the vector is defined as
$\\{f(\gamma_{r},e),g(\gamma_{r},e)\\}$. For example, in Fig. 2, consider
$\gamma_{r}=(a,\\{1.05,$ $1.05\\},\\{\bot,\top\\})$, we have
$\textit{row}(\gamma_{r})=\\{\\{+\\},\\{-,\top,\top\\}\\}$.

Before constructing a hypothesis $\mathcal{H}$ based on the timed observation
table $\mathbf{T}$, the learner has to ensure that $\mathbf{T}$ satisfies the
following conditions:

  * •

_Reduced:_
$\forall\emph{s},\emph{s}^{\prime}\in\bm{S}\colon\emph{s}\neq\emph{s}^{\prime}\text{
implies }\mathit{row}(\emph{s})\neq\mathit{row}(\emph{s}^{\prime})$;

  * •

_Closed:_ $\forall r\in\bm{R},\exists
s\in\bm{S}\colon\mathit{row}(s)=\mathit{row}(r)$;

  * •

_Consistent:_ $\forall\gamma_{r},\gamma_{r}^{\prime}\in\bm{S}\cup\bm{R}$,
$\mathit{row}(\gamma_{r})=\mathit{row}(\gamma_{r}^{\prime})$ implies that: for
all $\bm{\sigma_{r}},\bm{\sigma_{r}}^{\prime}\in\bm{\Sigma_{r}}$ such that
$\llbracket vw(\bm{\sigma_{r}})\rrbracket=\llbracket
vw(\bm{\sigma_{r}}^{\prime})\rrbracket$, if
$\gamma_{r}\bm{\sigma_{r}},\gamma_{r}^{\prime}\bm{\sigma_{r}}^{\prime}\in\bm{S}\cup\bm{R}$,
the following conditions are satisfied:

    * –

$\mathit{row}(\gamma_{r}\bm{\sigma_{r}})=\mathit{row}(\gamma_{r}^{\prime}\bm{\sigma_{r}}^{\prime})$;

    * –

$resets(\bm{\sigma_{r}})=resets(\bm{\sigma_{r}}^{\prime})$.

  * •

_Evidence-closed:_ $\forall\emph{s}\in\bm{S}$ and $\forall\emph{e}\in\bm{E}$,
if $\textit{vs}_{\mathcal{A}}(\emph{s},e)$ is not empty, there is
$e_{r}\in\textit{vs}_{\mathcal{A}}(\emph{s},e)$ such that
$\emph{s}e_{r}\in\bm{S}\cup\bm{R}$;

A timed observation table $\mathbf{T}$ is prepared if it satisfies the above
four conditions. To get the table prepared, the learner can perform the
following operations.

T1 |  $\epsilon$
---|---
$\epsilon$ |  $-$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})$ |  $+$
$(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$
$(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{1.05,0\\},\\{\bot,\top\\})$ |  $+$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{2.05,1\\},\\{\top,\top\\})$ |  $-$
$(a,\\{0,0\\},\\{\top,\top\\})(a,\\{1.05,1.05\\},\\{\top,\top\\})$ |  $-$

T2 |  $\epsilon$ |  $(a,1<c_{1}<2\wedge 1<c_{2}<2\wedge c_{1}=c_{2})$
---|---|---
$\epsilon$ |  $-$ |  $+,\bot,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})$ |  $+$ |  $-,\top,\top$
$(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(a,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{0,0\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{1.05,0\\},\\{\bot,\top\\})$ |  $+$ |  $-,\top,\top$
$(a,\\{1.05,1.05\\},\\{\bot,\top\\})(b,\\{2.05,1\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$
$(a,\\{0,0\\},\\{\top,\top\\})(a,\\{1.05,1.05\\},\\{\top,\top\\})$ |  $-$ |  $-,\top,\top$

Figure 3. Example of making the observation table consistent.

Making $\mathbf{T}$ closed. If there is $r\in\bm{R}$ such that for all
$s\in\bm{S}$, $\mathit{row}(r)\neq\mathit{row}(s)$, the learner will move $r$
from $\bm{R}$ to $\bm{S}$. Moreover, for each $\sigma\in\Sigma$, a reset-
clocked word $\pi(vw(r)\cdot\bm{\sigma})$ needs to be added to $\bm{R}$, where
$\bm{\sigma}=(\sigma,\\{0\\}^{|\mathcal{C}|})$. The mapping $\pi$ defined in
Section 2 can be implemented by a reset information query in the powerful
teacher situation.

Making $\mathbf{T}$ consistent. Considering the first case, there exist two
reset-clocked words $\gamma_{r},\gamma_{r}^{\prime}\in\bm{S}\cup\bm{R}$ at
least, for $\bm{\sigma_{r}},\bm{\sigma_{r}}^{\prime}\in\bm{\Sigma_{r}}$ such
that $\llbracket vw(\bm{\sigma_{r}})\rrbracket=\llbracket
vw(\bm{\sigma_{r}}^{\prime})\rrbracket$, both $\gamma_{r}\bm{\sigma_{r}}$ and
$\gamma_{r}^{\prime}\bm{\sigma_{r}}^{\prime}\in\bm{S}\cup\bm{R}$. However,
$\mathit{row}(\gamma_{r})=\mathit{row}(\gamma_{r}^{\prime})$ but
$\mathit{row}(\gamma_{r}\bm{\sigma_{r}})\neq\mathit{row}(\gamma_{r}^{\prime}\bm{\sigma_{r}^{\prime}})$.
In this case, there must be $\emph{e}\in\bm{E}$ such that
$f(\gamma_{r}\bm{\sigma_{r}},\emph{e})\neq
f(\gamma_{r}^{\prime}\bm{\sigma_{r}^{\prime}},\emph{e})$ or
$g(\gamma_{r}\bm{\sigma_{r}},\emph{e})\neq
g(\gamma_{r}^{\prime}\bm{\sigma_{r}^{\prime}},\emph{e})$. Thus, the learner
adds $\llbracket vw(\bm{\sigma_{r}})\rrbracket\cdot\emph{e}$ to $\bm{E}$, so
that $\gamma_{r}$ and $\gamma_{r}^{\prime}$ are separated. Consider the second
case that $resets(\bm{\sigma_{r}})\neq resets(\bm{\sigma_{r}}^{\prime})$. In
this case, $\llbracket vw(\bm{\sigma_{r}})\rrbracket$ is enough to distinguish
$\gamma_{r}$ from $\gamma_{r}^{\prime}$. So, the learner adds $\llbracket
vw(\bm{\sigma_{r}})\rrbracket$ to $\bm{E}$. After extending $\bm{E}$, the
learner fills the table by making reset information queries and membership
queries.

Making $\mathbf{T}$ evidence-closed. In this case, $\exists\emph{s}\in\bm{S}$
and $\exists\emph{e}\in\bm{E}$, $\textit{vs}_{\mathcal{A}}(\emph{s},e)$ is not
empty, and there is no $e_{r}\in\textit{vs}_{\mathcal{A}}(\emph{s},e)$ such
that $\emph{s}e_{r}\in\bm{S}\cup\bm{R}$. The learner finds
$e_{r}\in\textit{vs}_{\mathcal{A}}(\emph{s},e)$ and then adds all prefixes of
$\emph{s}e_{r}$ to $\bm{R}$, except for those already in $\bm{S}\cup\bm{R}$.
Similarly, the learner needs to fill the table.

The condition that an observation table is reduced is inherently preserved by
the aforementioned operations, together with the counterexample processing
described later in Section 4.3. Furthermore, a table may need several rounds
of these operations before being prepared since certain conditions may be
violated by different interleaved operations.

###### Example 4.4.

Fig. 3 shows a process for making the table consistent. Assuming that the CTA
in Fig. 1 recognizes the target timed language and an observation table T1 is
generated in the learning process. We show the inconsistency of T1 as follows.
Let $\gamma_{r}=\epsilon$ and
$\gamma_{r}^{\prime}=(a,\\{0,0\\},\\{\top,\top\\})$, we have
$\mathit{row}(\gamma_{r})=\mathit{row}(\gamma_{r}^{\prime})$. Choose
$\bm{\sigma_{r}}=(a,\\{1.05,$ $1.05\\},\\{\bot,\top\\})$ and
$\bm{\sigma_{r}}^{\prime}=(a,\\{1.05,$ $1.05\\},\\{\top,\top\\})$ such that
$\llbracket vw(\bm{\sigma_{r}})\rrbracket=\llbracket
vw(\bm{\sigma_{r}}^{\prime})\rrbracket$. We have
$\gamma_{r}\bm{\sigma_{r}}=(a,\\{1.05,1.05\\},\\{\bot,\top\\})$ and
$\gamma_{r}^{\prime}\bm{\sigma_{r}}^{\prime}=(a,\\{0,0\\},\\{\top,\top\\})$
$(a,\\{1.05,1.05\\},\\{\top,\top\\})$ in $\bm{S}\cup\bm{R}$. However, we find
$\mathit{row}(\gamma_{r}\bm{\sigma_{r}})\neq\mathit{row}(\gamma_{r}^{\prime}\bm{\sigma_{r}}^{\prime})$
and $resets(\bm{\sigma_{r}})\neq resets(\bm{\sigma_{r}}^{\prime})$. Thus, T1
violates the two conditions of consistency. In order to make the table
consistent, we add $\llbracket(a,\\{1.05,1.05\\})\rrbracket\cdot\epsilon$,
which equals $(a,1\textless c_{1}\textless 2\wedge 1<c_{2}<2\wedge
c_{1}=c_{2})$, to $\bm{E}$ to distinguish $\epsilon$ and
$(a,\\{0,0\\},\\{\top,\top\\})$, and then fill the table and get T2.

###  4.2. Hypothesis construction

When the observation table $\mathbf{T}$ is prepared, a hypothesis
$\mathcal{H}$ can be constructed based on $\mathbf{T}$ in two steps: 1. Build
a DFA M from $\mathbf{T}$; 2. Convert M into DTA $\mathcal{H}$.

Given a prepared table
$\mathbf{T}=(\Sigma,\bm{\Sigma_{G}},\bm{\Sigma_{r}},\bm{S},\bm{R},\bm{E},f,g)$,
the learner first builds a DFA $\text{M}=(L_{M},l_{M}^{0},F_{M},$
$\Sigma_{M},\Delta_{M})$ as follows.

  * •

the finite set of locations $L_{M}=\\{l_{\mathit{row}(s)}\mid s\in\bm{S}\\}$;

  * •

the initial location $l_{M}^{0}=l_{\mathit{row}(\epsilon)}$ for
$\epsilon\in\bm{S}$;

  * •

the finite set of accepting locations $F_{M}=\\{l_{\mathit{row}(s)}\mid
f(s\cdot\epsilon)=+\text{ for }s\in\bm{S}\text{ and }\epsilon\in\bm{E}\\}$;

  * •

the finite abstract alphabet
$\Sigma_{M}=\\{\bm{\sigma_{r}}\in\bm{\Sigma_{r}}\mid\gamma_{r}\bm{\sigma_{r}}\in\bm{S}\cup\bm{R}\text{
for }\gamma_{r}\in\bm{\Sigma_{r}}^{*}\\}$;

  * •

the finite set of transitions
$\Delta_{M}=\\{(l_{\mathit{row}(\gamma_{r})},\bm{\sigma_{r}},l_{\mathit{row}(\gamma_{r}\bm{\sigma_{r}})})\mid$
$\gamma_{r},\gamma_{r}\bm{\sigma_{r}}\in\bm{S}\cup\bm{R}\text{ for
}\bm{\sigma_{r}}\in\bm{\Sigma_{r}}\\}$.

The basic idea in the above construction is that we view
$\bm{\sigma_{r}}\in\bm{\Sigma_{r}}$ as an abstract action if $\bm{\sigma_{r}}$
occurs in the table and consider each row in the table as the location which
is reached by the row. We label the locations by function $\mathit{row}$. The
constructed DFA M is compatible with the timed observation table $\mathbf{T}$
in a sense captured by the following lemma.

###### Lemma 4.5.

Given a prepared observation table
$\mathbf{T}=(\Sigma,\bm{\Sigma_{G}},\bm{\Sigma_{r}},$
$\bm{S},\bm{R},\bm{E},f,g)$, for all $\gamma_{r}\cdot
e\in(\bm{S}\cup\bm{R})\cdot\bm{E}$, we have

  * •

if $f(\gamma_{r},e)=+$, there is $\gamma_{r}^{\prime}\in
vs_{\mathcal{A}}(\gamma_{r},e)$ such that
$resets(\gamma_{r}^{\prime})=g(\gamma_{r},e)$ and
$\gamma_{r}\gamma_{r}^{\prime}$ is accepted in the constructed DFA M;

  * •

if $f(\gamma_{r},e)=-$ and $vs_{\mathcal{A}}(\gamma_{r},e)\neq\emptyset$,
there is $\gamma_{r}^{\prime}\in vs_{\mathcal{A}}(\gamma_{r},e)$ such that
$resets(\gamma_{r}^{\prime})=g(\gamma_{r},e)$ and
$\gamma_{r}\gamma_{r}^{\prime}$ is not accepted in the constructed DFA M.

  * •

if $f(\gamma_{r},e)=-$ and $vs_{\mathcal{A}}(\gamma_{r},e)=\emptyset$, DFA M
has no accepting word in the form of $\gamma_{r}\gamma_{r}^{\prime}$ such that
$\llbracket vw(\gamma_{r}^{\prime})\rrbracket=e$.

After the DFA M is constructed, the learner constructs a hypothesis
$\mathcal{H}=(L,l_{0},F,\mathcal{C},$ $\Sigma,\Delta)$ from M. In the
hypothesis $\mathcal{H}$, $\mathcal{C}$ is the set of clocks known before
learning and $\Sigma$ is the given alphabet as in $\mathbf{T}$. In addition,
$L=L_{M}$, $l_{0}=l_{M}^{0}$, and $F=F_{M}$. The set of transitions $\Delta$
in $\mathcal{H}$ can be constructed as follows: For any $l\in L_{M}$ and
$\sigma\in\Sigma$, let
$\Psi_{l,\sigma}=\\{\mathbf{v}_{i}\mid(l,(\sigma,\mathbf{v}_{i},\mathbf{b}_{i}),l^{\prime})\in\Delta_{M}\\}$,
then applying the partition function $P^{c}(\cdot)$ to $\Psi_{l,\sigma}$
returns $n$ disjoint clock constraints, written as $I_{1},\cdots,I_{n}$,
satisfying $\mathbf{v}_{i}\in I_{i}$ for any $1\leq i\leq n$, where
$n=|\Psi_{l,\sigma}|$. Then for each transition
$(l,(\sigma,\mathbf{v}_{i},\mathbf{b}_{i}),l^{\prime})\in\Delta_{M}$, we add a
transition $(l,\sigma,I_{i},\\{c_{j}|\mathbf{b}_{i,j}=\top\\},l^{\prime})$ in
$\Delta$. After that, the construction of hypothesis $\mathcal{H}$ is
finished.

###### Definition 4.6 (Partition function).

Given a set of clock valuations $\Psi_{l,\sigma}$, the partition function
$P(\cdot)$ operates on it in the five steps:

  * •

For all clock valuations in $\Psi_{l,\sigma}$, we list them as
$\mathbf{v}_{1},\mathbf{v}_{2},\cdots,$ $\mathbf{v}_{n}$, with
$\\{0\\}^{|\mathcal{C}|}=\mathbf{v}_{1}\preceq\mathbf{v}_{2}\preceq\cdots\preceq\mathbf{v}_{n}$.
Then for $1\leq i\leq n$, we map $\mathbf{v}_{i}$ to a constraint $A_{i}$,
which is defined as

$\quad\quad A_{i}=\begin{cases}\llbracket\mathbf{v}_{i}\rrbracket,&\text{if}\
\ \exists 1\leq j\leq|\mathcal{C}|\text{ satisfying that
}\mathbf{v}_{i,j}>\kappa(c_{j});\\\ \emptyset,&\text{otherwise}.\end{cases}$

We denote the union of $A_{i}$ for all $1\leq i\leq n$ by $U_{0}$.

  * •

After $U_{0}$ is constructed, for $1\leq i\leq n$, we map clock valuation
$\mathbf{v}_{i}$ to a new constraint $U_{i}=\bigwedge_{1\leq
j\leq|\mathcal{C}|}ic_{i,j}$ where

$\quad\quad ic_{i,j}=\begin{cases}c_{j}\geq\mathbf{v}_{i,j},&\text{if}\ \
\mathbf{v}_{i,j}\in\mathbb{N};\\\
c_{j}\textgreater\lfloor\mathbf{v}_{i,j}\rfloor,&\text{otherwise}.\end{cases}$

  * •

Based on $U_{0}$ constructed in the first step and $U_{1},\cdots,U_{n}$
constructed in the second step, map the $n$ clock valuations
$\mathbf{v}_{1},\mathbf{v}_{2},\cdots,\mathbf{v}_{n}$ to the $n$ constraints
$W_{1},W_{2},\cdots,$ $W_{n}$, respectively, where $W_{i}$ is defined as

$\quad\quad\begin{cases}U_{n}-(U_{n}\cap U_{0}),&\text{if}\ \ i=n;\\\
U_{i}-(U_{i}\cap(W_{i+1}\cup W_{i+2}\cup\cdots\cup W_{n}\cup
U_{0})),&\text{otherwise}.\end{cases}$

  * •

Based on $W_{1},\cdots,W_{n}$ and $A_{1},\cdots,A_{n}$, map the $n$ clock
valuations $\mathbf{v}_{1},\mathbf{v}_{2},\cdots,\mathbf{v}_{n}$ to the $n$
constraints $I_{1},I_{2},\cdots,$ $I_{n}$, respectively, which is defined as

$\quad\quad I_{i}=W_{i}+A_{i}.$

  * •

Finally, find whether there are $\mathbf{v}_{i},\mathbf{v}_{j}$ such that
$A_{i}=A_{j}=\emptyset$ and $U_{i}=U_{j}$, but
$\llbracket\mathbf{v}_{i}\rrbracket\neq\llbracket\mathbf{v}_{j}\rrbracket$. If
so, we support that $\mathbf{v}_{i}\preceq\mathbf{v}_{j}$, then after the
previous three steps, $W_{i}=\emptyset$ and
$W_{j}=U_{j}-(U_{j}\cap(W_{j+1}\cup W_{j+2}\cup\cdots\cup W_{n}\cup U_{0}))$
since $U_{i}=U_{j}$. Next, in the fourth step, $I_{i}=\emptyset$ and
$I_{j}=W_{j}$ since $A_{i}=A_{j}=\emptyset$. To map $\mathbf{v}_{i}$ to the
correct partition, let $I_{i}=\llbracket\mathbf{v}_{i}\rrbracket$ and thus the
updated $I_{j}=W_{j}-I_{i}$. Note that after this step, the union of the
updated $I_{i}$ and $I_{j}$ is not changed.

The basic idea of the partition function is to generate disjoint clock
constraints $I_{1},\cdots,I_{n}$ containing the clock valuations. Specially,
we need to generate that for each $\mathbf{v}_{i}$, there is one and only one
final constraint $I_{i}$ containing it. In the first step, to avoid dividing a
region $\llbracket\mathbf{v}_{i}\rrbracket$ into more than one final
constraint, we select $\llbracket\mathbf{v}_{i}\rrbracket$ which may lead to
this situation, add it to $U_{0}$ and guarantee that $U_{0}$ does not
participate in the division operations in the second step and third step. In
the second step, we compute a coarse constraints $U_{i}$ containing the
corresponding clock valuations $\mathbf{v}_{i}$. But they are not disjoint. In
the third step, we guarantee the disjoint property and get the constraints
$W_{i}$. In the fourth step, since $U_{0}$ does not participate in the
division operations in the second step and third step, we select $A_{i}$ from
$U_{0}$ and add it to $W_{i}$. In the second step and third step, we do not
consider the relation between clocks in one clock valuation. But they may form
different regions (constraints). Hence, for two clock valuations such that
$\llbracket\mathbf{v}_{i}\rrbracket\neq\llbracket\mathbf{v}_{j}\rrbracket$ but
$U_{i}=U_{j}$ and $A_{i}=A_{j}=\emptyset$, if
$\mathbf{v}_{i}\preceq\mathbf{v}_{j}$, then $I_{i}=\emptyset$, which means
that $\mathbf{v}_{i}$ has no corresponding final constraint containing it.
Therefore, in the final step, we divide the constraint $I_{j}$ into two
constraints $I_{i}$ and $I_{j}$.

###### Lemma 4.7.

The clock constraints $I_{1},\cdots,I_{n}$ generated by partition function
$P(\cdot)$ are disjoint, i.e. $I_{i}\cap I_{j}=\emptyset$ for all $i\neq j$
and $1\leq i,j\leq n$.

###### Theorem 4.8.

$P(\cdot)$ returns a partition on $\mathbb{R}_{\geq
0}^{\lvert\mathcal{C}\rvert}$.

###### Lemma 4.9.

Given a DFA $\text{M}=(L_{M},l^{0}_{M},F_{M},\Sigma_{M},\Delta_{M})$, which is
generated from a prepared timed observation table $\mathbf{T}$, the hypothesis
$\mathcal{H}=(L,l_{0},F,\mathcal{C},\Sigma,\Delta)$ is transformed from M. For
all $\gamma_{r}\cdot e\in(\bm{S}\cup\bm{R})\cdot\bm{E}$, we have

  * •

if $f(\gamma_{r},e)=+$, there is $\gamma_{r}^{\prime}\in
vs_{\mathcal{A}}(\gamma_{r},e)$ such that
$resets(\gamma_{r}^{\prime})=g(\gamma_{r},e)$ and
$\gamma_{r}\gamma_{r}^{\prime}$ is accepted in the constructed hypothesis
$\mathcal{H}$;

  * •

if $f(\gamma_{r},e)=-$ and $vs_{\mathcal{A}}(\gamma_{r},e)\neq\emptyset$,
there is $\gamma_{r}^{\prime}\in vs_{\mathcal{A}}(\gamma_{r},e)$ such that
$resets(\gamma_{r}^{\prime})=g(\gamma_{r},e)$ and
$\gamma_{r}\gamma_{r}^{\prime}$ is not accepted in the constructed hypothesis
$\mathcal{H}$.

  * •

if $f(\gamma_{r},e)=-$ and $vs_{\mathcal{A}}(\gamma_{r},e)=\emptyset$,
$\mathcal{H}$ has no accepting word in the form of
$\gamma_{r}\gamma_{r}^{\prime}$ such that $\llbracket
vw(\gamma_{r}^{\prime})\rrbracket=e$.

###### Theorem 4.10.

The hypothesis $\mathcal{H}$ is a CTA.

###### Theorem 4.11.

For all $\gamma_{r}\cdot e\in(\bm{S}\cup\bm{R}\cdot\bm{E})$, for every valid
clocked word $\gamma^{\prime}$ such that
$\llbracket\gamma^{\prime}\rrbracket=\llbracket vw(\gamma_{r})\rrbracket\cdot
e$, $\mathcal{H}$ accepts $\pi(\gamma^{\prime})=\gamma_{r}^{\prime}$ if and
only if $f(\gamma_{r},e)=+$.

###  4.3. Equivalence query and counterexample processing

The equivalence problem determining whether
$\mathcal{L}(\mathcal{H})=\mathcal{L}(\mathcal{A})$ can be decomposed into the
two-side inclusion problem, i.e., whether
$\mathcal{L}(\mathcal{H})\subseteq\mathcal{L}(\mathcal{A})$ and
$\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\mathcal{H})$. Since the
deterministic timed automata are closed under complementation (Alur and Dill,
1994), we can implement the equivalence oracle as follows:
$\mathcal{L}(\mathcal{H})\subseteq\mathcal{L}(\mathcal{A})$ iff
$\mathcal{L}(\mathcal{H})\cap\overline{\mathcal{L}(\mathcal{A})}=\emptyset$,
and $\mathcal{L}(\mathcal{A})\subseteq\mathcal{L}(\mathcal{H})$ iff
$\mathcal{L}(\mathcal{A})\cap\overline{\mathcal{L}(\mathcal{H})}=\emptyset$.
If $\mathcal{L}(\mathcal{H})\not\subseteq\mathcal{L}(\mathcal{A})$, there is a
delay-timed word $\omega$ where the corresponding run $\rho$ in $\mathcal{H}$
reaches an accepting location and the corresponding run $\rho^{\prime}$ in
$\mathcal{A}$ reaches an unaccepting location. In this case, the teacher
provides the corresponding reset-delay-timed word of $\omega_{r}$ in the
target automaton $\mathcal{A}$ as a negative counterexample
$\mathit{ctx}_{-}=(\omega_{r},-)$. Similarly, if
$\mathcal{L}(\mathcal{A})\not\subseteq\mathcal{L}(\mathcal{H})$, the teacher
provides a positive counterexample $\mathit{ctx}_{+}=(\omega_{r},+)$. When
receiving a counterexample $\mathit{ctx}=(\omega_{r},+/-)$, the learner
converts the counterexample to a reset-clocked word
$\gamma_{r}=(\sigma_{1},\mathbf{v}_{1},\mathbf{b}_{1})(\sigma_{2},\mathbf{v}_{2},\mathbf{b}_{2})\cdots(\sigma_{n},\mathbf{v}_{n},\mathbf{b}_{n})$
and add all prefixes of $\gamma_{r}$ to $\bm{R}$ except for those already in
$\bm{S}\cup\bm{R}$. According to the definition of the reset-clocked word,
$\omega_{r}$ and $\gamma_{r}$ trigger the same sequence of transitions in
$\mathcal{A}$. According to the contraposition of Theorem 4.1, if $\omega$ is
an evidence of $\mathcal{L}(\mathcal{H})\neq\mathcal{L}(\mathcal{A})$,
$\gamma_{r}$ is an evidence of
$\mathscr{L}_{r}(\mathcal{H})\neq\mathscr{L}_{r}(\mathcal{A})$.

###  4.4. Learning algorithm

input : the timed observation table
$\mathbf{T}=(\Sigma,\bm{\Sigma_{G}},\bm{\Sigma_{r}},\bm{S},\bm{R},\bm{E},f,g)$;
the number of clocks $|\mathcal{C}|$.

output : the hypothesis $\mathcal{H}$ recognizing the target language
$\mathcal{L}$.

$\bm{S}\leftarrow\\{\epsilon\\}$;
$\bm{R}\leftarrow\\{\pi(\gamma)\mid\gamma=(\sigma,\\{0\\}^{|\mathcal{C}|}),\forall\sigma\in\Sigma\\}$;
$\bm{E}\leftarrow\\{\epsilon\\}$ ;

// initialization

1 fill $\mathbf{T}$ by membership queries;

2 $\mathit{equivalent}$ $\leftarrow$ $\bot$;

3 while  _$\mathit{equivalent}$ = $\bot$_ do

$\mathit{prepared}$ $\leftarrow$ is_prepared($\mathbf{T}$) ;

// whether the table is prepared

4 while  _$\mathit{prepared}$ = $\bot$_ do

5 if  _$\mathbf{T}$ is not closed_ then

6 make_closed($\mathbf{T}$)

7 if  _$\mathbf{T}$ is not consistent_ then

8 make_consistent($\mathbf{T}$)

9 if  _$\mathbf{T}$ is not evidence-closed_ then

10 make_evidence_closed($\mathbf{T}$)

11 $\mathit{prepared}$ $\leftarrow$ is_prepared($\mathbf{T}$);

12

$\text{M}\leftarrow$ build_DFA($\mathbf{T}$) ;

// transforming $\mathbf{T}$ to a DFA M

$\mathcal{H}\leftarrow$ build_hypothesis(M) ;

// constructing a hypothesis $\mathcal{H}$ from M

13 $\mathit{equivalent}$, $\mathit{ctx}$ $\leftarrow$
equivalence_query($\mathcal{H}$);

14 if  _$\mathit{equivalent}$ = $\bot$_ then

ctx_processing($\mathbf{T}$, $\mathit{ctx}$) ;

// counterexample processing

15

16

17return $\mathcal{H}$;

Algorithm 2 Learning deterministic timed automata from a powerful teacher

The learning process that integrates all the previously stated ingredients is
presented in Algorithm 2. First, the learner initializes a timed observation
table $\mathbf{T}$, where $\bm{S}=\\{\epsilon\\}$, $\bm{E}=\\{\epsilon\\}$.
For each $\sigma\in\Sigma$, the learner obtains the corresponding reset-
clocked word $\pi(\gamma)$ and the acceptance status in $\mathcal{A}$ of the
clocked word $\gamma=(\sigma,\\{0\\}^{\lvert\mathcal{C}\rvert})$ through
membership queries and adds the results to $\bm{R}$. Before constructing a
hypothesis, the learner performs several rounds of operations described in
Section 4.1 until $\mathbf{T}$ is prepared. Then, a hypothesis $\mathcal{H}$
is constructed leveraging an intermediate DFA M and submitted to the teacher
for an equivalence query. If the answer is positive, $\mathcal{H}$ recognizes
the target language. Otherwise, the learner receives a counterexample
$\mathit{ctx}$ to update $\mathbf{T}$. The whole procedure repeats until the
teacher gives a positive answer to an equivalence query.

###### Theorem 4.12.

Algorithm 2 terminates and returns a CTA $\mathcal{H}$ which recognizes the
target timed language $\mathcal{L}$.

###  4.5. Complexity

Suppose that $\mathcal{L}$ is a target timed language accepted by a DTA
$\mathcal{A}$, let $n=\lvert L\rvert$ represent the number of locations of
$\mathcal{A}$, $m=\lvert\Sigma\rvert$ represent the size of the alphabet,
$\kappa$ be a function mapping each clock $c\in\mathcal{C}$ to the largest
integer appearing in the guards over $c$ and $\Lambda=|\mathcal{C}|!\cdot
2^{|\mathcal{C}|}\cdot\prod_{c\in\mathcal{C}}(2\kappa(c)+2)$ represent the
bound of the number of clock regions. We measure the number of queries.

Equivalence query. According to the proof of Theorem 4.12, $\mathcal{H}$ has
at most $n\cdot\Lambda$ locations. The number of transitions from a location
for an action is at most $\Lambda$. Therefore, the number of transitions in
$\mathcal{H}$ is at most $mn\Lambda^{2}$. As every counterexample adds at
least one fresh transition to $\mathcal{H}$ if considering each final timing
constraint of the partition corresponds to a transition, the number of
equivalence queries is bounded by $mn\Lambda^{2}$.

Membership query. In order to count the number of membership queries,
$(\lvert\bm{S}\rvert+\lvert\bm{R}\rvert)\cdot\lvert\bm{E}\rvert$ needs to be
counted. Since in the observation table, $\bm{E}$ is used to distinguish the
elements in $\bm{S}$, we have $|\bm{E}|\leq n\cdot\Lambda$. Next,
$\lvert\bm{R}\rvert$ is analyzed as follows. Let $h$ denote the maximum length
of all counterexamples obtained by the learner. The algorithm adds elements to
$\bm{R}$ in three cases: processing of counterexamples, making $\mathbf{T}$
closed, and making $\mathbf{T}$ evidence-closed. In the first case, because
the number of counterexamples equals to the number of equivalence queries,
which is bounded by $mn\Lambda^{2}$, the number of prefixes added to $\bm{R}$
is at most $hmn\Lambda^{2}$ in this case. In the second case, since for each
prefix in $\bm{S}$ and each action, there is a corresponding prefix in
$\bm{R}$, the number of prefixes added to $\bm{R}$ in this step is at most
$mn\cdot\Lambda$. In the last case, the number of prefixes added to $\bm{R}$
depends on $\lvert\bm{S}\rvert\cdot\lvert\bm{E}\rvert$, which is at most
$(n\cdot\Lambda)^{2}$. Therefore, the number of membership queries is bounded
by $(n\cdot\Lambda+hmn\Lambda^{2}+mn\cdot\Lambda+(n\cdot\Lambda)^{2})\cdot
n\cdot\Lambda$.

Reset information query. In each membership query, the number of reset
information queries depends on the length of the suffix. Let $p$ be the length
of the longest suffix in $\bm{E}$. During the learning process, each new
suffix added to $\bm{E}$ is composed of a region word with length one and a
suffix that has already been in $\bm{E}$. Therefore, $p$ is at most
$\lvert\bm{E}\rvert-1$. Hence, the number of reset information queries to fill
the observation table is bounded by
$(\lvert\bm{E}\rvert-1)\cdot(\lvert\bm{S}\rvert+\lvert\bm{R}\rvert)\cdot\lvert\bm{E}\rvert$.
Moreover, to make the observation table closed, for each $s\in\bm{S}$, $m$
reset information queries are needed. As a result, the number in total is
bounded by
$(\lvert\bm{E}\rvert-1)\cdot(\lvert\bm{S}\rvert+\lvert\bm{R}\rvert)\cdot\lvert\bm{E}\rvert+m\cdot\lvert\bm{S}\rvert$.

##  5\. Learning DTA from a normal teacher

In this section, we extend the learning algorithm for learning a DTA
$\mathcal{A}$ from a normal teacher. In this situation, the teacher can only
answer the standard membership query and equivalence query. In a standard
membership query, the input is delay-timed words, and the teacher returns
whether the timed word is in the target timed language or not. In a standard
equivalence query, if $\mathcal{L}(\mathcal{A})\neq\mathcal{L}(\mathcal{H})$,
the teacher provides a delay-timed word as a counterexample.

The algorithm in the normal teacher situation is based on the learning
procedure in Section 4. In this algorithm, the structure of the observation
table is unchanged. $\bm{S}\cup\bm{R}$ still stores reset-clocked words, and
$\bm{E}$ still stores region words. In order to obtain reset-clocked words
from delay-timed words of the membership queries, the learner _guesses_ clock
reset information in the table.

Since guessing the reset information, for each reset case, it will result in a
table instance. A list $\mathit{ToExplore}$ is maintained to collect all these
table instances that need to be explored later. We use breadth-first search
(BFS) to explore the tables in $\mathit{ToExplore}$, which is crucial for
ensuring the termination. Since the algorithm cannot detect incorrect guesses
of reset information, depth-first search (DFS) may not terminate if it follow
a branch that never finds the correct hypothesis. Moreover, our BFS is not
based on a strictly FIFO queue. In each round, we take out the table instance
with the minimal number of guessed reset. Since the table instance contains
reset information, the operations on the table instance are the same as those
in the powerful teacher situation. Details are as follows.

The initial tables in $\mathit{ToExplore}$ are as follows. For each action
$\sigma\in\Sigma$, there is one row in $\bm{R}$ corresponding to the clocked
word $\gamma=(\sigma,\\{0\\}^{\lvert\mathcal{C}\rvert})$. To transform it to a
reset-clocked word, the learner needs to guess the reset information of each
clock in $\gamma$, get a reset-clocked word
$\gamma_{r}=(\sigma,\\{0\\}^{\lvert\mathcal{C}\rvert},\mathbf{b})$ and add
$\gamma_{r}$ into $\bm{R}$. For each action $\sigma$, there are
$2^{\lvert\mathcal{C}\rvert}$ possible combinations of guesses. So, in this
step, $2^{\lvert\mathcal{C}\rvert\lvert\Sigma\rvert}$ table instances are
added to $\mathit{ToExplore}$.

In each iteration of the algorithm, one table instance is taken out of
$\mathit{ToExplore}$. The learner checks whether the table is closed,
consistent, and evidence-closed. If the table is not closed, i.e. there exists
$r\in\bm{R}$ such that $row(r)\neq row(s)$ for all $s\in\bm{S}$. In this case,
the learner moves $r$ from $\bm{R}$ to $\bm{S}$. Then for each
$\sigma\in\Sigma$, a word
$\gamma=vw(r)\cdot(\sigma,\\{0\\}^{\lvert\mathcal{C}\rvert})$ is created, and
the learner needs to guess the reset information of
$(\sigma,\\{0\\}^{\lvert\mathcal{C}\rvert})$. Similar to the initialization of
the table, there are $2^{\lvert\mathcal{C}\rvert}$ possible combinations of
guesses for action $\sigma$. Therefore,
$2^{\lvert\mathcal{C}\rvert\lvert\Sigma\rvert}$ unfilled table instances will
be generated. Next, these $2^{\lvert\mathcal{C}\rvert\lvert\Sigma\rvert}$
unfilled table instances are filled by membership queries. Because the learner
cannot initiate the reset information query, for each added entry in $\bm{R}$,
it is necessary to guess reset information for all transitions in
$e\in\bm{E}$. For an element $e\in\bm{E}$, the reset information of $\lvert
e\rvert\cdot\lvert\mathcal{C}\rvert$ clocks needs to be guessed. Therefore,
for each new row in $\bm{R}$, a total of
$(\sum_{e_{i}\in\bm{E}\setminus\\{\epsilon\\}}{\lvert
e_{i}\rvert})\cdot\lvert\mathcal{C}\rvert$ clock reset information needs to be
guessed. Therefore, this procedure inserts at most
$2^{(\sum_{e_{i}\in\bm{E}\setminus\\{\epsilon\\}}{\lvert
e_{i}\rvert})\cdot\lvert\mathcal{C}\rvert^{2}\cdot\lvert\Sigma\rvert}$ table
instances to $\mathit{ToExplore}$.

If the table is not consistent, i.e. there exist two reset-clocked words
$\gamma_{r},\gamma_{r}^{\prime}\in\bm{S}\cup\bm{R}$ at least, for
$\bm{\sigma_{r}},\bm{\sigma_{r}}^{\prime}\in\bm{\Sigma_{r}}$ such that
$\llbracket vw(\bm{\sigma_{r}})\rrbracket=\llbracket
vw(\bm{\sigma_{r}}^{\prime})\rrbracket$, both $\gamma_{r}\bm{\sigma_{r}}$ and
$\gamma_{r}^{\prime}\bm{\sigma_{r}}^{\prime}\in\bm{S}\cup\bm{R}$. However,
$\mathit{row}(\gamma_{r})=\mathit{row}(\gamma_{r}^{\prime})$ but
$\mathit{row}(\gamma_{r}\bm{\sigma_{r}})\neq\mathit{row}(\gamma_{r}^{\prime}\bm{\sigma_{r}^{\prime}})$
or $resets(\bm{\sigma_{r}})\neq resets(\bm{\sigma_{r}}^{\prime})$. Let
$e\in\bm{E}$ be one place where they are different. Then $\llbracket
vw(\bm{\sigma_{r}})\rrbracket\cdot e$ needs to be added to $\bm{E}$. For each
entry in $\bm{S}\cup\bm{R}$, all transitions in $\llbracket
vw(\bm{\sigma_{r}})\rrbracket\cdot e$ need to be guessed, and then the table
can be filled. Hence, $2^{\lvert\llbracket vw(\bm{\sigma_{r}})\rrbracket\cdot
e\rvert\cdot\lvert\mathcal{C}\rvert\cdot(\lvert\bm{S}\rvert+\lvert\bm{R}\rvert)}$
filled table instances will be generated and inserted into
$\mathit{ToExplore}$. The operation for making tables evidence-closed is
analogous.

If the current table is prepared, the learner builds a hypothesis
$\mathcal{H}$ and makes an equivalence query to the teacher. If the answer is
negative, the teacher gives a delay-timed word $\omega$ as a counterexample.
The learner first finds the longest reset-clocked word $\gamma_{r}$ in
$\bm{S}\cup\bm{R}$, which agrees with a prefix of $\omega$ after converting
$\gamma_{r}$ to a delay-timed word. Then the reset information of $\gamma_{r}$
is copied to $\omega$, and the reset information of the remainder of $\omega$
needs to be guessed. Hence, at most
$2^{\lvert\omega\rvert\cdot\lvert\mathcal{C}\rvert}$ unfilled table instances
are generated. To fill these table instances, the reset information of
$\bm{E}$ also needs to be guessed. Therefore, there are at most
$2^{\lvert\omega\rvert\cdot(\sum_{e_{i}\in\bm{E}\setminus\\{\epsilon\\}}{\lvert
e_{i}\rvert})\cdot\lvert\mathcal{C}\rvert^{2}}$ filled table instances need to
be added in $\mathit{ToExplore}$.

###### Theorem 5.1.

The algorithm learning DTA from a normal teacher terminates and returns a
correct CTA $\mathcal{H}$.

_Complexity analysis._ If
$\mathbf{T}=(\Sigma,\bm{\Sigma_{G}},\bm{\Sigma_{r}},\bm{S},\bm{R},\bm{E},f,g)$
is the final table corresponding to the correct hypothesis, the number of
guessed resets in $\bm{S}\cup\bm{R}$ is
$(|\bm{S}|+|\bm{R}|)\cdot\lvert\mathcal{C}\rvert$, and the number of guessed
resets for entries in each row of the table is
$(\sum_{e_{i}\in\bm{E}\setminus\\{\epsilon\\}}{\lvert
e_{i}\rvert})\cdot\lvert\mathcal{C}\rvert$. Since we use BFS to explore the
tables in $ToExplore$ w.r.t. the size of the tables, a smaller table is always
handled before any larger ones. Hence, before finding the final table
$\mathbf{T}$ corresponding to the correct hypothesis, the number of the
handled tables is bounded by
$\mathcal{O}(2^{(|\bm{S}|+|\bm{R}|)\cdot\lvert\mathcal{C}\rvert^{2}\cdot(\sum_{e_{i}\in\bm{E}\setminus\\{\epsilon\\}}{\lvert
e_{i}\rvert})})$.

##  6\. Experiments

We have implemented the a prototype named DTAL in JAVA for our learning
algorithms of deterministic timed automata with multiple clocks. Specially, we
denote the implementations for the powerful and the normal teachers by
DTAL_powerful and by DTAL_normal, respectively. We compared our methods with
LearnTA proposed in (Waga, 2023) for learning DTAs, and with LearnRTA proposed
in (An et al., 2021a) for learning real-time automata (RTAs). These two
algorithms are implemented in C++ and Python, respectively. Note that we
omitted checking of evidence-closed condition in our experiments to avoid
adding too many extra rows in $\bm{R}$. The evaluations have been carried out
on an Intel Core-i7 processor with 16GB RAM running 64-bit Ubuntu.

###  6.1. Evaluation on DTAL_powerful

Experiment on RTAs. We first compared the performance of the learning
algorithm DTAL_powerful with the algorithm LearnRTA proposed in (An et al.,
2021a) by learning real-time automata (RTAs). Since RTA can be viewed as a TA
with only one clock which resets at every transition, we can directly use
DTAL_powerful to learn real-time automata instead of DTAL_normal by trivially
answering reset information queries. We used the $240$ randomly generated RTAs
from (An et al., 2021a), which are divided into $12$ groups depending on
different numbers of locations, size of alphabet, and maximum number of time
intervals that can be generated by a single division. These three numbers make
up case ID. Table 1 summarizes the experimental results. It can be seen that
the number of equivalence queries needed in DTAL_powerful is always very close
to that in LearnRTA. However, the number of membership queries needed in
DTAL_powerful is sightly smaller than that in LearnRTA. This is because that
we omitted checking of evidence-closed condition. Besides, the runtime needed
in DTAL_powerful is shorter than that in LearnRTA. This may be due to the fact
that these two algorithms are written in JAVA and Python, respectively.

Experiment on DTAs. We first compared the performance of our learning
algorithm DTAL_powerful with the algorithm LearnTA proposed in (Waga, 2023) on
learning the DTA “unbalanced:2” in (Waga, 2023) as an example. The target
automaton contains $5$ locations, $1$ action and $5$ transitions. Our
algorithm DTAL_powerful yields a timed automaton with only $8$ locations
(including the “sink” location) and $2$ clocks, whereas LearnTA yields a timed
automaton with $25$ locations and $7$ clocks. It gives an evidence that our
algorithm can return a much smaller DTA with fewer number of clocks. Since
when learning a DTA by using the algorithm DTAL_normal, the final table will
never be larger than the final table in the powerful teacher situation.
Therefore, the experimental result gives us highly confidence that DTAL_normal
will return a much smaller automaton than LearnTA once it terminates.

Table 1. Experimental results on learning RTAs. #Reset, #Membership,
#Equivalence represent the number of reset information queries, membership
queries and equivalence queries needed during the learning process,
respectively. $n$ is the number of locations of the learned automaton.

Case ID | Algorithm | #Reset | #Membership | #Equivalence | $n$ | time(s)
---|---|---|---|---|---|---
4-4-4 | DTAL_powerful | $228.0$ | $267.6$ | $28.7$ | $5$ | $2.9$
LearnRTA | $-$ | $298.4$ | $28.3$ | $5$ | $4.5$
6-4-4 | DTAL_powerful | $529.3$ | $578.8$ | $46.8$ | $7$ | $16.4$
LearnRTA | $-$ | $696.0$ | $45.6$ | $7$ | $37.1$
7-2-4 | DTAL_powerful | $388.2$ | $383.3$ | $32.6$ | $8$ | $3.5$
LearnRTA | $-$ | $554.0$ | $31.2$ | 8 | $9.0$
7-3-4 | DTAL_powerful | $458.2$ | $456.9$ | $37.6$ | $8$ | $6.5$
LearnRTA | $-$ | $630.4$ | $36.7$ | 8 | $17.0$
7-4-2 | DTAL_powerful | $469.9$ | $436.9$ | $23.6$ | $8$ | $2.9$
LearnRTA | $-$ | $630.0$ | $22.8$ | 8 | $11.0$
7-4-3 | DTAL_powerful | $470.9$ | $496.6$ | $32.0$ | $8$ | $5.8$
LearnRTA | $-$ | $680.0$ | $31.4$ | 8 | $16.1$
7-4-4 | DTAL_powerful | $529.4$ | $571.5$ | $46.6$ | $8$ | $14.0$
LearnRTA | $-$ | $793.6$ | $45.2$ | 8 | $34.7$
7-4-5 | DTAL_powerful | $613.6$ | $639.3$ | $50.0$ | $8$ | $19.7$
LearnRTA | $-$ | $831.3$ | $48.5$ | 8 | $46.0$
7-4-6 | DTAL_powerful | $907.8$ | $986.4$ | $85.2$ | $8$ | $110.3$
LearnRTA | $-$ | $1149.9$ | $83.4$ | 8 | $142.5$
7-4-7 | DTAL_powerful | $1029.8$ | $1143.1$ | $95.0$ | $8$ | $176.1$
LearnRTA | $-$ | $1304.3$ | $93.1$ | 8 | $219.9$
8-4-4 | DTAL_powerful | $804.0$ | $841.4$ | $56.3$ | $9$ | $33.9$
LearnTA | $-$ | $1156.5$ | $54.3$ | 9 | $55.7$
10-4-4 | DTAL_powerful | $1268.2$ | $1291.1$ | $70.2$ | $11$ | $94.1$
LearnTA | $-$ | $1843.3$ | $67.9$ | 11 | $167.7$

###  6.2. Evaluation on DTAL_normal

Table 2. Experimental results on learning DTAs. Each row represents one DTA
where $\lvert L\rvert$ is the number of locations, $\lvert\Sigma\rvert$ is the
alphabet size, $\lvert\mathcal{C}\rvert$ is the number of clock variables, and
$\kappa(\mathcal{C})$ is the maximum constant in the guards in the DTA. $n$ is
the number of locations of the learned automaton. $-$ represents a timeout
(1.5 hours).

$\lvert L\rvert$ | $\lvert\Sigma\rvert$ | $\lvert\mathcal{C}\rvert$ | $\kappa(\mathcal{C})$ | Algorithm | #Membership | #Equivalence | $n$ | time(s)
---|---|---|---|---|---|---|---|---
2 | 1 | 2 | 3 | DTAL_normal | $763145$ | $272734$ | $3$ | $2440$
LearnTA | $1189$ | $6$ | $3$ | $0.035$
2 | 1 | 2 | 30 | DTAL_normal | $891513$ | $320108$ | $3$ | $5093$
LearnTA | $793983$ | $33$ | $29$ | $631$
3 | 1 | 2 | 3 | DTAL_normal | $1020044$ | $102024$ | $3$ | $1269$
LearnTA | $1251$ | $7$ | $4$ | $0.009$
3 | 1 | 2 | 30 | DTAL_normal | $914554$ | $122622$ | $3$ | $2588$
LearnTA | $1874410$ | $49$ | $39$ | $475$
4 | 1 | 2 | 50 | DTAL_normal | $-$ | $-$ | $-$ | $-$
LearnTA | $-$ | $-$ | $-$ | $-$

Table 2 summarizes the experimental results. It shows that, as long as the
maximum constant $\kappa(\mathcal{C})$ increases, the number of locations in
the timed automata learned by LearnTA increases dramatically. This may be due
to the fact that in the timed observation table of LearnTA, prefixes consist
of a series of simple elementary languages. Hence, as the value of
$\kappa(\mathcal{C})$ increases, the number of prefixes in the timed
observation table increases significantly, thus affecting the number of
locations of the hypothesis. Besides, in LearnTA, the number of the membership
queries blows up exponentially to the value of $\kappa(\mathcal{C})$. This is
because that when learning DTA from a normal teacher, symbolic membership
queries is forbidden, a symbolic membership query needs to be reduced to
finitely many membership queries. However, the size of this decomposition
exponentially blows up with respect to $\kappa(\mathcal{C})$. Similarly, in
LearnTA, the number of equivalence queries also grows as $\kappa(\mathcal{C})$
increases.

The experimental results show that DTAL in the normal teacher situation
requires more membership queries and equivalence queries. This is because when
guessing the reset information of the target DTA, a large number of
observation tables are generated, and more membership queries and equivalence
queries are needed to maintain these observation tables. But it can return a
much smaller automaton, which benefits from the equivalence relation presented
in Section 3. The results also show that both algorithms, i.e., DTAL and
LearnTA, need improvements before being applied in practice.

##  7\. Related work

Active learning. In (Grinchtein et al., 2006, 2010), Grinchtein et al. propose
learning algorithms for deterministic event-recording automata (ERA) (Alur et
al., 1999). ERA is a kind of timed automata with several restrictions on
clocks such that for every action $a$, a clock $x_{a}$ is associated to record
the time length from the last occurrence of $a$ to the current. Recently, in
(Henry et al., 2020), Henry et al. consider the learning problem of reset-free
ERA in which some transitions may reset no clocks. In (An et al., 2020), An et
al. provide an active learning method for deterministic one-clock timed
automata (DOTA). After that, several improvements have been proposed, e.g.,
using PAC learning (Shen et al., 2020), mutation testing (Tang et al., 2022),
SMT solving (Xu et al., 2022), etc. Real-time automata can be viewed as a kind
of DOTA such that the single clock resets at every transition. The efficient
learning algorithms have been designed in both the deterministic case (An et
al., 2021a) and the nondeterministic case (An et al., 2021b). Instead of using
clocks, the “timer” is another kind of model to record the time length. It can
be assigned a value, and if it counts down to zero, a visible timeout signal
will be triggered. In (Caldwell et al., 2016), Caldwell et al. proposed an
algorithm for learning the Mealy machine with timers from programmable logic
controllers. In (Vaandrager et al., 2021), Vaandrager et al. presented an
efficient learning algorithm for such models with one timer. Recently, an
active learning algorithm of DTA with Myhill-Nerode style characterization is
proposed in (Waga, 2023). However, with a large maximum constant in the guards
in the target DTA, the number of queries required during learning and the
number of locations in the learned DTA grows significantly in this algorithm.
Our algorithm can return a much smaller DTA.

Passive learning. In (Verwer et al., 2007, 2012), an algorithm is proposed to
learn deterministic RTA (Dima, 2001) from labelled time-stamped event
sequences. A passive learning algorithm for timed automata with one clock is
further proposed in (Verwer et al., 2009, 2011). In (Tappler et al., 2019),
Tappler et al. present a passive learning algorithm for deterministic timed
automata based on genetic programming (GP). In further, by introducing a
testing process on the system under test (SUT), Aichernig et al. add an active
manner in the GP-based learning procedure (Aichernig et al., 2020). Recently,
in (Tappler et al., 2022), Tappler et al. present an SMT-based passive
learning algorithm for deterministic timed automata. There are also some works
on passive learning of timed automata in practical cases (Pastore et al.,
2017; Cornanguer et al., 2022) and dynamical systems (Jin et al., 2021). As
mentioned before, passive learning algorithms cannot guarantee the correctness
of the learned model.

##  8\. Conclusion and Future work

We propose an active learning approach for deterministic multi-clock timed
automata. We transform the problem into learning the reset-clocked language of
the target automaton. We first introduce an equivalence relation for reset-
clocked languages. Based on it, we present a learning algorithm for
deterministic timed automata in the powerful teacher situation by designing
the membership query and the reset information query over region words. In
further, we drop the reset information query and present the active learning
algorithm in the normal teacher situation where the learner can only make
standard membership queries and equivalence queries.

In future work, we intend to improve the algorithm by using the technique
reported in (Xu et al., 2022) so that it can be used in learning timed models
with large sizes of practical systems.

###### Acknowledgements.

We thank the anonymous reviewers for their valuable feedback and suggestions
for improving the quality of this paper. Y. Teng and M. Zhang are supported by
Shanghai 2023 “Science and Technology Innovation Action Plan”: Special Project
for Key Technical Breakthrough of Blockchain (No. 23511100800), and the
National Natural Science Foundation of China (No. 61972284, 62032019). J. An
is supported by ERATO HASUO Metamathematics for Systems Design Project (No.
JPMJER1603), JST.

## References

  * (1)
  * Aichernig et al. (2020) Bernhard K. Aichernig, Andrea Pferscher, and Martin Tappler. 2020\.  From Passive to Active: Learning Timed Automata Efficiently. In _Proceedings of the 12th International Symposium on NASA Formal Methods, NFM 2020_ _(LNCS, Vol. 12229)_. Springer, 1–19.  https://doi.org/10.1007/978-3-030-55754-6_1
  * Alur and Dill (1994) Rajeev Alur and David L. Dill. 1994.  A Theory of Timed Automata.  _Theor. Comput. Sci._ 126, 2 (1994), 183–235.  https://doi.org/10.1016/0304-3975(94)90010-8
  * Alur et al. (1999) Rajeev Alur, Limor Fix, and Thomas A. Henzinger. 1999\.  Event-Clock Automata: A Determinizable Class of Timed Automata.  _Theor. Comput. Sci._ 211, 1-2 (1999), 253–273.  https://doi.org/10.1016/S0304-3975(97)00173-4
  * Alur et al. (2005) Rajeev Alur, P. Madhusudan, and Wonhong Nam. 2005\.  Symbolic Compositional Verification by Learning Assumptions. In _Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005_ _(LNCS, Vol. 3576)_. Springer, 548–562.  https://doi.org/10.1007/11513988_52
  * An et al. (2020) Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2020.  Learning One-Clock Timed Automata. In _26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020_ _(LNCS, Vol. 12078)_. Springer, 444–462.  https://doi.org/10.1007/978-3-030-45190-5_25
  * An et al. (2021a) Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2021a.  Learning real-time automata.  _Sci. China Inf. Sci._ 64, 9 (2021).  https://doi.org/10.1007/s11432-019-2767-4
  * An et al. (2021b) Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2021b.  Learning Nondeterministic Real-Time Automata.  _ACM Trans. Embed. Comput. Syst._ 20, 5s (2021), 99:1–99:26.  https://doi.org/10.1145/3477030
  * Angluin (1978) Dana Angluin. 1978\.  On the Complexity of Minimum Inference of Regular Sets.  _Inf. Control._ 39, 3 (1978), 337–350.  https://doi.org/10.1016/S0019-9958(78)90683-6
  * Angluin (1987) Dana Angluin. 1987\.  Learning Regular Sets from Queries and Counterexamples.  _Inf. Comput._ 75, 2 (1987), 87–106.  https://doi.org/10.1016/0890-5401(87)90052-6
  * Caldwell et al. (2016) Ben Caldwell, Rachel Cardell-Oliver, and Tim French. 2016\.  Learning Time Delay Mealy Machines From Programmable Logic Controllers.  _IEEE Trans Autom. Sci. Eng._ 13, 2 (2016), 1155–1164.  https://doi.org/10.1109/TASE.2015.2496242
  * Cornanguer et al. (2022) Lénaïg Cornanguer, Christine Largouët, Laurence Rozé, and Alexandre Termier. 2022\.  TAG: Learning Timed Automata from Logs. In _Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022_. AAAI Press, 3949–3958.  https://ojs.aaai.org/index.php/AAAI/article/view/20311
  * Dima (2001) Catalin Dima. 2001\.  Real-Time Automata.  _J. Autom. Lang. Comb._ 6, 1 (2001), 3–23.  https://doi.org/10.25596/jalc-2001-003
  * Fiterau-Brostean et al. (2016) Paul Fiterau-Brostean, Ramon Janssen, and Frits W. Vaandrager. 2016.  Combining Model Learning and Model Checking to Analyze TCP Implementations. In _Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016_ _(LNCS, Vol. 9780)_. Springer, 454–471.  https://doi.org/10.1007/978-3-319-41540-6_25
  * Gold (1978) E. Mark Gold. 1978\.  Complexity of Automaton Identification from Given Data.  _Inf. Control._ 37, 3 (1978), 302–320.  https://doi.org/10.1016/S0019-9958(78)90562-4
  * Grinchtein et al. (2010) Olga Grinchtein, Bengt Jonsson, and Martin Leucker. 2010\.  Learning of event-recording automata.  _Theor. Comput. Sci._ 411, 47 (2010), 4029–4054.  https://doi.org/10.1016/j.tcs.2010.07.008
  * Grinchtein et al. (2006) Olga Grinchtein, Bengt Jonsson, and Paul Pettersson. 2006\.  Inference of Event-Recording Automata Using Timed Decision Trees. In _Proceedings of the 17th International Conference on Concurrency Theory, CONCUR 2006_ _(LNCS, Vol. 4137)_. Springer, 435–449.  https://doi.org/10.1007/11817949_29
  * Henry et al. (2020) Léo Henry, Thierry Jéron, and Nicolas Markey. 2020\.  Active Learning of Timed Automata with Unobservable Resets. In _Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020_ _(LNCS, Vol. 12288)_. Springer, 144–160.  https://doi.org/10.1007/978-3-030-57628-8_9
  * Hopcroft and Ullman (1979) John E. Hopcroft and Jeffrey D. Ullman. 1979.  _Introduction to Automata Theory, Languages and Computation_.  Addison-Wesley.
  * Jin et al. (2021) Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2021.  Inferring Switched Nonlinear Dynamical Systems.  _Formal Aspects Comput._ 33, 3 (2021), 385–406.  https://doi.org/10.1007/S00165-021-00542-7
  * Kearns and Vazirani (1994) Michael J. Kearns and Umesh V. Vazirani. 1994.  _An Introduction to Computational Learning Theory_.  MIT Press.
  * Leucker (2006) Martin Leucker. 2006\.  Learning Meets Verification. In _Proceedings of the 5th International Symposium on Formal Methods for Components and Objects, FMCO 2006_ _(LNCS, Vol. 4709)_. Springer, 127–151.  https://doi.org/10.1007/978-3-540-74792-5_6
  * Pastore et al. (2017) Fabrizio Pastore, Daniela Micucci, and Leonardo Mariani. 2017\.  Timed k-Tail: Automatic Inference of Timed Automata. In _Proceedings of the 10th IEEE International Conference on Software Testing, Verification and Validation, ICST 2017_. IEEE Computer Society, 401–411.  https://doi.org/10.1109/ICST.2017.43
  * Peled et al. (2002) Doron A. Peled, Moshe Y. Vardi, and Mihalis Yannakakis. 2002\.  Black Box Checking.  _Journal of Automata, Languages and Combinatorics_ 7, 2 (2002), 225–246.  https://doi.org/10.25596/jalc-2002-225
  * Schuts et al. (2016) Mathijs Schuts, Jozef Hooman, and Frits W. Vaandrager. 2016\.  Refactoring of Legacy Software Using Model Learning and Equivalence Checking: An Industrial Experience Report. In _Proceedings of the 12th International Conference on Integrated Formal Methods, IFM 2016_ _(LNCS, Vol. 9681)_. Springer, 311–325.  https://doi.org/10.1007/978-3-319-33693-0_20
  * Shen et al. (2020) Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue, and Naijun Zhan. 2020\.  PAC Learning of Deterministic One-Clock Timed Automata. In _Proceedings of the 22nd International Conference on Formal Engineering Methods, ICFEM 2020_ _(LNCS, Vol. 12531)_. Springer, 129–146.  https://doi.org/10.1007/978-3-030-63406-3_8
  * Steffen et al. (2011) Bernhard Steffen, Falk Howar, and Maik Merten. 2011\.  Introduction to Active Automata Learning from a Practical Perspective. In _Proceedings of the 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems - Formal Methods for Eternal Networked Software Systems, SFM 2011_ _(LNCS, Vol. 6659)_. Springer, 256–296.  https://doi.org/10.1007/978-3-642-21455-4_8
  * Tang et al. (2022) Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan, and Naijun Zhan. 2022\.  Learning Deterministic One-Clock Timed Automata via Mutation Testing. In _Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis, ATVA 2022_ _(LNCS, Vol. 13505)_. Springer, 233–248.  https://doi.org/10.1007/978-3-031-19992-9_15
  * Tappler et al. (2019) Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen, and Florian Lorber. 2019\.  Time to Learn - Learning Timed Automata from Tests. In _Proceedings of the 17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019_ _(LNCS, Vol. 11750)_. Springer, 216–235.  https://doi.org/10.1007/978-3-030-29662-9_13
  * Tappler et al. (2022) Martin Tappler, Bernhard K. Aichernig, and Florian Lorber. 2022.  Timed Automata Learning via SMT Solving. In _Proceedings of the 14th International Symposium on NASA Formal Methods , NFM 2022_ _(LNCS, Vol. 13260)_. Springer, 489–507.  https://doi.org/10.1007/978-3-031-06773-0_26
  * Vaandrager (2017) Frits W. Vaandrager. 2017\.  Model learning.  _Commun. ACM_ 60, 2 (2017), 86–95.  https://doi.org/10.1145/2967606
  * Vaandrager et al. (2021) Frits W. Vaandrager, Roderick Bloem, and Masoud Ebrahimi. 2021\.  Learning Mealy Machines with One Timer. In _Proceedings of the 15th International Conference Language and Automata Theory and Applications, LATA 2021_ _(LNCS, Vol. 12638)_. Springer, 157–170.  https://doi.org/10.1007/978-3-030-68195-1_13
  * Verwer et al. (2007) SE Verwer, MM De Weerdt, and Cees Witteveen. 2007.  An algorithm for learning real-time automata. In _Benelearn 2007: Proceedings of the Annual Machine Learning Conference of Belgium and the Netherlands, Amsterdam, The Netherlands, 14-15 May 2007_.
  * Verwer et al. (2009) Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. 2009\.  One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit. In _Language and Automata Theory and Applications, Third International Conference, LATA 2009, Tarragona, Spain, April 2-8, 2009. Proceedings_ _(Lecture Notes in Computer Science, Vol. 5457)_ , Adrian-Horia Dediu, Armand-Mihai Ionescu, and Carlos Martín-Vide (Eds.). Springer, 740–751.  https://doi.org/10.1007/978-3-642-00982-2_63
  * Verwer et al. (2011) Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. 2011\.  The efficiency of identifying timed automata and the power of clocks.  _Inf. Comput._ 209, 3 (2011), 606–625.  https://doi.org/10.1016/j.ic.2010.11.023
  * Verwer et al. (2012) Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. 2012\.  Efficiently identifying deterministic real-time automata from labeled data.  _Mach. Learn._ 86, 3 (2012), 295–333.  https://doi.org/10.1007/s10994-011-5265-4
  * Waga (2023) Masaki Waga. 2023\.  Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. In _CAV 2023_ _(LNCS, Vol. 13964)_. Springer, 3–26.  https://doi.org/10.1007/978-3-031-37706-8_1
  * Xu et al. (2022) Runqing Xu, Jie An, and Bohua Zhan. 2022.  Active Learning of One-Clock Timed Automata Using Constraint Solving. In _Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis, ATVA 2022_ _(LNCS, Vol. 13505)_. Springer, 249–265.  https://doi.org/10.1007/978-3-031-19992-9_16