# Active Learning of Mealy Machines with Timers

Véronique Bruyère, Bharat Garhewal, Guillermo A Pérez, Gaëtan Staquet, Frits W Vaandrager

► To cite this version:

Véronique Bruyère, Bharat Garhewal, Guillermo A Pérez, Gaëtan Staquet, Frits W Vaandrager. Active Learning of Mealy Machines with Timers. QEST+FORMATS 2025 - Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, Aug 2025, Aarhus, Denmark. pp.42-61, 10.1007/978-3-032-05792-1_3. hal-05376642

HAL Id: hal-05376642

https://hal.science/hal-05376642v1

Submitted on 21 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Active Learning of Mealy Machines with Timers*

Véronique Bruyère¹ Ⓙ, Bharat Garhewal² Ⓙ, Guillermo A. Pérez³ Ⓙ, Gaëtan Staquet⁴ Ⓙ, and Frits W. Vaandrager² Ⓙ

¹ University of Mons, Belgium
veronique.bruyere@umons.ac.be

² Radboud University, The Netherlands
{b.garhewal,f.vaandrager}@cs.ru.nl

³ University of Antwerp – Flanders Make, Belgium
guillermo.perez@quantwerpen.be

⁴ Centre Inria de l'Université de Rennes, France
gaetan.staquet@inria.fr

**Abstract.** We present the first algorithm for query learning Mealy machines with timers in a black-box context. Our algorithm is an extension of the $L^\#)$ algorithm of Vaandrager et al. to a timed setting. We rely on symbolic queries which empower us to reason on untimed executions while learning. Similarly to the algorithm for learning timed automata of Waga, these symbolic queries can be realized using finitely many concrete queries. Experiments with a prototype implementation show that our algorithm is able to efficiently learn realistic benchmarks.

**Keywords:** Timed systems, model learning, active automata learning

## 1 Introduction

To understand and verify complex systems, we need accurate models that are understandable for humans or can be analyzed fully automatically. Such models are typically not available for legacy software and for AI systems constructed from training data. Model learning is a technology that potentially may fill this gap. In this work, we consider a specific kind of model learning: *active automata learning*, which is a black-box technique for constructing state machine models of software and hardware from information obtained through testing (i.e., providing inputs and observing the resulting outputs). It has been successfully used in many applications, e.g., for spotting bugs in implementations of major network protocols [13–17, 28]. We refer to [24, 31] for surveys and further references.

Timing plays a crucial role in many applications. However, extending model learning algorithms to a setting that incorporates quantitative timing information turns out to be challenging. Twenty years ago, the first papers on this subject were published [20, 27], but we still do not have scalable algorithms for

<footnote>* Gaëtan Staquet was a research fellow of the F.R.S.-FNRS. The research of B. Garhewal, F. Vaandrager, and G.A. Pérez, was supported by NWO projects 612.001.852 “GIRLS” and OCENW.M.23.155 “EVI”, and FWO project G0AH524N “SynthEx”.</footnote>
a general class of timed models. Consequently, in applications of model learning technology, timing issues still need to be artificially suppressed.

Several authors have proposed active learning algorithms for the popular framework of timed automata (TAs) [2], which extends DFAs with clock variables. Some of these proposals, for instance [21–23] have never been implemented. In recent years, however, several algorithms have been proposed and implemented that successfully learned realistic benchmark models. A first line of work restricts to subclasses of TAs such as deterministic one-clock TAs [4, 35]. A second line of work explores synergies between active and passive learning algorithms. Aichernig et al. [1, 30], for instance, employ a passive learning algorithm based on genetic programming to generate hypothesis models, which are subsequently refined using equivalence queries. A major result was obtained recently by Waga [34], who presents an algorithm for active learning of (general) deterministic TAs and shows the effectiveness of the algorithm on various benchmarks. Waga’s algorithm is inspired by ideas of Maler & Pnueli [27]. Based on the notion of elementary languages of [27], Waga uses symbolic queries which are then performed using finitely many concrete queries. Notably, symbolic queries are also used for learning other families of automata, such as register automata [19].

A challenge for learning algorithms for TAs is the inference of the guards and resets that label transitions. Given those difficulties, Vaandrager et al. [32] propose to consider learning algorithms for models using timers instead of clocks, e.g., the class of models defined by Dill [11]. The value of a timer decreases when time advances, whereas the value of a clock increases. A timer can be set to integer values on transitions and may be stopped or times out (its value becomes 0) in later transitions. Each timeout triggers an observable output, allowing a learner to observe the occurrence of timeouts. In [32], the notion of Mealy machine with a single timer (MM1T) is introduced, such that the absence of guards and invariants simplifies learning. A learner still has to determine which transitions (re)start the timer, but this no longer creates a combinatorial blow-up. If a transition sets a timer, then slight changes in the timing of this transition will trigger the corresponding changes in the timing of the resulting timeout, allowing a learner to identify the exact cause of each timeout.

Even if many realistic systems can be modeled as MM1Ts (e.g., the benchmarks in [32] and the brick sorter and traffic controller examples in [10]), the restriction to a single timer is a serious limitation. Kogel et al. [26] propose Mealy machines with local timers (MMLTs), where multiple timers are subject to carefully chosen constraints to enable efficient learning. Although quite interesting, the constraints of MMLTs are too restrictive for many applications (e.g., the FDDI protocol [25, 34]). Also, any MMLT can be converted to an equivalent MM1T. In [8], we explore a general extension of MM1Ts with multiple timers (MMTs), and show that for MMTs that are race-avoiding, the cause of a timeout event can be efficiently determined by “wiggling” the timing of input events. Finally, MMTs form a subclass of TAs, and thus, existing model checking algorithms and tools for TAs (such as UPPAAL<fnref n="5" />) can be used.

<footnote n="5">⁵ https://uppaal.org/</footnote>
Our main contribution is a learning algorithm for the MMT model of [8], that is obtained by extending the $L^\#$ learning algorithm for Mealy machines of Vaandrager et al. [33] and by using the concept of symbolic queries as in [34]. Extending the $L^\#$ algorithm to multiple timers is not an easy task; it requires several new ideas. As this approach is different from Angluin's $L^*$ framework [5], used in other timed model learning algorithms, we cannot immediately apply existing ideas. Moreover, to the best of our knowledge, there is no notion of minimal MMT, in contrast to the minimal representations of timed languages proposed in [6] and the minimal model for timed automata with integer resets of [12]. Experiments with a prototype implementation, written in Rust, show that our algorithm is able to efficiently learn realistic benchmarks. The missing proofs and further details can be consulted in the arXiv version [7].

## 2 Mealy Machines with Timers

A Mealy machine is a variant of the classical finite automaton that associates an output with each transition. It can be seen as a relation between input words and output words. Mealy machines with timers [32] can be used to enforce timing constraints over the behavior of the relation, e.g., if we send a message and do not receive the acknowledgment after $d$ units of time, we resend the message.

We fix two non-empty finite sets $I$ of inputs and $O$ of outputs. A Mealy machine with timers uses a finite set $X$ of timers that can trigger transitions when they time out. Intuitively, changes in the state of the machine will be driven both by reading inputs and by “timeouts”. To formalize this, it is convenient to define the set $TO[X] = \{to[x] | x \in X\}$ of timeouts of $X$. We write $A(M)$ for the set $I \cup TO[X]$ of actions of $M$: reading an input or processing a timeout. The set $U(M) = (X \times \mathbb{N}^{>0}) \cup \{\perp\}$ contains the updates of $M$, where $(x, c)$ means that timer $x$ is started with value $c$, and $\perp$ stands for no timer update. We impose constraints on the shape of MMTs, e.g., a timer $x$ can time out only when it is active, to define the timed semantics in a straightforward manner.

**Definition 1 (Mealy machine with timers).** A Mealy machine with timers $(MMT, \text{for short})$ is a tuple $M = (X, Q, q_0, \chi, \delta)$ where:

- $X$ is a finite set of timers,

- $Q$ is a finite set of states, with $q_0 \in Q$ the initial state,

- $\chi: Q \to \mathcal{P}(X)$ assigns a set of active timers to each state, and

- $\delta: Q \times A(M) \to Q \times O \times U(M)$ is a partial transition function.

We write $q \xrightarrow{\frac{i}{o}} q'$ if $\delta(q, i) = (q', o, u)$. We require the following:

1. In the initial state, no timer is active, i.e., $\chi(q_0) = \emptyset$.

2. All active timers of the target state of a transition come from the source state, except at most one timer that may be started on the transition. That is, if $q \xrightarrow[\perp]{\frac{i}{o}} q'$, then $\chi(q') \subseteq \chi(q)$, and if $q \xrightarrow{\frac{i}{o}}_{(x,c)} q'$, then $\chi(q') \setminus \{x\} \subseteq \chi(q)$.
<figure><img src="image_2.png" /><figcaption>**Fig. 1.** An MMT with $\chi(q_0) = \emptyset$, $\chi(q_1) = \{x\}$, and $\chi(q) = \{x, y\}$ for all other $q$.</figcaption></figure>

3. If timer $x$ times out, then $x$ was active in the source state, i.e., if $q \xrightarrow{to[x]/o} q'$ then $x \in \chi(q)$. Moreover, if $u \neq \perp$, then $u$ must be $(x, c)$ for some $c \in \mathbb{N}^{>0}$.

When needed, we add a superscript to indicate which MMT is considered, e.g., $Q^M$, $q_0^M$, etc. Missing symbols in $q \xrightarrow{i/o} q'$ are quantified existentially. We say a transition $q \xrightarrow{u} q'$ starts (resp. restarts) a timer $x$ if $u = (x, c)$ and $x$ is inactive (resp. active) in $q$. We say that a transition<fnref n="6" /> $q \xrightarrow{i} q'$ with $i \neq to[x]$ stops timer $x$ if $x$ is inactive in $q'$. The requirement that a $to[x]$-transition can only restart timer $x$ is without loss of generality and a choice made to simplify the presentation (see [7, Appendix E.2]). An example of an MMT is given in Figure 1.

A run $\pi$ of $\mathcal{M}$ either consists of a single state $p_0$ or of a nonempty sequence of transitions $\pi = p_0 \xrightarrow{\frac{i_1}{o_1}} p_1 \xrightarrow{\frac{i_2}{o_2}} \dots \xrightarrow{\frac{i_n}{o_n}} p_n$. We denote by $\text{runs}(\mathcal{M})$ the set of runs of $\mathcal{M}$. We often write $q \xrightarrow{i} \in \text{runs}(\mathcal{M})$ to highlight that $\delta(q, i)$ is defined. We lift the notation to words $w = i_1 \cdots i_n$ as usual: $p_0 \xrightarrow{w} p_n \in \text{runs}(\mathcal{M})$ if there exists a run $p_0 \xrightarrow{i_1} \cdots \xrightarrow{i_n} p_n \in \text{runs}(\mathcal{M})$. Note that any run $\pi$ is uniquely determined by state $p_0$ and word $w$, as $\mathcal{M}$ is deterministic. A run $p_0 \xrightarrow{w} \in \text{runs}(\mathcal{M})$ is $x$-spanning (with $x \in X$) if it begins with a transition (re)starting $x$, ends with a $to[x]$-transition, and no intermediate transition restarts or stops $x$.

## 2.1 Timed Semantics

The semantics of an MMT $\mathcal{M}$ is defined via an infinite-state labeled transition system describing all possible configurations and transitions between them. A valuation is a partial function $\kappa: X \to \mathbb{R}^{\ge 0}$ that assigns nonnegative real numbers to timers. For $Y \subseteq X$, we write $\text{Val}(Y)$ for the set of all valuations $\kappa$ with $\text{dom}(\kappa) = Y$. A configuration of $\mathcal{M}$ is a pair $(q, \kappa)$ where $q \in Q$ and $\kappa \in \text{Val}(\chi(q))$. The initial configuration is the pair $(q_0, \kappa_0)$ where $\kappa_0 = \emptyset$ since $\chi(q_0) = \emptyset$. If $\kappa \in \text{Val}(Y)$ is a valuation in which all timers from $Y$ have a value of at least $d \in \mathbb{R}^{\ge 0}$, then $d$ units of time may elapse. We write $\kappa - d \in \text{Val}(Y)$ for the resulting valuation that satisfies $(\kappa - d)(x) = \kappa(x) - d$, for all $x \in Y$. If

<footnote n="6">⁶ Technically, it is the arrival at a state where the timer is marked as inactive that stops the timer. However, we find it convenient to reason about the transitions leading to such a state as being responsible for stopping the timer.</footnote>
the valuation $\kappa$ contains a value $\kappa(x) = 0$ for some timer $x$, then $x$ may time out. We define the transitions between configurations $(q, \kappa)$, $(q', \kappa')$ as follows:

**delay transition** $(q, \kappa) \xrightarrow{d} (q, \kappa - d)$, with $\kappa(x) \ge d$ for every $x \in \chi(q)$,

**discrete transition** $(q, \kappa) \xrightarrow{\frac{i}{o}} (q', \kappa')$, with $q \xrightarrow{\frac{i}{o}} q'$ a transition, $\kappa'(y) = \kappa(y)$ for all $y \in \chi(q')$ except that $\kappa'(x) = c$ if $u = (x, c)$. Moreover, if $i = \text{to}[x]$ then $\kappa(x) = 0$ and we call it a *timeout transition*; otherwise, we call it an *input transition*.

A timed run of $\mathcal{M}$ is a sequence of configuration transitions such that delay and discrete transitions alternate, beginning and ending with a delay transition. We say a configuration $(q, \kappa)$ is *reachable* if there is a timed run $\rho$ that starts with the initial configuration and ends with $(q, \kappa)$. The *untimed projection* of $\rho$, noted $\text{untime}(\rho)$, is the run obtained by omitting the valuations and delay transitions of $\rho$. A run $\pi$ is said *feasible* if there is a timed run $\rho$ such that $\text{untime}(\rho) = \pi$.

A timed word over a set $\Sigma$ is an alternating sequence of delays from $\mathbb{R}^{\ge 0}$ and symbols from $\Sigma$, such that it starts and ends with a delay. The length of a timed word $w$, noted $|w|$, is the number of symbols of $\Sigma$ in $w$. Note that, when $\Sigma = A(\mathcal{M})$, a timed run reading a timed word $w$ is uniquely determined by its first configuration and $w$. We thus write $(p, \kappa) \xrightarrow{w} \text{ for a timed run. A timed run } \rho$ is called *x-spanning* (with $x \in X$) if $\text{untime}(\rho)$ is *x-spanning*.

**Example 1.** Let $\mathcal{M}$ be the MMT of Figure 1. The timed run reading the timed word $0.5 \cdot i \cdot 1 \cdot i \cdot 1 \cdot \text{to}[x] \cdot 2 \cdot \text{to}[y] \cdot 0$ and its untimed projection are:

$$ (q_0, \emptyset) \xrightarrow{0.5} (q_0, \emptyset) \xrightarrow{\frac{i}{o}} (q_1, x=2) \xrightarrow{1} (q_1, x=1) \xrightarrow{\frac{i}{o'}} (q_2, x=1, y=3) \xrightarrow{1} (q_2, x=0, y=2) \\ \xrightarrow{\frac{to[x]}{o}} (q_3, x=y=2) \xrightarrow{2} (q_3, x=y=0) \xrightarrow{\perp} (q_0, \emptyset) \xrightarrow{0} (q_0, \emptyset), \\ \pi = q_0 \xrightarrow{\frac{i}{o}} q_1 \xrightarrow{\frac{i}{o'}} (y, 3) \xrightarrow{q_2} \xrightarrow{\frac{to[x]}{o}} (x, 2) \xrightarrow{q_3} \xrightarrow{\frac{to[y]}{o}} q_0. $$

Hence, $\pi$ is feasible, unlike the run $q_0 \xrightarrow{\frac{i \cdot i \cdot \text{to}[y]}{o}}$, as the value of $y$ in $q_2$ is always greater than the value of $x$, no matter the chosen delays. Observe that $q_1 \xrightarrow{\frac{i \cdot \text{to}[x] \cdot \text{to}[y]}{o}}$ is $y$-spanning, while $q_0 \xrightarrow{\frac{i \cdot i \cdot \text{to}[x]}{o}}$ is $x$-spanning.

As $(q_2, x = 0, y = 2)$ is reachable, we say that $x$ is *enabled* in $q_2$: it is possible to observe the timeout of $x$ in $q_2$ along some timed run. However, $y$ is not enabled in $q_2$, as it is impossible to reach a configuration $(q_2, x = \cdot, y = 0)$. △

Formally, we write $\chi_0(q)$ for the set of all enabled timers of $q$, i.e.,

$$ \chi_0(q) = \{x \in \chi(q) \mid \exists(q_0, \emptyset) \xrightarrow{w} (q, \kappa) : \kappa(x) = 0\}. $$

If $q$ has at least one enabled timer then, just by waiting in $q$ for long enough, we can force one timer to reach the value zero. A desirable property is for all such behaviors to have a corresponding timeout transition, which is the case for $\mathcal{M}$. We thus say that an MMT $\mathcal{N}$ is *complete* if for all $q \in Q$ and all $i \in I \cup TO[\chi_0(q)]$ we have $q \xrightarrow{i} \in runs(\mathcal{N})$.<fnref n="7" />

<footnote n="7">⁷ Notice that we only require the timeout transitions to be defined for enabled timers.</footnote>
## 2.2 Symbolic Semantics

Our learning algorithm is based on an untimed, symbolic semantics that abstracts from timing delays and timer names. The idea is that, rather than the name of a timer in a $to[x]$ event, we record a pointer to the preceding transition that (re)started this timer, together with the value to which the timer was set in this preceding transition. Consider, for instance, the run

$$ \pi = q_0 \xrightarrow{\frac{i}{(x,2)}} q_1 \xrightarrow{\frac{to[x]}{(x,2)}} q_1 \xrightarrow{\frac{to[x]}{u_1}} q_1 $$

of the MMT of Figure 1. Then the symbolic input word of $\pi$ is $w = i \cdot to[2, 1] \cdot to[2, 2]$, as the first action of $\pi$ is the input $i$, the second action is a timeout that is caused by setting the timer to 2 in the first transition, and the third action is a timeout that is caused by setting the timer to 2 in the second transition. More generally, consider a run

$$ \pi = p_0 \xrightarrow{\frac{i_1/o_1}{u_1}} p_1 \xrightarrow{\frac{i_2/o_2}{u_2}} \dots \xrightarrow{\frac{i_n/o_n}{u_n}} p_n $$

with $p_0 = q_0^M$. For $k \in \{1, \dots, n\}$, let $\pi_k$ be the prefix of run $\pi$ up to state $p_k$. Suppose that timer $x$ is active in the last state of $\pi_k$, for some $k > 0$. Then we define $cs(\pi_k, x)$ as the pair $(c, j)$, where $j$ is the index of the last transition (re)starting $x$, and $c$ is the value to which $x$ is set in this transition:

$$ cs(\pi_k, x) = \begin{cases} (c, k) & \text{if } u_k = (x, c), \\ cs(\pi_{k-1}, x) & \text{otherwise.} \end{cases} $$

Now we associate with $\pi$ a symbolic word (sw, in short) $sw(\pi) = i_1 \cdots i_n$ over alphabet $A = I \cup TO[\mathbb{N}^{>0} \times \mathbb{N}^{>0}]$ as follows. For every $k \in \{1, \dots, n\}$, if $i_k \in I$ then $i_k = i_k$, and if $i_k = to[x]$ then $i_k = to[cs(\pi_{k-1}, x)]$. Similarly, we associate an output word $ow(\pi)$ with $\pi$, consisting of the sequence of output actions $o_1 \cdots o_n$ occurring in run $\pi$. We write $L_{sym}(M)$ to denote the symbolic input language of $M$, defined as the set of symbolic input words associated with feasible runs of $M$ starting from $q_0^M$.

Notice that, since MMTs are deterministic, a feasible run $\pi$ can be denoted via the word $w = i_1 \cdots i_n$, and vice-versa. Thus, for every word $w$ labeling a feasible run $\pi$, we also associate a sw to $w$ as $\bar{w} = sw(\pi)$. Moreover, since each transition of an MMT (re)starts at most one timer, at most one run can be associated with any symbolic input word. For instance, the symbolic input word $w = i \cdot i \cdot to[2, 1] \cdot to[3, 2]$ induces the run $q_0 \xrightarrow{\frac{i}{(x,2)}} q_1 \xrightarrow{\frac{i}{(y,3)}} q_2 \xrightarrow{\frac{to[x]}{u_2}} q_3 \xrightarrow{\frac{to[y]}{u_3}} q_0$ in $M$. If $w \in L_{sym}(M)$, we write $out^M(w)$ for the output word $ow(\pi)$ of the unique run $\pi$ of $M$ with $sw(\pi) = w$.

We now define a notion of symbolic equivalence between two MMTs.

**Definition 2 (Symbolic equivalence).** Two complete MMTs $M$ and $N$ are symbolically equivalent, noted $M \approx_M N$, if $L_{sym}(M) = L_{sym}(N)$ and, for each $w \in L_{sym}(M)$, $out^M(w) = out^N(w)$.

As outputs and updates at the start of spanning runs are the same, symbolic equivalence implies timed equivalence (defined as a bisimulation, see [7, Appendix A]), i.e., the MMTs produce the same output words on all timed input words.
## 2.3 Learning framework

As usual for active learning algorithms, we rely on Angluin's framework [5]: A teacher knows an MMT $\mathcal{M}$, and a learner can query the teacher to obtain knowledge about $\mathcal{M}$. The set of MMTs $\mathcal{M}$ that we consider for our learning algorithm must be *s-learnable* (the $s$ stands for symbolically), i.e., $\mathcal{M}$ is complete and every run of $\mathcal{M}$ is feasible. The MMT of Figure 1 is *s-learnable*. From any complete MMT, one can construct an *s-learnable* MMT that is symbolically equivalent, by using *zones* (akin to the homonymous concept for timed automata, see [9]). The complete proof is given in [7, Appendix B].

**Lemma 1.** For any complete MMT $\mathcal{M}$, there is an *s-learnable* MMT $\mathcal{N} \stackrel{\text{sym}}{\approx} \mathcal{M}$.

We now define the *queries* the learner uses to gather knowledge about $\mathcal{M}$, the MMT of the teacher. For classical Mealy machines [29, 33], there are two queries: *output queries* providing the sequence of outputs for a given input word, and *equivalence queries* asking whether a hypothesis $\mathcal{H}$ is correct. If it is not, a counterexample is returned, i.e., a word $w$ inducing different outputs in $\mathcal{H}$ and in $\mathcal{M}$. In this work, we need to adapt those queries to encode the timed behavior induced by the timers of $\mathcal{M}$. As two MMTs do not use the same timers in general, we rely on *sws*, and adapt our queries accordingly. In order to deal with timed behavior, we also need a new type of query, called a *wait query*. Kogel et al. introduced a similar type of query, called *timer query*, in [26].

**Definition 3 (Symbolic queries).** The learner uses three symbolic queries, parametrized by either a symbolic input word $\mathbf{w}$ or a complete MMT $\mathcal{H}$:

*   **OQ<sup>s</sup>(w)** If $\mathbf{w} \in L_{\text{sym}}(\mathcal{M})$, then this query returns $\text{out}^{\mathcal{M}}(\mathbf{w})$.

*   **WQ<sup>s</sup>(w)** If $\mathbf{w} \in L_{\text{sym}}(\mathcal{M})$, then this query returns the set of all pairs $(c, j)$ with $\mathbf{w}$ to $[c, j] \in L_{\text{sym}}(\mathcal{M})$.

*   **EQ<sup>s</sup>(H)** This query returns *yes* if $\mathcal{H} \stackrel{\text{sym}}{\approx} \mathcal{M}$, and otherwise a symbolic input word $\mathbf{w}$ witnessing the non-equivalence: either $\mathbf{w} \in L_{\text{sym}}(\mathcal{H}) \setminus L_{\text{sym}}(\mathcal{M})$, or $\mathbf{w} \in L_{\text{sym}}(\mathcal{M}) \setminus L_{\text{sym}}(\mathcal{H})$, or $\mathbf{w} \in L_{\text{sym}}(\mathcal{H}) \cap L_{\text{sym}}(\mathcal{M})$ and $\text{out}^{\mathcal{H}}(\mathbf{w}) \neq \text{out}^{\mathcal{M}}(\mathbf{w})$.

*   **OQ<sup>s</sup>** and **EQ<sup>s</sup>** are analogous to regular output and equivalence queries for Mealy machines, while **WQ<sup>s</sup>** provides, for each timer $x$ enabled at the end of the run induced by the symbolic word, the transition which last (re)started $x$ and the constant $c$ with which $x$ was (re)started. (See Example 2 below.)

Similarly to the TA learning algorithm of Waga [34], these symbolic queries can be performed via concrete output and equivalence queries. This is possible under the assumption that $\mathcal{M}$ is *race-avoiding* [8], i.e., $\mathcal{M}$ allows runs to be observed deterministically, in the sense that any feasible run $\pi$ is the untimed projection of a run $\rho$ where all delays are non-zero and there are no two timers that time out at the same time along $\rho$.<fnref n="8" /> Not all MMTs are race-avoiding and

<footnote n="8">⁸ We highlight that we do not require this to hold for any timed run $\rho$. Importantly, if $\mathcal{M}$ is race-avoiding, then we can always change the delays in the runs to avoid having concurrent timeouts.</footnote>
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** On the left, a tree $\mathcal{T}$ from which the hypothesis MMT on the right is constructed. Basis states of $\mathcal{T}$ have a gray background.</figcaption></figure>

a decidable characterization of those MMTs that are given in [8]. MMTs with one timer [32] and Mealy machines with local timers [26] (translated as MMTs) are all race-avoiding, this is also the case for all benchmarks in Section 4.

**Lemma 2.** For race-avoiding MMTs, the three symbolic queries can be realized via a polynomial number of concrete output and equivalence queries.

For intuition, for all symbolic queries, we can construct a system of linear temporal constraints whose solutions can be mapped to concrete input words. Technically, the system also depends on the tree we use to structure the result of queries we have made. See [7, Appendix C] for details.

## 3 Learning algorithm

We now present our learning algorithm for MMTs, called $L_{MMT}^{\#}$. Given the hidden s-learnable MMT $\mathcal{M}$ we want to learn, this algorithm gradually builds a tree-shaped MMT $\mathcal{T}$ that stores the observations obtained by membership and wait queries. It then constructs a hypothesis MMT $\mathcal{H}$ obtained from $\mathcal{T}$ whose certain states (the basis) are the states of $\mathcal{H}$ and certain transitions are redirected to the basis. An example of MMTs $\mathcal{T}$ and $\mathcal{H}$ is given in Figure 2 for the MMT $\mathcal{M}$ of Figure 1, such that the equivalence query fails. The main difficulties of the learning process are: (i) $\mathcal{T}$ uses its own timers without knowing those of $\mathcal{M}$ and for which it is necessary to discover when two distinct timers of $\mathcal{T}$ represent the same timer of $\mathcal{M}$ (see the concept of timer matching and functional simulation below); (ii) the basis of $\mathcal{T}$ used to define the states of $\mathcal{H}$ must be formed of states that correspond to distinct states of $\mathcal{M}$ despite partial knowledge of its timers (see the concept of apartness and Theorem 2 below). Before moving on to the details of the $L_{MMT}^{\#}$ algorithm, let us state its complexity. Observe that the same bounds hold with concrete queries, by Lemma 2, and that the complexity becomes polynomial when $|X^{\mathcal{M}}|$ is fixed.

**Theorem 1.** The $L_{MMT}^{\#}$ algorithm terminates and returns an MMT $\mathcal{N} \stackrel{\text{sym}}{\approx} \mathcal{M}$ s.t. $\mathcal{N}$ has a size polynomial in $|Q^{\mathcal{M}}|$ and factorial in $|X^{\mathcal{M}}|$. Its running time and number of symbolic queries of $L_{MMT}^{\#}$ are polynomial in $|Q^{\mathcal{M}}|, |I|$ and the length of the longest counterexample returned by the teacher, factorial in $|X^{\mathcal{M}}|$.
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Sample observation tree (we write $x_i$ instead of $x_{t_i}$ for all states $t_i$) with $\chi(t_1) = \chi(t_2) = \{x_1\}$, $\chi(t_3) = \chi(t_5) = \{x_1, x_3\}$, $\chi(t_6) = \{x_3, x_6\}$, and $\chi(t) = \emptyset$ for the other states $t$.</figcaption></figure>

## 3.1 Observation tree

We describe the main data structure of $L_{\text{MMT}}^{\#}$: a modification of the *observation tree* used for $L^\#$ [33]. We impose that this tree $\mathcal{T}$ is a tree-shaped MMT whose every run is feasible. Each state $q$ of $\mathcal{T}$ has its own timer $x_q$ that can only be started by the incoming transition of $q$, and may be restarted only by a $\text{to}[x_q]$-transition. Due to the tree-shape nature of $\mathcal{T}$, we can impose strict constraints on the sets of active and enabled timers of its states, as described in the next definition. We only provide the main ideas, see [7, Appendix D] for details.

**Definition 4 (Observation tree).** An MMT $\mathcal{M}$ is tree shaped if for every state $q \in Q^\mathcal{M}$ there is a unique run, denoted $\text{run}^\mathcal{M}(q)$, that starts in $q_0^\mathcal{M}$ and ends in $q$. An observation tree is a tree-shaped MMT $\mathcal{T} = (X, Q, q_0, \chi, \delta)$ such that $X = \{x_q \mid q \in Q \setminus \{q_0\}\}$, every run of $\mathcal{T}$ is feasible,

- for all $p \xrightarrow{(x,c)}^i q$ with $i \in I$, we have $x = x_q$,

- for all $q \in Q, x \in X$, we have $x \in \chi(q)$ if and only if there is an x-spanning run traversing $q$, and

- for all $q \in Q, x \in X$, we have $x \in \chi_0(q)$ if and only if $q \xrightarrow{\text{to}[x]} \in \text{runs}(\mathcal{T})$.

We explain how to use $\mathbf{OQ}^s$ and $\mathbf{WQ}^s$ to gradually grow $\mathcal{T}$ on an example.

*Example 2.* Let $\mathcal{M}$ be the MMT of Figure 1 and $\mathcal{T}$ be the observation tree of Figure 3, except that $t_3 \xrightarrow{i} \notin \text{runs}(\mathcal{T})$, i.e., the subtree rooted at $t_6$ is not present in the tree. We construct that subtree, via $\mathbf{OQ}^s$ and $\mathbf{WQ}^s$.

First, we create the $t_3 \xrightarrow{i} \text{transition}$. Let $w = i \cdot i$ be the unique word such that $t_0 \xrightarrow{w} t_3$ and $\mathbf{w} = \bar{w} = i \cdot i$ be the corresponding sw. As $\mathcal{M}$ is s-learnable (and, thus, complete), it follows that $q_0^\mathcal{M} \xrightarrow{\mathbf{w} \cdot i} \in \text{runs}(\mathcal{M})$, i.e., $\mathbf{w} \cdot i \in L_{\text{sym}}(\mathcal{M})$. So, we can call $\mathbf{OQ}^s(\mathbf{w} \cdot i)$, which returns $o \cdot o' \cdot o'$. Hence, we create the transition $t_3 \xrightarrow{i \parallel o'} t_6$ in $\mathcal{T}$. We initially use a $\perp$ update (seen as a sort of wildcard) as we do not yet have any information about the potential update of the corresponding transition (here, $q_2 \xrightarrow{(x,2)} q_3$) in $\mathcal{M}$. Later on, we may discover that the transition must start a timer, in which case $\perp$ will be replaced by an actual update.

We then perform a symbolic wait query in $t_6$, i.e., call $\mathbf{WQ}^s(\mathbf{w} \cdot i)$, which returns the set $\{(2,3), (3,2)\}$ meaning that the second (resp. third) transition
of the run $q_0^T \xrightarrow{w,i} \emptyset$ must (re)start a timer with constant 3 (resp. constant 2). So, the $\perp$ of the newly created transition is replaced by $(x_6, 2)$ (as the label of the transition is an input). It remains to create the $to[x_3]$- and $to[x_6]$-transitions from $t_6$ by performing two symbolic output queries. We call $OQ^s(w \cdot i \cdot to[2])$ and $OQ^s(w \cdot i \cdot to[3])$ and create the transitions. We obtain the tree of Figure 3. ▼

**Functional simulation.** Each state of an observation tree can be mapped to a state of the hidden $\mathcal{M}$, by adapting the notion of functional simulation of $L^\#$ [33]. We have a function $f: Q^T \to Q^\mathcal{M}$ that preserves the initial state and the behavior of transitions. In addition, since $\mathcal{T}$ and $\mathcal{M}$ may use different timers, we have a function $g: X^T \to X^\mathcal{M}$ that maps timers of $\mathcal{T}$ to timers of $\mathcal{M}$. We lift $g$ to actions such that $g(i) = i$ for every $i \in I$ and $g(to[x]) = to[g(x)]$ for every $x \in \text{dom}(g)$. We require, for all $q, q' \in Q^T$, $x, y \in X^T$, $i \in I$ and $o \in O$:

1. $f$ preserves the initial state, i.e., $f(q_0^T) = q_0^{\mathcal{M}}$;

2. any timer that is active in $q$ has a corresponding active timer in $f(q)$, i.e., if $x \in \chi^T(q)$, then $g(x) \in \chi^\mathcal{M}(f(q))$;

3. two distinct timers that are active in $q$ are mapped to two distinct timers in $\mathcal{M}$, i.e., if $x \neq y$ and both are active in $q$, then $g(x) \neq g(y)$;

4. for each $q \xrightarrow{i/o} q'$ in $\mathcal{T}$, there is a corresponding transition $f(q) \xrightarrow{g(i)/o} f(q')$ in $\mathcal{M}$;

5. using rule (4) we may construct, for each run $\pi$ of $\mathcal{T}$, a corresponding run $(f,g)(\pi)$ of $\mathcal{M}$. We require that the causality of timeouts is preserved, i.e., for each $q \xrightarrow{to[x]/o} q'$ in $\mathcal{T}$ with $q$ the last state of $\pi$, $cs(\pi, x) = cs((f,g)(\pi), g(x))$.

One can show the following properties from the above constraints.

**Lemma 3.** Let $\mathcal{M}$ be an s-learnable MMT, $\mathcal{T}$ be an observation tree, and $f$ and $g$ be the functions described above. Then, for any state $q \in Q^T$, we have $|\chi^T(q)| \le |\chi^\mathcal{M}(f(q))|$ and for all $x \in \chi_0^T(q)$, it holds that $g(x) \in \chi_0^\mathcal{M}(f(q))$.

We say that a state $q$ of $\mathcal{T}$ is *explored once* $\mathbf{WQ}^s(q)$ has been called. By definition of wait queries, it means that every enabled timer of $f(q)$ is identified in $q$, i.e., $|\chi_0(q)| = |\chi_0(f(q))|$. We thus obtain a *one-to-one correspondence* between $\chi_0^T(q)$ and $\chi_0^\mathcal{M}(f(q))$. Define $\mathcal{E}^T$ as the maximal set of explored states of $\mathcal{T}$. During the learning process, we will ensure that a wait query is performed only on states that are successors of an explored state to keep $\mathcal{E}^T$ as a subtree of $\mathcal{T}$.

*Example 3.* In the tree of Figure 3, the explored states are $t_0, t_1, t_2, t_3, t_5$, and $t_6$. In Example 2, $t_0$ to $t_3$, and $t_5$ were already explored and formed a subtree. The wait query over $t_6$ made it an explored state, i.e., $\mathcal{E}^T$ is still a subtree. ▼

**Apartness.** A key aspect of $L^\#$ for regular Mealy machines is the notion of *apartness* indicating which states of an observation tree have different behaviors [33]: states $p, p'$ are *apart* if they have different output responses to the same input word. Here, we face a more complex situation as we need to handle
the fact that different timers in $\mathcal{T}$ can represent the same timer in $\mathcal{M}$. Before defining apartness in the MMT setting, we need to introduce two concepts.

For two states $p, p'$ of $\mathcal{T}$, we define a matching $m: \chi^T(p) \to \chi^T(p')$ as an injective partial function. This matching is meant to indicate that the timers $x$ and $m(x)$ could represent the same timer in $\mathcal{M}$. By abuse of notation, it is denoted as $m: p \leftrightarrow p'$. A matching is maximal if $m$ is total or surjective, i.e., $m$ embeds $\chi^T(p)$ in $\chi^T(p')$ or $m^{-1}$ embeds $\chi^T(p')$ in $\chi^T(p)$. Recall that if two distinct timers $x$ and $y$ are both active in the same state of $\mathcal{T}$, it must hold that $g(x) \neq g(y)$, i.e., they correspond to different timers in $\mathcal{M}$ (by functional simulation). Hence, we say that a matching $m$ is valid if for all $x \in \text{dom}(m)$ and $q \in \mathcal{Q}^T$, we do not have $x, m(x) \in \chi^T(q)$.

Second, given a run $\pi = p_0 \xrightarrow{i_1} p_1 \xrightarrow{i_2} \dots \xrightarrow{i_n} p_n$ and a matching $m: p_0 \leftrightarrow p'_0$, we want to check whether it is possible to “read” the same word $i_1 \dots i_n$ from $p'_0$ while extending $m$ during this reading. If this is possible, this unique run, denoted $\text{read}_\pi^m(p'_0)$, is equal to $\pi' = p'_0 \xrightarrow{i'_1} p'_1 \xrightarrow{i'_2} \dots \xrightarrow{i'_n} p'_n$ such that:

(i) If $i_j \in I$, then $i'_j = i_j$.

(ii) If $i_j = \text{to}[x]$ for some $x \in X^T$, recall that $x \in \chi^T(p_0)$ or $x = x_{p_k}$ for some $k$. Then, $i'_j$ is either $\text{to}[m(x)]$, or $\text{to}[x_{p'_k}]$ with the same $k$.

When $\text{read}_\pi^m(p'_0)$ exists, we therefore have a matching between $\pi$ and $\pi'$, denoted $m_{\pi'}^\pi: \pi \leftrightarrow \pi'$, which extends $m$ such that $m_{\pi'}^\pi = m \cup \{x_{p_k} \mapsto x_{p'_k} \mid k \le n\}$.

While two states of a Mealy machine are apart when they have different output responses to the same input word, we have five different apartness cases in the MMT setting. An illustrative example is given after the definition.

**Definition 5 (Apartness).** For two states $p_0, p'_0$ and a matching $m: p_0 \leftrightarrow p'_0$, we say that $p_0, p'_0$ are $m$-apart, denoted by $p_0 \#^m p'_0$, if there are $\pi = p_0 \xrightarrow{i_1} \dots \xrightarrow{i_n/o} p_n$ and $\text{read}_\pi^m(p'_0) = \pi' = p'_0 \xrightarrow{i'_1} \dots \xrightarrow{i'_n/o'} p'_n$ with $m_{\pi'}^\pi: \pi \leftrightarrow \pi'$, and

**Structural apartness** either $m_{\pi'}^\pi$ is invalid, or

**Behavioral apartness** one of the following cases holds:

$o \neq o'$ (outputs)

$u = (x, c) \wedge u' = (x', c') \wedge c \neq c'$ (constants)

$p_n, p'_n \in \mathcal{E}^T \wedge |\chi_0^T(p_n)| \neq |\chi_0^T(p'_n)|$ (sizes)

$p_n, p'_n \in \mathcal{E}^T \wedge \exists x \in \text{dom}(m_{\pi'}) : (x \in \chi_0^T(p_n) \Leftrightarrow m_{\pi'}^\pi(x) \notin \chi_0^T(p'_n))$ (enabled)

The word $w = i_1 \dots i_n$ is called a witness of $p_0 \#^m p'_0$, denoted $w \vdash p_0 \#^m p'_0$.

**Example 4.** Let $\mathcal{T}$ be the tree of Figure 3 and $\pi = t_0 \xrightarrow{i/o} (x_{1,2}) \xrightarrow{t_1} \xrightarrow{to[x_1]/o} t_2 \in \text{runs}(\mathcal{T})$. Let us show that $\text{read}_\pi^\emptyset(t_3)$ exists ($\emptyset$ is the empty matching). As the first action in $\pi$ is $i$, we take the transition $t_3 \xrightarrow{i/o'} (x_{6,2}) \xrightarrow{t_6}$ to the second action in $\pi$ is $\text{to}[x_1]$ with $x_1$ a fresh timer, we retrieve the corresponding fresh timer $x_6$ in the new run. Hence, $\pi' = \text{read}_\pi^\emptyset(t_3) = t_3 \xrightarrow{i/o'} (x_{6,2}) \xrightarrow{to[x_6]/o} t_9$ and $m_{\pi'}^\pi: \pi \leftrightarrow \pi'$
with $m_{\pi'}^{\pi} = \emptyset \cup \{x_1 \mapsto x_6\}$. Let us now show some cases of apartness. The states $t_0, t_3$ are $\emptyset$-apart as the first transition of $\pi$ outputs $o$ but the first transition of $\pi'$ outputs $o' \neq o$, i.e., $i \vdash t_0 \#^{\emptyset} t_3$ by (outputs). The states $t_1, t_6$ are also $\emptyset$-apart as $t_1, t_6 \in \mathcal{E}^T$ and $|\chi_0(t_1)| = 1 \neq |\chi_0(t_6)| = 2$, i.e., $\varepsilon \vdash t_1 \#^{\emptyset} t_6$ by (sizes). Now, with $m: x_1 \mapsto x_3$, let $\sigma = t_1 \xrightarrow{(i/o)(x_{3,3})} t_3 \xrightarrow{to[x_1]} t_5$ and $\sigma' = read_{\pi'}^m(t_3) = t_3 \xrightarrow{(i/o')(x_{6,2})} t_6 \xrightarrow{to[x_3]} t_{10}$. We have a structural apartness as $m_{\rho'}^{\rho} = m \cup \{x_3 \mapsto x_6\}$ is invalid $(\chi^T(t_6) = \{x_3, x_6\})$. We also have $i \vdash t_1 \#^m t_3$ by (constants). ▼

Observe that any extension $m'$ of $m$ is such that $w \vdash p \#^{m'} p'$, i.e., taking a larger matching does not break the apartness, as $read_p^{m_w}(p') = read_p^{m_w'}(p') = p' \xrightarrow{w'}$. Moreover, we claim that the definition of apartness is reasonable: when $p \#^m p'$, then $f(p) \neq f(p')$ (the two states are really distinct) or $g(x) \neq g(m(x))$ for some $x$ ($m$ and $g$ do not agree).

**Theorem 2.** Let $\mathcal{T}$ be an observation tree for an s-learnable MMT with functional simulation $(f,g)$, $p,p' \in Q^T$, and $m,m': p \leftrightarrow p'$ matchings. Then,

$$- w \vdash p \#^m p' \wedge m \subseteq m' \Rightarrow w \vdash p \#^{m'} p', \text{ and}$$

$$- p \#^m p' \Rightarrow f(p) \neq f(p') \lor \exists x \in \mathit{dom}(m) : g(x) \neq g(m(x)).$$

The second implication of Theorem 2 is the one we leverage in our algorithm below. The reverse implication is false as the learned MMT can be smaller than that of the teacher (see the MMT in Figure 4 learned from the MMT of Figure 1).

## 3.2 Hypothesis construction

In this section, we provide the construction of a hypothesis $\mathcal{H}$ from $\mathcal{T}$. In short, we extend the observation tree such that some conditions are satisfied and we define a subset of $Q^T$, called the *basis*, that forms the set of states of $\mathcal{H}$. Similar to $L^\#$ [33], we then “fold” the tree; that is, some transitions $q \to r$ must be redirected to some state $p$ of the basis. For MMTs, we also need to map every timer active in $r$ to an active timer of $p$. Formally, we define:

- The *basis* $\mathcal{B}^T$ is a subtree of $Q^T$ such that $q_0^T \in \mathcal{B}^T$ and $p \#^m p'$ for any $p \neq p' \in \mathcal{B}^T$ and maximal matching $m: p \leftrightarrow p'$. By Theorem 2, we thus know that $f(p) \neq f(p')$ or $g(x) \neq g(m(x))$ for some $x \in \mathit{dom}(m)$. As we have this for every maximal $m$, we *conjecture* that $f(p) \neq f(p')$. We may be wrong, i.e., $f(p) = f(p')$ but we need a matching that is currently unavailable, due to unknown active timers which will be discovered later.

- The *frontier* $\mathcal{F}^T \subseteq Q^T$ is the set of immediate non-basis successors of basis states. We say $p \in \mathcal{B}^T$ and $r \in \mathcal{F}^T$ are *compatible* under a maximal matching $m$ if $\neg(p \#^m r)$. We write $\mathit{compat}^T(r)$ for the set of all such pairs $(p,m)$. Hence $\mathit{compat}^T(r)$ indicates all the possible ways to redirect a transition $q \to r$ to some state $p \in \mathcal{B}^T$ together with an adequate maximal matching $m$.

During the learning algorithm, the tree is extended such that a complete MMT $\mathcal{H}$ can be constructed from $\mathcal{T}$. We will ensure that:
(A) each basis and frontier state is explored, i.e. $\mathcal{B}^T \cup \mathcal{F}^T \subseteq \mathcal{E}^T$, in order to discover timers as fast as possible,

(B) the basis is complete, i.e., $p \stackrel{i}{\to}$ is defined for every $i \in I \cup TO[\chi_0^T(p)]$, and

(C) for every $r \in \mathcal{F}^T$, $\mathit{compat}^T(r) \neq \emptyset$ and $|\chi^T(p)| = |\chi^T(r)|$ for every $(p, m) \in \mathit{compat}^T(r)$. The last constraint imposes the same number of active timers for both $p$ and $r$ since folding them using $(p, m)$ will merge them.

These constraints are obtained via $\mathbf{OQ}^s$ and $\mathbf{WQ}^s$, as we now illustrate.

**Example 5.** In order to simplify the explanations, we assume from now on that a call to $\mathbf{OQ}^s(\mathbf{w} \cdot i)$ with $i \in I$ automatically adds the corresponding transition to $\mathcal{T}$, and that a call to $\mathbf{WQ}^s(\mathbf{w})$ automatically calls $\mathbf{OQ}^s(\mathbf{w} \cdot \mathit{to}[j])$, for every $\mathit{to}[j]$ deduced from the wait query, modifies updates accordingly, and adds the new explored states to $\mathcal{E}^T$. Moreover, we let $\mathbf{OQ}^s(q, i)$ denote $\mathbf{OQ}^s(\mathbf{w} \cdot i)$ and $\mathbf{WQ}^s(q)$ denote $\mathbf{WQ}^s(\mathbf{w})$ with $\mathbf{w}$ such that $q_0^T \stackrel{\mathbf{w}}{\to} q \in \mathit{runs}(\mathcal{T})$.

Let $\mathcal{T}$ be the observation tree of Figure 3 for the MMT $\mathcal{M}$ of Figure 1. One can check that $t_0, t_1$, and $t_3$ are all pairwise apart under any maximal matching. So, $\mathcal{B}^T = \{t_0, t_1, t_3\}$ (highlighted in gray in the figure) and $\mathcal{F}^T = \{t_2, t_5, t_6\}$. Moreover, we have $\mathit{compat}^T(t_2) = \{(t_1, x_1 \mapsto x_1), (t_3, x_1 \mapsto x_1)\}$, and $\mathit{compat}^T(t_5) = \mathit{compat}^T(t_6) = \emptyset$. We thus promote $t_6$ by moving it from the frontier to the basis, i.e., $\mathcal{B}^T = \{t_0, t_1, t_3, t_6\}$. To satisfy (B), we call $\mathbf{OQ}^s(t_6, i)$ and add a new transition $t_6 \xrightarrow{i/o} \bot \to t_{11}$. We call $\mathbf{WQ}^s(t_9)$, $\mathbf{WQ}^s(t_{10})$, and $\mathbf{WQ}^s(t_{11})$, which yield $\chi(t_9) = \chi_0(t_9) = \{x_3\}$, $\chi(t_{10}) = \emptyset$, and $\chi(t_{11}) = \chi_0(t_{11}) = \{x_3, x_{11}\}$. Hence, we get (A) with $\mathcal{F}^T = \{t_2, t_5, t_9, t_{10}, t_{11}\}$.

Observe that (C) is not satisfied, due to $(t_3, m) \in \mathit{compat}^T(t_2)$ with $m: x_1 \mapsto x_1$ but $|\chi(t_3)| = 2$ while $|\chi(t_2)| = 1$. To resolve this issue, we replay<fnref n="9" /> the run $\pi = t_3 \xrightarrow{\mathit{to}[x_1]\mathit{to}[x_3]} t_8$ (witnessing that $x_3$ is active in $t_3$ and eventually times out) from the state $t_2$. That is, we extend the tree $\mathcal{T}$ in order to create $\mathit{read}_\pi^m(t_2)$ while extending $m$, if this is possible (see apartness paragraph). As $t_2 \xrightarrow{\mathit{to}[x_1]} t_4$ already exists, let us replay $t_5 \xrightarrow{\mathit{to}[x_3]}$ from $t_4$. We call $\mathbf{WQ}^s(t_4)$ to learn $\chi_0(t_4) = \chi(t_4) = \{x_1\}$. We can stop the creation of $\mathit{read}_\pi^m(t_2)$. Indeed, as $\chi_0(t_5) = \{x_1, x_3\}$, $\chi_0(t_4) = \{x_1\}$, we conclude that $\mathit{to}[x_1] \vdash t_3 \#^m t_2$ by (sizes). Hence, $(t_3, m)$ is no longer a compatible pair and it is removed from $\mathit{compat}^T(t_2)$.

In general, replaying a run when (C) is not satisfied may have two results due to newly defined transitions: either finding a new active timer in a state, or a new apartness pair (as we illustrated). In any case, the set of compatible pairs of a state gets reduced. ▼

We now explain, via an example, how to construct a hypothesis $\mathcal{H}$ such that $Q^\mathcal{H} = \mathcal{B}^T$. The idea is to pick a $(p, m) \in \mathit{compat}^T(r)$ for each frontier state $r$. Then, the unique transition $q \stackrel{i}{\to} r$ in $\mathcal{T}$ becomes $q \stackrel{i}{\to} p$ in $\mathcal{H}$, i.e., $p$ and $r$ are merged. We also globally rename the timers according to $m$.

<footnote n="9">⁹ See [7, Appendix E.1] for details.</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 4. On top, an observation tree from which the hypothesis MMT at the bottom is constructed, with $y_1 = [[x_1]]_\equiv$ and $y_2 = [[x_3]]_\equiv$. Basis states are highlighted with a gray background.</figcaption></figure>

Example 6. Let $\mathcal{M}$ be the MMT of Figure 1 and $\mathcal{T}$ be the observation tree of Figure 4, with $\mathcal{B}^{\mathcal{T}} = \{t_0, t_1, t_3, t_6, t_9\}$ and $\mathcal{F}^{\mathcal{T}} = \{t_2, t_5, t_{10}, t_{11}, t_{12}, t_{15}\}$. Constraints (A) to (C) are satisfied and

$$ 
\begin{align*}
\mathit{compat}^{\mathcal{T}}(t_2) &= \{(t_1, x_1 \mapsto x_1)\} \\
\mathit{compat}^{\mathcal{T}}(t_5) &= \{(t_6, x_6 \mapsto x_1, x_3 \mapsto x_3)\} \\
\mathit{compat}^{\mathcal{T}}(t_{10}) &= \mathit{compat}^{\mathcal{T}}(t_{12}) = \{(t_0, \emptyset)\} \\
\mathit{compat}^{\mathcal{T}}(t_{11}) &= \{(t_6, x_6 \mapsto x_{11}, x_3 \mapsto x_3)\} \\
\mathit{compat}^{\mathcal{T}}(t_{15}) &= \{(t_9, x_3 \mapsto x_3)\}
\end{align*}
$$

We construct $\mathcal{H}$ with $Q^\mathcal{H} = \mathcal{B}^\mathcal{T}$. While defining the transitions $q \to q'$ is easy when $q, q' \in \mathcal{B}^\mathcal{T}$, we have to redirect the transition to some basis state when $q' \in \mathcal{F}^\mathcal{T}$. To do so, we first define a map $\mathbf{h} : \mathcal{F}^\mathcal{T} \to \mathcal{B}^\mathcal{T}$ (to redirect transitions into the basis), and an equivalence relation $\equiv$ over the set of active timers of the basis and the frontier (to declare which timers are equal). For each $r \in \mathcal{F}^\mathcal{T}$, we pick $(p, m) \in \mathit{compat}^{\mathcal{T}}(r)$, define $\mathbf{h}(r) = p$, and add $x \equiv m(x)$ for every $x \in \mathit{dom}(m)$ (and compute the symmetric and transitive closure of $\equiv$). Here,

$$ 
\begin{align*}
\mathbf{h}(t_2) &= t_1, \mathbf{h}(t_5) = \mathbf{h}(t_{11}) = t_6, \mathbf{h}(t_{10}) = \mathbf{h}(t_{12}) = t_0, \mathbf{h}(t_{15}) = t_9, \\
x_1 \equiv x_6 \equiv x_{11}, \text{ and } x_3 \equiv x_3.
\end{align*}
$$

We check that the constructed relation $\equiv$ is valid, i.e., it does not lead to an undesirable situation $x \equiv y$ and $x, y \in \chi^{\mathcal{T}}(q)$ for some $q$ (in which case, we restart again by picking some different pair $(p, m) \in \mathit{compat}^{\mathcal{T}}(r)$). In this example, $\equiv$ is valid, and we construct $\mathcal{H}$ by copying the transitions starting from a basis state (while folding the tree when required), except that a timer $x$ is replaced by
its equivalence class $[[x]] =$. Figure 4 gives the resulting $\mathcal{H}$, which is symbolically
equivalent to $\mathcal{M}$.

We highlight that it is *not* always possible to construct a valid $\equiv$. However,
in this case, we can still construct a *generalized* MMT, in which the transitions
can arbitrarily rename the active timers. The size of that machine is also $|\mathcal{B}^T|$,  
and from it a classical MMT can be constructed of size $n! \cdot |\mathcal{B}^T|$, with $n =$
$\max_{p \in \mathcal{B}^T} |\chi^T(p)|$. See [7, Appendix E.2] for more information. We observed that
a valid $\equiv$ can always be constructed for all our benchmarks.

**3.3 Main loop**

We finally give the main loop of $L_{\text{MMT}}^{\#}$. We initialize $\mathcal{T}$ to only contain $q_0^T$, $\mathcal{B}^T = \mathcal{E}^T = \{q_0^T\}$, and $\mathcal{F}^T = \emptyset$. The main loop is split into two parts:

**Refinement loop** The *refinement loop* extends the tree to obtain the conditions (A) to (C) (see section 3.2 page 13), by performing the following operations, in this order, until no more changes are possible:

**Seismic** If we discover a new active timer in a basis state, then it may be
that $\neg(q \#^m q')$ for some $q, q' \in \mathcal{B}^T$ and maximal $m$, due to the new
timer. To avoid this, we reset the basis back to $\{q_0^T\}$, as soon as a new
timer is found, without removing states from $\mathcal{T}$.

**Promotion** If $\mathit{compat}^T(r)$ is empty for some frontier state $r$, then we know
that $q \#^m r$ for every $q \in \mathcal{B}^T$ and maximal matching $m: q \leftrightarrow r$. Hence,
we promote $r$ to the basis.

**Completion** If an *i*-transition is missing from some basis state *p*, we complete the basis with that transition.

**Active timers** We ensure $|\chi^T(p)| = |\chi^T(r)|$ for every $(p, \cdot) \in \mathit{compat}^T(r)$.

**Hypothesis and equivalence** We call $\mathbf{EQ}^s(\mathcal{H})$ with $\mathcal{H}$ a hypothesis. If the answer is **yes**, we return $\mathcal{H}$. Otherwise, we process the counterexample, as we now explain in an example.

*Example 7.* Let $\mathcal{T}$ be the observation tree of Figure 2 with $\mathcal{B}^T = \{t_0, t_1\}$, $\mathcal{F}^T = \{t_2, t_3\}$, and $\mathit{compat}^T(t_2) = \mathit{compat}^T(t_3) = \{(t_1, x_1 \mapsto x_1)\}$. Figure 2 also gives the MMT constructed from $\mathcal{T}$, which is not symbolically equivalent to the MMT of Figure 1, with $\mathbf{w} = i \cdot i \cdot \mathit{to}[1] \cdot \mathit{to}[2]$ as a counterexample. We extend $\mathcal{T}$ such that $\mathbf{w}$ can be read in $\mathcal{T}$. That is, we call $\mathbf{WQ}^s(t_5)$ and discover that the transition from $t_1$ to $t_3$ must start the timer $x_3$. Hence, $t_3$ has no compatible state anymore (i.e., we found a new apartness pair) and gets promoted. After completing the tree and performing $\mathbf{WQ}^s$ on the frontier states, we get the tree from Figure 3.

In our example, simply adding the symbolic word provided by the teacher
was enough to discover a new apartness pair (meaning that the hypothesis can
no longer be constructed). However, there may be cases where we need to *replay*
(see Example 5) a part of the newly added run $t_0 \xrightarrow{w}$: split the run into $t_0 \xrightarrow{u} t \xrightarrow{v}$
with $t \in \mathcal{F}^T$ and replay $t \xrightarrow{v}$ from the state compatible with $t$ that was selected
to build the hypothesis. Repeat this principle until a compatible set is reduced.
<table><caption>**Table 1.** Experimental Results.</caption><thead><tr><th>Model</th><th>Q</th><th>I</th><th>X</th><th>WQ<sup>s</sup></th><th>OQ<sup>s</sup></th><th>EQ<sup>s</sup></th><th>Time[ms]</th></tr></thead><tbody><tr><td>AKM</td><td>4</td><td>5</td><td>1</td><td>22</td><td>35</td><td>2</td><td>684</td></tr><tr><td>CAS</td><td>8</td><td>4</td><td>1</td><td>60</td><td>89</td><td>3</td><td>1344</td></tr><tr><td>Light</td><td>4</td><td>2</td><td>1</td><td>10</td><td>13</td><td>2</td><td>302</td></tr><tr><td>PC</td><td>8</td><td>9</td><td>1</td><td>75</td><td>183</td><td>4</td><td>2696</td></tr><tr><td>TCP</td><td>11</td><td>8</td><td>1</td><td>123</td><td>366</td><td>8</td><td>3182</td></tr><tr><td>Train</td><td>6</td><td>3</td><td>1</td><td>32</td><td>28</td><td>3</td><td>1559</td></tr><tr><td>MMT of Fig. 1</td><td>3</td><td>1</td><td>2</td><td>11</td><td>5</td><td>2</td><td>1039</td></tr><tr><td>FDDI 1-station</td><td>9</td><td>2</td><td>2</td><td>32</td><td>20</td><td>1</td><td>1105</td></tr><tr><td>Oven</td><td>12</td><td>5</td><td>1</td><td>907</td><td>317</td><td>3</td><td>9452</td></tr><tr><td>WSN</td><td>9</td><td>4</td><td>1</td><td>175</td><td>108</td><td>4</td><td>3291</td></tr></tbody></table>

## 4 Implementation and Experiments

We have implemented $L_{MMT}^{\#}$ as an open-source tool.<fnref n="10" /> Note that our prototype implementation only uses symbolic queries, with no explicit translation into concrete ones. As we do not yet have a timed conformance testing algorithm for checking equivalence between a hypothesis and the teacher’s MMT, we utilize a BFS algorithm to check for symbolic equivalence between the two MMTs.<fnref n="11" />

We evaluated the performance of our tool on a selection of both real and synthetic benchmarks. We use the AKM, TCP and Train benchmarks from [32], and the CAS, Light and PC benchmarks from [1]. These have also been used for experimental evaluation by [26, 32, 34] and can be described as Mealy machines with a single timer (MM1Ts). We introduce two additional benchmarks with two timers: a model of an FDDI station [25, 34] (see [7, Appendix F] for details on our adaptation), and the MMT of Figure 1. We did not include the FDDI 2 process benchmark from [34], as our implementation cannot (yet) handle the corresponding generalized MMTs. Finally, we learned instances of the Oven and WSN MMLTs benchmarks from [26]. We modified the timing parameters to generate smaller MM1Ts. For each experiment, we record the number of OQ<sup>s</sup>, WQ<sup>s</sup>, EQ<sup>s</sup>, and the time taken to finish the experiment. Note, in practice, a WQ<sup>s</sup>, in addition to returning the list of timeouts and their constants, also provides the outputs of the timeout transitions. This is straightforward, as a WQ<sup>s</sup> must necessarily trigger the timeouts in order to observe them. Thus, we do not count the OQ<sup>s</sup> associated with a WQ<sup>s</sup>.<fnref n="12" />

The results are given in Table 1. Here, we highlight that the presented data is only meant to indicate that our algorithm is able to learn these models within a reasonable amount of time. The table also gives insight into which benchmarks require more or less (symbolic) queries to be learned with our algorithm.

<footnote n="10">¹⁰ See: https://gitlab.science.ru.nl/bharat/mmt_lsharp and Zenodo [18].</footnote>

<footnote n="11">¹¹ That is, seeking a difference in behavior in the product of the two MMTs.</footnote>

<footnote n="12">¹² An upper bound on the number of OQ<sup>s</sup> can be obtained by adding $|X||WQ<sup>s</sup>|$ to the values for $|OQ<sup>s</sup>|$.</footnote>
Comparison with other learning algorithms for timed systems is complicated. First, we need to convert the numbers of symbolic $L_{MMT}^{#}$ queries to concrete queries. As our prototype does not implement the concrete queries, we can only use the theoretical polynomial bounds given in Lemma 2. Note that for MM1Ts, each symbolic query can be implemented using a single concrete query (see Lemma 3 in [32]). For the FDDI protocol using two timers, we need at most 1282 concrete queries in total while around 118200 queries are used in [34]. Second, several algorithms presented in the literature learn TAs [1, 4, 34, 35]. Typically, these models have different numbers of states and transitions than an MMT model: Mealy machines tend to be more compact than TAs, but the use of timers may lead to more states than a TA encoding. Therefore we cannot just compare numbers of queries. As a third complication, equivalence queries can be implemented in different ways, which may affect the total number of queries required for learning. Finally, concerning models close to our MMTs, MMLTs [26] can be converted to equivalent MM1Ts [32], but this may blow up the number of states. Since $L_{MMT}^{#}$ learns the MM1Ts, it is less efficient than the MMLT learner of [26] which learns the more compact MMLT representations, or than the learner of [32] specially designed for MM1Ts. However, $L_{MMT}^{#}$ can handle a larger class of models, as it can handle multiple timers.

# 5 Future work

A major challenge in $L_{MMT}^{#}$ is to infer the update on transitions. This would become easier if we know in advance that timers can only be started by specific inputs, akin to what is done in *event recording automata* (ERA) [3] for TAs. Although, as discussed in [32], the restrictions of ERAs make it hard to capture the timing behavior of standard network protocols. It would be interesting to study the theoretical complexity of learning a system that can be modelled by ERAs as well as MMTs. A more interesting trail would be to allow transitions to start multiple timers, instead of a single one, which would permit more complex models (such as those resulting of parallel composition of simpler models) to be learned. It would also be interesting to explore the theory of generalized MMTs.

# References

1. Aichernig, B.K., Pferscher, A., Tappler, M.: From Passive to Active: Learning Timed Automata Efficiently. In: Lee, R., Jha, S., Mavridou, A. (eds.) Proceedings of the 12th International Symposium NASA Formal Methods, NFM 2020. Lecture Notes in Computer Science, vol. 12229, pp. 1–19. Springer (2020). https://doi.org/10.1007/978-3-030-55754-6_1

2. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8

3. Alur, R., Fix, L., Henzinger, T.A.: Event-Clock Automata: A Determinizable Class of Timed Automata. Theoretical Computer Science 211(1-2), 253–273 (1999). https://doi.org/10.1016/S0304-3975(97)00173-4
4. An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning One-Clock Timed Automata. In: Biere, A., Parker, D. (eds.) Proceedings of the 26th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020. Lecture Notes in Computer Science, vol. 12078, pp. 444–462. Springer (2020). https://doi.org/10.1007/978-3-030-45190-5_25

5. Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation 75(2), 87–106 (1987). https://doi.org/10.1016/0890-5401(87)90052-6

6. Bojanczyk, M., Lasota, S.: A machine-independent characterization of timed languages. In: Czumaj, A., Mehlhorn, K., Pitts, A.M., Wattenhofer, R. (eds.) Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II. Lecture Notes in Computer Science, vol. 7392, pp. 92–103. Springer (2012). https://doi.org/10.1007/978-3-642-31585-5_12

7. Bruyère, V., Garhewal, B., Pérez, G.A., Staquet, G., Vaandrager, F.W.: Active Learning of Mealy Machines with Timers. CoRR abs/2403.02019 (2024). https://doi.org/10.48550/ARXIV.2403.02019

8. Bruyère, V., Pérez, G.A., Staquet, G., Vaandrager, F.W.: Automata with Timers. In: Petrucci, L., Sproston, J. (eds.) Proceedings of the 21st International Conference Formal Modeling and Analysis of Timed Systems, FORMATS 2023. Lecture Notes in Computer Science, vol. 14138, pp. 33–49. Springer (2023). https://doi.org/10.1007/978-3-031-42626-1_3

9. Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8

10. Dierl, S., Howar, F.M., Kauffman, S., Kristjansen, M., Larsen, K.G., Lorber, F., Mauritz, M.: Learning Symbolic Timed Models from Concrete Timed Data. In: Rozier, K.Y., Chaudhuri, S. (eds.) Proceedings of the 15th International Symposium NASA Formal Methods, NFM 2023. Lecture Notes in Computer Science, vol. 13903, pp. 104–121. Springer (2023). https://doi.org/10.1007/978-3-031-33170-1_7

11. Dill, D.L.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) Proceedings of the International Workshop Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, vol. 407, pp. 197–212. Springer (1989). https://doi.org/10.1007/3-540-52148-8_17

12. Doveri, K., Ganty, P., Srivathsan, B.: A Myhill-Nerode style characterization for timed automata with integer resets. In: Barman, S., Lasota, S. (eds.) 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2024, December 16-18, 2024, Gandhinagar, Gujarat, India. LIPICS, vol. 323, pp. 21:1–21:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2024). https://doi.org/10.4230/LIPICS.FSTTCS.2024.21

13. Ferreira, T., Brewton, H., D'Antoni, L., Silva, A.: Prognosis: closed-box analysis of network protocol implementations. In: Kuipers, F.A., Caesar, M.C. (eds.) Proceedings of the ACM SIGCOMM 2021 Conference. pp. 762–774. ACM (2021). https://doi.org/10.1145/3452296.3472938

14. Fiterau-Brostean, P., Howar, F.: Learning-Based Testing the Sliding Window Behavior of TCP Implementations. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) Proceedings of the Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems FMICS and 17th International Workshop on Automated Verification
of Critical Systems AVoCS 2017. Lecture Notes in Computer Science, vol. 10471, pp. 185–200. Springer (2017). https://doi.org/10.1007/978-3-319-67113-0_12

15. Fiterau-Brostean, P., Janssen, R., Vaandrager, F.W.: Combining Model Learning and Model Checking to Analyze TCP Implementations. In: Chaudhuri, S., Farzan, A. (eds.) Proceedings of the 28th International Conference Computer Aided Verification, CAV 2016. Lecture Notes in Computer Science, vol. 9780, pp. 454–471. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6_25

16. Fiterau-Brostean, P., Jonsson, B., Merget, R., de Ruiter, J., Sagonas, K., Somorovsky, J.: Analysis of DTLS Implementations Using Protocol State Fuzzing. In: Capkun, S., Roesner, F. (eds.) Proceedings of the 29th USENIX Security Symposium, USENIX Security 2020. pp. 2523–2540. USENIX Association (2020), https://www.usenix.org/conference/usenixsecurity20/presentation/fiterau-brostean

17. Fiterau-Brostean, P., Lenaerts, T., Poll, E., de Ruiter, J., Vaandrager, F.W., Verleg, P.: Model learning and model checking of SSH implementations. In: Erdogmus, H., Havelund, K. (eds.) Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. pp. 142–151. ACM (2017). https://doi.org/10.1145/3092282.3092289

18. Garhewal, B.: L\# MMT artifact (2024). https://doi.org/10.5281/ZENODO.10647627, https://zenodo.org/doi/10.5281/zenodo.10647627

19. Garhewal, B., Vaandrager, F.W., Howar, F., Schrijvers, T., Lenaerts, T., Smits, R.: Grey-Box Learning of Register Automata. In: Dongol, B., Troubitsyna, E. (eds.) Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12546, pp. 22–40. Springer (2020). https://doi.org/10.1007/978-3-030-63461-2_2

20. Grinchtein, O., Jonsson, B., Leucker, M.: Learning of Event-Recording Automata. In: Lakhnech, Y., Yovine, S. (eds.) Proceedings of the Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems - Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004. Lecture Notes in Computer Science, vol. 3253, pp. 379–396. Springer (2004). https://doi.org/10.1007/978-3-540-30206-3_26

21. Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theoretical Computer Science 411(47), 4029–4054 (2010). https://doi.org/10.1016/J.TCS.2010.07.008

22. Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of Event-Recording Automata Using Timed Decision Trees. In: Baier, C., Hermanns, H. (eds.) Proceedings of the 17th International Conference Concurrency Theory, CONCUR 2006. Lecture Notes in Computer Science, vol. 4137, pp. 435–449. Springer (2006). https://doi.org/10.1007/11817949_29

23. Henry, L., Jéron, T., Markey, N.: Active Learning of Timed Automata with Unobservable Resets. In: Bertrand, N., Jansen, N. (eds.) Proceedings of the 18th International Conference Formal Modeling and Analysis of Timed Systems, FOR-MATS 2020. Lecture Notes in Computer Science, vol. 12288, pp. 144–160. Springer (2020). https://doi.org/10.1007/978-3-030-57628-8_9

24. Howar, F., Steffen, B.: Active Automata Learning in Practice - An Annotated Bibliography of the years 2011 to 2016. In: Bennaceur, A., Hähnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits - International Dagstuhl Seminar 16172, Dagstuhl Castle, Germany, April 24-27,
2016, Revised Papers. Lecture Notes in Computer Science, vol. 11026, pp. 123–148.
Springer (2018). https://doi.org/10.1007/978-3-319-96562-8_5

25. Johnson, M.J.: Proof that Timing Requirements of the FDDI Token Ring Protocol are Satisfied. IEEE Transactions on Computers **35**(6), 620–625 (1987). https://doi.org/10.1109/TCOM.1987.1096832

26. Kogel, P., Klös, V., Glesner, S.: Learning Mealy Machines with Local Timers. In: Li, Y., Tahar, S. (eds.) Proceedings of the 24th International Conference on Formal Engineering Methods Formal Methods and Software Engineering, ICFEM 2023. Lecture Notes in Computer Science, vol. 14308, pp. 47–64. Springer (2023). https://doi.org/10.1007/978-981-99-7584-6_4

27. Maler, O., Pnueli, A.: On Recognizable Timed Languages. In: Walukiewicz, I. (ed.) Proceedings of the 7th International Conference Foundations of Software Science and Computation Structures, FOSSACS 2004. Lecture Notes in Computer Science, vol. 2987, pp. 348–362. Springer (2004). https://doi.org/10.1007/978-3-540-24727-2_25

28. de Ruiter, J., Poll, E.: Protocol State Fuzzing of TLS Implementations. In: Jung, J., Holz, T. (eds.) Proceedings of the 24th USENIX Security Symposium, USENIX Security 15. pp. 193–206. USENIX Association (2015), https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter

29. Shahbaz, M., Groz, R.: Inferring Mealy Machines. In: Cavalcanti, A., Dams, D. (eds.) Proceedings of the 16th Formal Methods, FM 2009. Lecture Notes in Computer Science, vol. 5850, pp. 207–222. Springer (2009). https://doi.org/10.1007/978-3-642-05089-3_14

30. Tappler, M., Aichernig, B.K., Larsen, K.G., Lorber, F.: Time to Learn - Learning Timed Automata from Tests. In: André, É., Stoelinga, M. (eds.) Proceedings of the 17th International Conference Formal Modeling and Analysis of Timed Systems, FORMATS 2019. Lecture Notes in Computer Science, vol. 11750, pp. 216–235. Springer (2019). https://doi.org/10.1007/978-3-030-29662-9_13

31. Vaandrager, F.W.: Model learning. Communications of the ACM **60**(2), 86–95 (2017). https://doi.org/10.1145/2967606

32. Vaandrager, F.W., Bloem, R., Ebrahimi, M.: Learning Mealy Machines with One Timer. In: Leporati, A., Martín-Vide, C., Shapira, D., Zandron, C. (eds.) Proceedings of the 15th International Conference Language and Automata Theory and Applications, LATA 2021. Lecture Notes in Computer Science, vol. 12638, pp. 157–170. Springer (2021). https://doi.org/10.1007/978-3-030-68195-1_13

33. Vaandrager, F.W., Garhewal, B., Rot, J., Wißmann, T.: A New Approach for Active Automata Learning Based on Apartness. In: Fisman, D., Rosu, G. (eds.) Proceedings of the 28th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Lecture Notes in Computer Science, vol. 13243, pp. 223–243. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_12

34. Waga, M.: Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization. In: Enea, C., Lal, A. (eds.) Proceedings of the 35th International Conference Computer Aided Verification, CAV 2023. Lecture Notes in Computer Science, vol. 13964, pp. 3–26. Springer (2023). https://doi.org/10.1007/978-3-031-37706-8_1

35. Xu, R., An, J., Zhan, B.: Active Learning of One-Clock Timed Automata Using Constraint Solving. In: Bouajjani, A., Holík, L., Wu, Z. (eds.) Proceedings of the 20th International Symposium Automated Technology for Verification and Analysis, ATVA 2022. Lecture Notes in Computer Science, vol. 13505, pp. 249–265. Springer (2022). https://doi.org/10.1007/978-3-031-19992-9_16