11institutetext: Technical University of Dortmund, Dortmund, Germany
22institutetext: Uppsala University, Uppsala, Sweden 33institutetext: National
Technical University of Athens, Athens, Greece

# Scalable Tree-based Register Automata Learning (Extended Version with
Appendices)††thanks: A version of this paper without appendices appears in the
proceedings of TACAS 2024.

Simon Dierl 11 0000-0001-9730-9335 Paul Fiterau-Brostean 22
0000-0002-5185-0035 Falk Howar 11 0000-0002-9524-4459 Bengt Jonsson 22
0000-0001-7897-601X Konstantinos Sagonas 2233 0000-0001-9657-0179 Fredrik
Tåquist 22 0000-0003-4066-9078

###### Abstract

Existing active automata learning (AAL) algorithms have demonstrated their
potential in capturing the behavior of complex systems (e.g., in analyzing
network protocol implementations). The most widely used AAL algorithms
generate finite state machine models, such as Mealy machines. For many
analysis tasks, however, it is crucial to generate richer classes of models
that also show how relations between data parameters affect system behavior.
Such models have shown potential to uncover critical bugs, but their learning
algorithms do not scale beyond small and well curated experiments. In this
paper, we present ${SL}^{\lambda}$, an effective and scalable register
automata (RA) learning algorithm that significantly reduces the number of
tests required for inferring models. It achieves this by combining a tree-
based cost-efficient data structure with mechanisms for computing short and
restricted tests. We have implemented ${SL}^{\lambda}$ as a new algorithm in
RALib. We evaluate its performance by comparing it against ${SL}^{*}$, the
current state-of-the-art RA learning algorithm, in a series of experiments,
and show superior performance and substantial asymptotic improvements in
bigger systems.

###### Keywords:

Active automata learning, Register automata

##  1 Introduction

_Model Learning_ (aka _Active Automata Learning_ (AAL) [7, 39, 49]) infers
automata models that represent the dynamic behavior of a software or hardware
component from tests. Models obtained through (active) learning have proven
useful for many purposes, such as analyzing security protocols [44, 24, 40,
18, 17], mining APIs [6], supporting model-based testing [25, 51, 46] and
conformance testing [5]. The AAL algorithms employed in these works are
efficient and supported by various domain-specific optimizations (e.g., [30]),
but they all generate finite state machine (FSM) models, such as Mealy
machines.

For many analysis tasks, however, it is crucial for models to also be able to
describe _data flow_ , i.e., constraints on data parameters that are passed
when the component interacts with its environment, as well as the mutual
influence between dynamic behavior and data flow. For instance, models of
protocol components must describe how different parameter values in sequence
numbers, identifiers, etc. influence the behavior, and vice versa. Existing
techniques for extending AAL to _Extended FSM_ (EFSM) models [10, 1, 8] take
several different approaches. Some reduce the problem to inferring FSMs by
using manually supplied abstractions on the data domain [1], which requires
insight into the control/data dependencies of a system under learning (SUL).
Others extend AAL for finite state models by allowing transitions to contain
predicates over rich data domains, but cannot generate state variables to
model data dependencies between consecutive interactions [12, 34]. Finally,
there exist extensions of AAL to EFSM models with guards and state variables,
such as _register automata_ [3, 2, 10]. While their potential has been shown
by being able to uncover critical bugs in e.g., TCP implementations [15, 14],
their learning algorithms do not scale beyond small and well curated
experiments.

We follow the third line of works and address the scalability of register
automata (RA) learning algorithms in our work. The main challenge when scaling
AAL algorithms is reducing the number of tests that learners perform on a SUL.
Generally, these tests are sequences of actions of the form $u\cdot v$, where
$u$ is the prefix and $v$ the suffix of the sequence. Tests $u\cdot v$ and
$u^{\prime}\cdot v$ are then used to determine if prefixes $u$ and
$u^{\prime}$ can be distinguished based on the SUL’s output triggered by $v$.
When inferring RA models, prefixes are sequences of actions with data values,
e.g., $\mathsf{push}(1)\,\mathsf{push}(2)$, and suffixes are sequences of
actions with symbolic parameters, e.g.,
$\mathsf{pop}(p_{1})\,\mathsf{pop}(p_{2})$, that, when instantiated, can incur
a number of tests that is exponential in the length of the suffix for
identifying dependencies between prefix values and suffix parameters, e.g.,
different test outcomes for $(p_{1}=2\land p_{2}=1)$ and $(p_{1}=2\land
p_{2}=3)$, and for distinguishing prefixes based on suffixes. To make register
automata learning scalable, it is crucial to reduce the use of suffixes in
tests along three dimensions:  (i) First, it is important to use only _few
tests_.  (ii) Second, when using suffixes in tests, _shorter suffixes_ should
be preferred over longer ones.  (iii) Third, it is essential to _restrict
tests to relevant dependencies_ between prefix values and suffix parameters
instead of bluntly testing all possible dependencies.

In this paper, we present the ${SL}^{\lambda}$ algorithm for learning register
automata which achieves scalability by optimizing the use of tests and
suffixes in tests in the three stated dimensions. ${SL}^{\lambda}$ uses a
_classification tree_ as a data structure, constructs a minimal prefix-closed
set of prefixes and a suffix-closed set of _short_ and _restricted_ suffixes
for identifying and distinguishing locations, transitions, and registers.
Technically, we adopt the idea of using a classification tree from learners
for FSMs [32, 31] where it proved very successful for reducing tests. We also
adopt the technique of computing short suffixes incrementally in order to keep
them short [7, 31]. This has not been studied for RAs before and leads to an
improved worst case complexity compared to state-of-the-art approaches
(Theorem 5.1). Finally, we show how suffixes can be restricted to relevant
data dependencies, which is essential for achieving scalability (Section 4).

We have implemented ${SL}^{\lambda}$ as a new algorithm in the RALib111RALib
is available at https://github.com/LearnLib/ralib. tool [9]. For comparison,
we have also implemented in RALib the ${SL}^{CT}$ algorithm that uses a
classification tree but relies on suffixes from counterexamples instead of
computing short suffixes from inconsistencies. We evaluate the
${SL}^{\lambda}$ algorithm by comparing its performance against the ${SL}^{*}$
[10] and ${SL}^{CT}$ algorithms in a series of experiments, confirming that:
(i) classification trees scale much better than observation tables for
register automata,  (ii) using restricted suffixes leads to a dramatic
reduction of tests for all compared algorithms, and  (iii) computing short
suffixes from inconsistencies outperforms using suffixes from counterexamples.

Related Work. For a broad overview of AAL refer to the survey paper of de la
Higuera [26] from 2005 and to a more recent paper by Howar and Steffen [27].

Learning beyond DFAs has been investigated for many models aside from register
automata. For example, algorithms have been presented for workflow Petri nets
[13], data automata [23], generic nondeterministic transition systems [50],
symbolic automata [12], one-timer automata [47], and systems of procedural
automata [21]. Learning of register automata has been performed by combining a
FSM learner with the Tomte front-end [3, 2]. A different approach using
bespoke RA learning algorithms [29, 36] has been implemented in RALib. Active
learning algorithms for nominal automata, which extend FSMs to infinite
alphabets and infinite sets of states, have also been developed [37]. While
the expressivity of nominal DFAs is equivalent to that of deterministic
register automata with equality, nominal automata do not represent registers
symbolically but through permutations on infinite sets, leading to big models
(e.g., for storing some data value twice) and active learning algorithms with
a high query complexity.

Applications of AAL are diverse. Active learning enables the generation of
behavioral models for software [45, 42], e.g. for network protocol
implementations [40], enabling security analyses and model checking [4, 19,
20]. It can be used in testing [35, 43] and to enable formal analyses [49].
Finally, it can be combined with passive learning approaches to support life-
long learning [22]. More theoretical advances include the use of Galois
connections to model SUL-oracle mappers [33] and the introduction of apartness
[48], to formalize state distinction.

Outline. We present the key ideas in tree-based learning of RA informally in
the next section, before providing formal definitions of basic concepts in
Section 3. Sections 4, 6 and 5 present the ${SL}^{\lambda}$ algorithm, its
properties, and the experimental evaluation of its performance. The paper ends
with few concluding remarks.

##  2 Main Ideas

In this section, we introduce the main ideas behind the ${SL}^{\lambda}$
algorithm. As illustrating example, we will use a stack of capacity two, which
stores a sequence of natural numbers. The stack supports the operations
$\mathsf{push}$ and $\mathsf{pop}$, both of which take one natural number as a
parameter. The operation $\mathsf{push}(\mathtt{d})$ succeeds if the stack is
not full, i.e., contains at most one element; the operation
$\mathsf{pop}(\mathtt{d})$ succeeds if the last pushed and not yet popped
element is $\mathtt{d}$. Let a _symbol_ denote an operation with data value,
such as $\mathsf{push}(1)$, and let $\mathcal{L}_{\mathit{Stack}}$ denote the
prefix-closed language consisting of the words of symbols representing
sequences of successful operations. Figure 1 shows an acceptor for
$\mathcal{L}_{\mathit{Stack}}$. The initial location $l_{0}$ corresponds to an
empty stack, location $l_{1}$ corresponds to a stack with one element, and
$l_{2}$ to a location where the stack is full. There is also an implicit sink
location for each word that is not accepted by $\mathcal{L}_{\mathit{Stack}}$,
e.g. pushing a third element, or popping a non-top element. In each location,
registers contain the elements in the stack: for $i=0,1,2$, location $l_{i}$
has $i$ registers, where the register with the highest index contains the
topmost stack element.

$l_{0}$$l_{1}$$l_{2}$$\scriptstyle\emptyset$$\scriptstyle\\{x_{1}\\}$$\scriptstyle\\{x_{1},x_{2}\\}$$\frac{\mathsf{push}(p)~{}|~{}true}{x_{1}:=p}$$\frac{\mathsf{pop}(p)~{}|~{}p=x_{1}}{-}$$\frac{\mathsf{push}(p)~{}|~{}true}{x_{1}:=x_{1},x_{2}:=p}$$\frac{\mathsf{pop}(p)~{}|~{}p=x_{2}}{x_{1}:=x_{1}}$
Figure 1: Register automaton accepting language of stack with capacity two.

The task of the ${SL}^{\lambda}$ algorithm is to learn the acceptor in Fig. 1
in a black-box scenario, i.e., knowing only the operations ($\mathsf{push}$
and $\mathsf{pop}$) and the relations that may be used in guards (here tests
for equality), by asking two kinds of queries. A _membership query_ asks
whether a word $w$ is in $\mathcal{L}$; it can be realized by a simple test.
An _equivalence query_ asks whether a hypothesis RA accepts $\mathcal{L}$; if
so, the query is answered by $yes$, otherwise by a _counterexample_ , which is
a word on which the hypothesis and $\mathcal{L}$ disagree; in a black box
setting it is typically approximated by a conformance testing algorithm. Like
other AAL algorithms, ${SL}^{\lambda}$ iterates a cycle in which membership
queries are used to construct a hypothesis, which is then subject to
validation by an equivalence query. If a counterexample is found, hypothesis
construction is resumed, etc., until a hypothesis agrees with $\mathcal{L}$.

Classical AAL algorithms that learn DFAs maintain an expanding set of words,
$S_{p}$, called _short prefixes_ , and an expanding set of words, called
_suffixes_ , which induce an equivalence relation $\equiv$ on prefixes,
defined by $u\equiv u^{\prime}$ iff $uv\in\mathcal{L}\Leftrightarrow
u^{\prime}v\in\mathcal{L}$ for all suffixes $v$; this allows equivalence
classes of prefixes to represent states in a DFA. The ${SL}^{\lambda}$
algorithm maintains a set ${U}$ of data words called _prefixes_ , which is the
union of $S_{p}$ and one-symbol extensions of elements in $S_{p}$. Instead of
suffixes, ${SL}^{\lambda}$ maintains a set $\mathcal{V}$ of _symbolic
suffixes_ , each of which is a _parameterized_ word, i.e., a word where data
values are replaced by parameters $p_{1},\ldots,p_{m}$. For each prefix $u$,
say $\mathsf{push}(0)$, and symbolic suffix $\vec{v}$, say
$\mathsf{push}(p_{1})\mathsf{pop}(p_{2})$, membership in $\mathcal{L}$ of
words of form $u\vec{v}$ depends on the relation between the data values of
$u$ and the parameters $p_{1},p_{2}$ of $\vec{v}$, which in ${SL}^{\lambda}$
is represented by a function ${\cal L}[u,\vec{v}]$ with parameters $x_{1}$
(representing the data value of $u$), $p_{1}$, and $p_{2}$. In this case
${\cal L}[u,\vec{v}](x_{1},p_{1},p_{2})$ is $+$ iff $p_{2}=p_{1}$ and $-$
otherwise. In ${SL}^{\lambda}$, such functions are represented as decision
trees of a specific form.

${\it true}$$p_{2}=p_{1}$$p_{2}\neq p_{1}$ Figure 2: Decision tree for ${\cal
L}[u,\vec{v}](x_{1},p_{1},p_{2})$.

Figure 2 shows the decision tree for the just described function. Note that it
checks constraints for parameters one at a time: first the constraint on only
$p_{1}$ (which is ${\it true}$), and thereafter the constraint on $p_{2}$ (a
comparison with $p_{1}$). Two prefixes $u$, $u^{\prime}$ are then equivalent
w.r.t. $\mathcal{V}$ if ${\cal L}[u,\vec{v}]$ and ${\cal
L}[u^{\prime},\vec{v}]$ are “isomorphic modulo renaming” for all
$\vec{v}\in\mathcal{V}$ (details in Section 4).

Functions of form ${\cal L}[u,\vec{v}]$ are generated by so-called _tree
queries_ , which perform membership queries for relevant combinations of
relations between data values in $u$ and parameters in $\vec{v}$, and
summarize the results in a canonical way. The tree query above requires five
membership queries. ${SL}^{\lambda}$ employs techniques for reducing this
number by restricting the symbolic suffix; see end of this section.

Initially, $S_{p}$ and $\mathcal{V}$ contain only the empty sequence
$\epsilon$. Since $\epsilon$ is a short prefix, one-symbol extensions,
$\mathsf{push}(0)$ and $\mathsf{pop}(0)$, are entered into ${U}$. Tree queries
are performed for the prefixes in ${U}$ and the empty suffix, revealing that
$\mathsf{push}(0)$ is accepted and $\mathsf{pop}(0)$ is rejected. Thus,
$\mathsf{push}(0)$ cannot be distinguished from $\epsilon$, but
$\mathsf{pop}(0)$ can, so it must lead to a new location, hereafter referred
to as the _sink_ , which is therefore added to $S_{p}$. One-symbol extensions
of $\mathsf{pop}(0)$, in this case $\mathsf{pop}(0)\mathsf{push}(1)$ and
$\mathsf{pop}(0)\mathsf{pop}(1)$, are added to ${U}$ and tree queries for them
and the empty suffix are performed, revealing that they cannot be separated
from the sink. At this point, we can formulate hypothesis $\mathcal{H}_{0}$ in
Fig. 3(left) from $S_{p}$, ${U},$ and the computed decision trees.

$l_{0}$sink$\scriptstyle\emptyset$$\scriptstyle\emptyset$$\mathcal{H}_{0}$
$\frac{\mathsf{push}(p)~{}|~{}true}{-}$$\frac{\mathsf{pop}(p)~{}|~{}true}{-}$$\frac{\mathsf{push}(p)~{}|~{}true}{-}$
$\frac{\mathsf{pop}(p)~{}|~{}true}{-}$

$l_{0}$$l_{1}$$l_{2}$$\scriptstyle\emptyset$$\scriptstyle\emptyset$$\scriptstyle\emptyset$$\mathcal{H}_{1}$
$\frac{\mathsf{push}(p)~{}|~{}true}{-}$$\frac{\mathsf{push}(p)~{}|~{}true}{-}$
(a)

$l_{0}$$l_{1}$$l_{2}$$\mathcal{H}_{2}$
$\scriptstyle\emptyset$$\scriptstyle\\{x_{1}\\}$$\scriptstyle\emptyset$$\frac{\mathsf{push}(p)~{}|~{}true}{x_{1}:=p}$$\frac{\mathsf{pop}(p)~{}|~{}p=x_{1}}{-}$$\frac{\mathsf{push}(p)~{}|~{}true}{-}$
(b)

Figure 3: Three hypotheses constructed by ${SL}^{\lambda}$: $\mathcal{H}_{0}$
(left), $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ (right).

This hypothesis is then subject to validation. Assume that it finds the
counterexample $\mathsf{push}(0)\mathsf{push}(1)\mathsf{push}(2)$, which is
accepted by $\mathcal{H}_{0}$ but rejected by $\mathcal{L}_{\mathit{Stack}}$.
Analysis of this counterexample reveals that $\epsilon$ and $\mathsf{push}(0)$
are inequivalent, since they are separated by the suffix
$\mathsf{push}(p_{1})\mathsf{push}(p_{2})$ (since the concatenation of
$\epsilon$ and $\mathsf{push}(p_{1})\mathsf{push}(p_{2})$ is accepted for all
$p_{1},p_{2}$ but $\mathsf{push}(0)\cdot\mathsf{push}(1)\mathsf{push}(2)$ is
always rejected for all $p_{1},p_{2}$). It could seem natural to add
$\mathsf{push}(p_{1})\mathsf{push}(p_{2})$ to $\mathcal{V}$, but
${SL}^{\lambda}$ will not do that, since it follows the principle (from
$L^{\lambda}$ [28]) that a new prefix in $S_{p}$ must extend an existing
prefix by one symbol, and that a new suffix in $\mathcal{V}$ must prepend one
symbol to an existing one. This principle keeps $S_{p}$ prefix-closed and
$\mathcal{V}$ suffix-closed, and aims to avoid inclusion of unnecessarily long
sequences. Therefore, instead of adding
$\mathsf{push}(p_{1})\mathsf{push}(p_{2})$ as a suffix, ${SL}^{\lambda}$
enters the prefix $\mathsf{push}(0)$ into $S_{p}$, and adds one-symbol
extensions of $\mathsf{push}(0)$, in this case
$\mathsf{push}(0)\mathsf{push}(1)$ and $\mathsf{push}(0)\mathsf{pop}(1)$, to
${U}$. It notes that $\mathsf{push}(0)\mathsf{push}(1)$ is inequivalent to
both $\epsilon$ and $\mathsf{push}(0)$, separated by the suffix
$\mathsf{push}(p_{1})$. Again, $\mathsf{push}(0)\mathsf{push}(1)$ is therefore
promoted to a short prefix, and its one-symbol extensions,
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{push}(2)$ and
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{pop}(2)$, are entered into ${U}$.
Now, ${SL}^{\lambda}$ is able to add suffixes to $\mathcal{V}$ that separate
all prefixes in $S_{p}$, by two operations that achieve consistency.

  1. 1.

The $\mathsf{push}$-extensions of $\epsilon$ and
$\mathsf{push}(0)\mathsf{push}(1)$, (i.e., $\mathsf{push}(0)$ and
$\mathsf{push}(0)\mathsf{push}(1)\\-\mathsf{push}(2)$) are separated by the
empty suffix, hence these two prefixes are separated by the suffix
$\mathsf{push}(p_{1})$, a one-symbol extension of $\epsilon$ which is added to
$\mathcal{V}$.

  2. 2.

The $\mathsf{push}$-extensions of $\epsilon$ and $\mathsf{push}(0)$ (i.e.,
$\mathsf{push}(0)$ and $\mathsf{push}(0)\mathsf{push}(1)$) are separated by
the suffix $\mathsf{push}(p_{1})$, hence $\epsilon$ and $\mathsf{push}(0)$ are
separated by $\mathsf{push}(p_{1})\mathsf{push}(p_{2})$, formed by prepending
a symbol to the just added suffix $\mathsf{push}(p_{1})$, which is added to
$\mathcal{V}$.

After adding the suffixes, the closedness and consistency criteria are met,
producing hypothesis $\mathcal{H}_{1}$ in Fig. 3(right, top). Assume that the
validation of $\mathcal{H}_{1}$ finds counterexample
$\mathsf{push}(0)\mathsf{pop}(0)$, which is in $\mathcal{L}_{\mathit{Stack}}$,
but rejected by $\mathcal{H}_{1}$. This counterexample reveals that after
$\mathsf{push}(0)$, the two continuations $\mathsf{pop}(0)$ and
$\mathsf{pop}(1)$ lead to inequivalent locations (separated by suffix
$\epsilon$), suggesting to refine the $\mathsf{pop}(p)$-transition after
$\mathsf{push}(0)$. To this end, $\mathcal{V}$ is extended by a suffix formed
by prepending $\mathsf{pop}(p)$ to the empty suffix, and a tree query is
invoked for ${\cal L}[\mathsf{push}(0),\mathsf{pop}(p_{1})]$, which is $+$ iff
$p_{1}=x_{1}$ and $-$ otherwise. Since ${\cal
L}[\mathsf{push}(0),\mathsf{pop}(p_{1})]$ makes a test for $x_{1}$, which
represents the data value of $\mathsf{push}(0)$, we infer that the data
parameter of the $\mathsf{push}(0)$-prefix must be remembered in a register,
and that the $\mathsf{pop}(p)$-transition must be split into two with guards
$(x_{1}\neq p)$ and $(x_{1}=p)$. The resulting hypothesis, $\mathcal{H}_{2}$,
is shown in Fig. 3(right, bottom), which is subject to another round of
validation; the subsequent hypothesis construction reveals the
$\mathsf{pop}$-transitions from $l_{2}$ in Fig. 1.

In ${SL}^{\lambda}$, the sets ${U}$ and $\mathcal{V}$ are maintained in a
_classification tree_ $CT$, a data structure that is specially designed to
represent how the suffixes in $\mathcal{V}$ partition ${U}$ into equivalence
classes corresponding to locations. This permits an optimization that can
elide superfluous membership queries. A classification tree is a decision
tree. Each leaf is labeled by a subset of ${U}$. Each inner node is labeled by
a symbolic suffix $\vec{v}$ and induces a subtree for each equivalence class
w.r.t. $\vec{v}$, whose leaves contain prefixes in this equivalence class. For
example, in Fig. 4, which shows a $CT$ corresponding to hypothesis
$\mathcal{H}_{1}$, the nodes are labeled by the suffixes $\epsilon$,
$\mathsf{push}(p_{1})$ and $\mathsf{push}(p_{1})\mathsf{push}(p_{2})$, which
separate the leaves into four equivalence classes corresponding to the four
locations in Fig. 1. Each edge is labeled by the results of the tree queries
for a prefix in its equivalence class and the symbolic suffix of the source
node.

$\epsilon$$\mathsf{push}(p_{1})$$\mathsf{push}(p_{1})\,\mathsf{push}(p_{2})$$\underline{\mathsf{pop}(0)}$
$\mathsf{pop}(0)\mathsf{push}(1)$ $\mathsf{pop}(0)\mathsf{pop}(1)$
$\mathsf{push}(0)\mathsf{pop}(1)$
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{pop}(2)$ $\underline{\epsilon}$
$\underline{\mathsf{push}(0)}$
$\underline{\mathsf{push}(0)\mathsf{push}(1)}$$true$$true$$true$$true$$true$$true$
Figure 4: Classification tree for hypothesis $\mathcal{H}_{1}$ in Fig. 3.
Short prefixes are underlined.

Each tree query requires a number of membership queries which may grow
exponentially with the length of the suffix. ${SL}^{\lambda}$ reduces this
number by _restricting_ the involved symbolic suffix to induce fewer
membership queries, as long as the tree query can still make the separation
between prefixes or transitions for which it was invoked. To illustrate,
recall that the analysis of the counterexample
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{push}(2)$ for $\mathcal{H}_{0}$ shows
that $\epsilon$ and $\mathsf{push}(0)$ are inequivalent. To separate these, we
need not naïvely use the symbolic suffix
$\mathsf{push}(p_{1})\mathsf{push}(p_{2})$; but we can restrict it by
considering only values of $p_{1}$ and $p_{2}$ that are _fresh_ , i.e.,
different from all other preceding parameters in the prefix and suffix. With
this restriction, the suffix can still separate $\epsilon$ and
$\mathsf{push}(0)$, and the tree query for prefix $\mathsf{push}(0)$ requires
only one membership query instead of five.

##  3 Data Languages and Register Automata

In this section, we review background concepts on data languages and register
automata. Our definitions are parameterized on a _theory_ , which is a pair
$\langle\mathcal{D},\mathcal{R}\rangle$ where $\mathcal{D}$ is a (typically
infinite) domain of data values, and $\mathcal{R}$ is a set of relations (of
arbitrary arity) on $\mathcal{D}$. Examples of theories include:  (i)
$\langle\mathbb{N},\\{=\\}\rangle$, the theory of natural numbers with
equality, and  (ii) $\langle\mathbb{R},\\{<\\}\rangle$, the theory of real
numbers with inequality; this theory also allows to express equality between
elements.  Theories can be extended with constants (allowing, e.g., theories
of sums with constants).

Data Languages. We assume a set $\Sigma$ of actions, each with an arity that
determines how many parameters it takes from the domain $\mathcal{D}$. For
simplicity, we assume that all actions have arity $1$; our techniques can be
extended to handle actions with arbitrary arities. A data symbol is a term of
form $\alpha(\mathtt{d})$, where $\alpha$ is an action and
$\mathtt{d}\in\mathcal{D}$ is a data value. A data word (or simply _word_) is
a finite sequence of data symbols. The concatenation of two words $u$ and $v$
is denoted $uv$, often we then refer to $u$ as a _prefix_ and $v$ as a
_suffix_. Two words
$w=\alpha_{1}(\mathtt{d}_{1})\ldots\alpha_{n}(\mathtt{d}_{n})$ and
$w^{\prime}=\alpha_{1}(\mathtt{d}_{1}^{\prime})\ldots\alpha_{n}(\mathtt{d}_{n}^{\prime})$
with the same sequences of actions are _$\mathcal{R}$ -indistinguishable_,
denoted $w\approx_{\mathcal{R}}w^{\prime}$, if
$R(\mathtt{d}_{i_{1}},\ldots,\mathtt{d}_{i_{j}})\Leftrightarrow
R(\mathtt{d}_{i_{1}}^{\prime},\ldots,\mathtt{d}_{i_{j}}^{\prime})$ whenever
$R$ is a $j$-ary relation in $\mathcal{R}$ and $i_{1},\cdots,i_{j}$ are
indices among $1\ldots n$. A data language $\mathcal{L}$ is a set of data
words that respects $\mathcal{R}$ in the sense that
$w\approx_{\mathcal{R}}w^{\prime}$ implies $w\in\mathcal{L}\Leftrightarrow
w^{\prime}\in\mathcal{L}$. We often represent data languages as mappings from
the set of words to $\\{+,-\\}$, where $+$ stands for accept and $-$ for
reject.

Register Automata. We assume a set of registers $x_{1},x_{2},\ldots$, and a
set of _formal parameters_ $p,p_{1},p_{2},\ldots$. A parameterized symbol is a
term of form $\alpha(p)$, where $\alpha$ is an action and $p$ a formal
parameter. A _constraint_ is a conjunction of negated and unnegated relations
(from $\mathcal{R}$) over registers and parameters. An _assignment_ is a
parallel update of registers with values from registers or the formal
parameter $p$. We represent it as a mapping $\pi$ from
$\\{x_{i_{1}},\ldots,x_{i_{m}}\\}$ to
$\\{x_{j_{1}},\ldots,x_{j_{n}}\\}\cup\\{p\\}$, meaning that the value
$\pi(x_{i_{k}})$ is assigned to $x_{i_{k}}$, for $k=1,\ldots,m$. In multiple-
assignment notation, this would be written
$x_{i_{1}},\ldots,x_{i_{m}}:=\pi(x_{i_{1}}),\ldots,\pi(x_{i_{m}})$.

###### Definition 1

A register automaton (RA) is a tuple
$\mathcal{A}=(L,l_{0},\mathcal{X},\Gamma,\lambda)$, where

  * •

$L$ is a finite set of locations, with $l_{0}\in L$ as the initial location,

  * •

$\mathcal{X}$ maps each location $l\in L$ to a finite set $\mathcal{X}(l)$ of
registers,

  * •

$\Gamma$ is a finite set of transitions, each of form $\langle
l,\alpha(p),g,\pi,l^{\prime}\rangle$, where

    * –

$l\in L$ is a source location and $l^{\prime}\in L$ is a target location,

    * –

$\alpha(p)$ is a parameterized symbol,

    * –

$g$, the _guard_ , is a constraint over $p$ and $\mathcal{X}(l)$, and

    * –

$\pi$ (the assignment) is a mapping from $\mathcal{X}(l^{\prime})$ to
$\mathcal{X}(l)\cup\\{p\\}$, and

  * •

$\lambda$ maps each $l\in L$ to $\\{+,-\\}$, where $+$ denotes accept and $-$
reject.  $\sqcap$$\sqcup$

A _state_ of a RA $\mathcal{A}=(L,l_{0},\mathcal{X},\Gamma,\lambda)$ is a pair
$\langle l,\mu\rangle$ where $l\in L$ and $\mu$ is a valuation over
$\mathcal{X}(l)$, i.e., a mapping from $\mathcal{X}(l)$ to $\mathcal{D}$. A
_step_ of $\mathcal{A}$, denoted $\langle
l,\mu\rangle\xrightarrow{\alpha(\mathtt{d})}\langle
l^{\prime},\mu^{\prime}\rangle$, transfers the state of $\mathcal{A}$ from
$\langle l,\mu\rangle$ to $\langle l^{\prime},\mu^{\prime}\rangle$ on input of
the data symbol $\alpha(\mathtt{d})$ if there is a transition $\langle
l,\alpha(p),g,\pi,l^{\prime}\rangle\in\Gamma$ such that  (i)
$\mu~{}\models~{}g[\mathtt{d}/p]$, i.e., $d$ satisfies the guard $g$ under the
valuation $\mu$, and  (ii) $\mu^{\prime}$is defined by
$\mu^{\prime}(x_{i})=\mu(x_{j})$ if $\pi(x_{i})=x_{j}$, otherwise
$\mu^{\prime}(x_{i})=d$ if $\pi(x_{i})=p$.  A _run_ of $\mathcal{A}$ over a
data word $w=\alpha(\mathtt{d}_{1})\ldots\alpha(\mathtt{d}_{n})$ is a sequence
of steps of $\mathcal{A}$

$\langle
l_{0},\mu_{0}\rangle~{}\xrightarrow{\alpha_{1}(\mathtt{d}_{1})}~{}\langle
l_{1},\mu_{1}\rangle\quad\ldots\quad\langle
l_{n-1},\mu_{n-1}\rangle~{}\xrightarrow{\alpha_{n}(\mathtt{d}_{n})}~{}\langle
l_{n},\mu_{n}\rangle$

for some initial valuation $\mu_{0}$. The run is accepting if
$\lambda(l_{n})=+$ and rejecting if $\lambda(l_{n})=-$. The word $w$ is
accepted (rejected) by $\mathcal{A}$ under $\mu_{0}$ if $\mathcal{A}$ has an
accepting (rejecting) run over $w$ from $\langle l_{0},\mu_{0}\rangle$. Define
the language $\mathcal{L}(\mathcal{A})$ of $\mathcal{A}$ as the set of words
accepted by $\mathcal{A}$. A language is _regular_ if it is the language of
some RA.

We require a RA to be _determinate_ , meaning that there is no data word over
which it has both accepting and rejecting runs. A determinate RA can be easily
transformed into a deterministic one by strengthening its guards, and a
deterministic RA is by definition also determinate. Our construction of RAs in
Section 4 will generate determinate RAs which are not necessarily
deterministic. RAs have been extended to Register Mealy Machines (RMM) in
several works and it has been established how RA learning algorithms can be
used to infer models of systems with inputs and outputs [9], which we do, too.

##  4 The $SL^{\lambda}$ Learning Algorithm

In this section, we present the main building blocks of ${SL}^{\lambda}$
before an overview of the main algorithm, followed by techniques for reducing
the cost of tree queries (page 4) and for analyzing counterexamples (page 4).

Symbolic Decision Trees. The functions, of form ${\cal L}[u,\vec{v}]$, that
result from tree queries, should represent how the language $\mathcal{L}$ to
be learned processes instantiations of $\vec{v}$ after the prefix $u$. Since
${SL}^{\lambda}$ is intended to construct canonical RAs, it is natural to let
these functions have the form of a tree-shaped “mini-RA”, which we formalize
as _symbolic decision trees_ of a certain form.

For a word $u=\alpha_{1}(\mathtt{d}_{1})\ldots\alpha_{k}(\mathtt{d}_{k})$ and
a symbolic suffix
$\vec{v}=\alpha_{1}^{\prime}(p_{1})\ldots\alpha_{m}^{\prime}(p_{m})$ a
$(u,\vec{v})$-path $\tau$ is a sequence $g_{1},\ldots,g_{m}$, where each
$g_{i}$ is a constraint over $x_{1},\ldots,x_{k}$ and $p_{1},\ldots,p_{i}$.
Define the condition represented by $\tau$, denoted ${\cal G}_{\tau}$, as
$g_{1}\land\cdots\land g_{m}$. A $(u,\vec{v})$-tree $T$ is a mapping from a
set $Dom(T)$ of $(u,\vec{v})$-paths to $\\{+,-\\}$. Write
$\overline{\mathtt{d}}$ for $\mathtt{d}_{1},\ldots,\mathtt{d}_{k}$,
$\overline{\mathtt{d}^{\prime}}$ for
$\mathtt{d}^{\prime}_{1},\ldots,\mathtt{d}^{\prime}_{m}$, $\overline{x}$ for
$x_{1},\ldots,x_{k}$ and $\overline{p}$ for $p_{1},\ldots,p_{m}$. A
$(u,\vec{v})$-tree $T$ can be seen a function with parameters
$\overline{x},\overline{p}$ to $\\{+,-\\}$, defined by
$T(\overline{x},\overline{p})=T(\tau)$ whenever $\tau\in Dom(T)$ and ${\cal
G}_{\tau}(\overline{x},\overline{p})$ holds. That is, for data values
$\overline{\mathtt{d}}$ and $\overline{\mathtt{d}^{\prime}}$ and each
$(u,\vec{v})$-path $\tau$, we have
$T(\overline{\mathtt{d}},\overline{\mathtt{d}^{\prime}})=T(\tau)$ whenever
${\cal G}_{\tau}(\overline{\mathtt{d}},\overline{\mathtt{d}^{\prime}})$ is
true. If $\mathcal{L}$ is a data language, then ${\cal L}[u,\vec{v}]$ is a
$(u,\vec{v})$-tree representing membership in $\mathcal{L}$ in the sense that
for any values of $p_{1},\ldots,p_{m}$ we have ${\cal
L}[u,\vec{v}](\overline{\mathtt{d}},\overline{p})=+$ iff
$u\alpha_{1}^{\prime}(p_{1})\ldots\alpha_{m}^{\prime}(p_{m})\in\mathcal{L}$,
and ${\cal L}[u,\vec{v}](\overline{\mathtt{d}},\overline{p})=-$ iff
$u\alpha_{1}^{\prime}(p_{1})\ldots\alpha_{m}^{\prime}(p_{m})\not\in\mathcal{L}$.
For example, Fig. 2 shows a $(u,\vec{v})$-tree where
$u=\mathsf{push}(\mathtt{d}_{1})$ and
$\vec{v}=\mathsf{push}(p_{1})\mathsf{pop}(p_{2})$. This tree maps the
$(u,\vec{v})$-path ${\it true}\land p_{2}=p_{1}$ to $+$ and ${\it true}\land
p_{2}\neq p_{1}$ to $-$. From this, we can determine, e.g., that the word
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{pop}(1)\in\mathcal{L}$, but
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{pop}(2)\not\in\mathcal{L}$.

${SL}^{\lambda}$ generates $(u,\vec{v})$-trees ${\cal L}[u,\vec{v}]$
representing the language $\mathcal{L}$ to be learned through so-called _tree
queries_ , which perform membership queries for values of the data parameters
$p_{1},\ldots,p_{m}$ that cover relevant equivalence classes of
$\approx_{\mathcal{R}}$.

From the results of tree queries, we can extract registers and guards in the
location reached by a prefix $u$. Intuitively, the registers must remember the
data values of $u$ that occur in some guard in some ${\cal L}[u,\vec{v}]$, and
the outgoing guards from the location reached by $u$ can be derived from the
initial guards in the trees ${\cal L}[u,\vec{v}]$, since the initial guards
represent the constraints that are used when processing the first symbol of
$\vec{v}$. Let $\mathit{mem}_{\vec{v}}(u)$, the set of memorable parameters,
denote the set of registers among $\\{x_{1},\ldots,x_{k}\\}$ that occur on
some $(u,\vec{v})$-path in $Dom({\cal L}[u,\vec{v}])$. Intuitively, if $x_{i}$
is a memorable parameter, then the $i^{th}$ data value in $u$ will be
remembered in the register $x_{i}$ in the location reached by $u$. For
example, for the stack in Fig. 1, in the location reached by
$\mathsf{push}(0)$ the data value $\mathtt{d}_{1}=0$ is memorable so will be
remembered in register $x_{1}$. Note that a $(u,\vec{v})$-tree itself does not
have any registers: it only serves to show which registers are needed in the
location reached by $u$ in the to-be-constructed automaton. Define
$\mathit{mem}_{\mathcal{V}}(u)$ as
$\cup_{\vec{v}\in\mathcal{V}}\mathit{mem}_{\vec{v}}(u)$. For a prefix $u$ and
symbolic suffix $\vec{v}$ whose first action is $\alpha$, let ${\cal
G}_{\\{\vec{v}\\}}(u,\alpha)$ denote the initial guards in the
$(u,\vec{v})$-tree ${\cal L}[u,\vec{v}]$, with $p_{1}$ replaced by $p$. For a
set $\mathcal{V}$, let ${\cal G}_{\mathcal{V}}(u,\alpha)$ denote the set of
satisfiable conjunctions of guards in ${\cal G}_{\\{\vec{v}\\}}(u,\alpha)$ for
$\vec{v}\in\mathcal{V}$ with first action $\alpha$.

Two $(u,\vec{v})$-trees, $T$ and $T^{\prime}$, are _equivalent_ denoted
$T\equiv T^{\prime}$, if $Dom(T)=Dom(T^{\prime})$ and
$T(\tau)=T^{\prime}(\tau)$ for each $\tau\in Dom(T)$. For a mapping $\gamma$
on registers, we define its extension to $(u,\vec{v})$-paths in the natural
way. For a $(u,\vec{v})$-tree $T$, we define $\gamma(T)$ by
$Dom(\gamma(T))=\\{\gamma(\tau)~{}:~{}\tau\in Dom(T)\\}$ and
$\gamma(T)(\gamma(\tau))=T(\tau)$.

Let $u\equiv_{\mathcal{V}}u^{\prime}$ denote that ${\cal
L}[u,\vec{v}]\equiv{\cal L}[u^{\prime},\vec{v}]$, for all symbolic suffixes
$\vec{v}\in\mathcal{V}$. Let $u\simeq_{\mathcal{V}}^{\gamma}u^{\prime}$ denote
that $\gamma$ is a bijection from $\mathit{mem}_{\mathcal{V}}(u)$ to
$\mathit{mem}_{\mathcal{V}}(u^{\prime})$ such that for all
$\vec{v}\in\mathcal{V}$ we have $\gamma({\cal L}[u,\vec{v}])\equiv{\cal
L}[u^{\prime},\vec{v}]$. Let $u\simeq_{\mathcal{V}}u^{\prime}$ denote that
$u\simeq_{\mathcal{V}}^{\gamma}u^{\prime}$ for some bijection $\gamma$.
Intuitively, two words $u$ and $u^{\prime}$ are equivalent if there is a
bijection $\gamma$ which for each $\vec{v}\in\mathcal{V}$ transforms ${\cal
L}[u,\vec{v}]$ to ${\cal L}[u^{\prime},\vec{v}]$, Note that in general, when
$u\simeq_{\mathcal{V}}u^{\prime}$, there can be several such bijections.

Data Structures. During the construction of a hypothesis, the ${SL}^{\lambda}$
algorithm maintains:  (i) a prefix-closed set $S_{p}$ of _short prefixes_ ,
representing locations,  (ii) and a set of one-symbol extensions of the
prefixes in $S_{p}$, representing transitions; we use ${U}$ to represent the
union of $S_{p}$ and this set, and  (iii) a suffix-closed set $\mathcal{V}$ of
symbolic suffixes.  Each one-symbol extension of form $u{\alpha(\mathtt{d})}$
is formed to let $\mathtt{d}$ satisfy a specific guard $g$; we then always
choose $\mathtt{d}$ as a representative data value, denoted
$\mathtt{d}_{u}^{g}$, satisfying $g$ after $u$.

The sets ${U}$ and $\mathcal{V}$ are maintained in a _classification tree_
$CT$, which is designed to represent how the suffixes in $\mathcal{V}$
partition the set ${U}$ into equivalence classes corresponding to locations. A
classification tree is a rooted tree, consisting of nodes connected by edges.
Each inner node is labeled by a symbolic suffix, and each leaf is labeled by a
subset of ${U}$. To each node $N$ is assigned a representative prefix
$\mathit{rp}(N)$ in ${U}$. For a node $N$, let $\mathit{suff}(N)$ its suffix
and $\mathcal{V}(N)$ denote the set of symbolic suffixes of $N$ and all its
ancestors in the tree. Each outgoing edge from $N$ corresponds to an
equivalence class of $\simeq_{\mathcal{V}(N)}$ from which a representative
member is chosen as the representative prefix of its target node. Each leaf
node $N$ is labeled by a set of data words, which are all in the same
equivalence class of $\simeq_{\mathcal{V}(N)}$. Thus, nodes in different
leaves are guaranteed to be inequivalent, since they are separated by the
symbolic suffixes in $\mathcal{V}(\mathit{lca}(N,~{}N^{\prime}))$, where
$\mathit{lca}(N,~{}N^{\prime})$ is the lowest common ancestor node of $N$ and
$N^{\prime}$. We let $\mathcal{U}$ denote the mapping, which maps each prefix
$u\in{U}$ to the classification tree leaf where it is contained. We also let
$\mathcal{V}(u)$ denote $\mathcal{V}(\mathcal{U}(u))$, the suffixes of all
ancestors of $\mathcal{U}(u)$. The representative prefix, $\mathit{rp}(N)$, of
each leaf node $N$ will induce a location in the RA to be constructed.

Function  _$\mathit{Sift}(u,N)$_ is

if  _$N$ is a leaf_ then $\mathcal{U}\leftarrow\mathcal{U}[u\mapsto N]$

else

Compute ${\cal L}[u,\mathit{suff}(N)]$

if  _$N$ has child $N^{\prime}$ with
$u\simeq_{\mathcal{V}(N)}\mathit{rp}(N^{\prime})$_ then
$\mathit{Sift}(u,N^{\prime})$

else

Create new leaf $N^{\prime}$ as child of $N$ with $\mathit{rp}(N^{\prime})=u$

$\mathit{Sift}(u,N^{\prime})$

Function  _Expand( $u$)_ is

$S_{p}\leftarrow S_{p}\cup\\{u\\}$

for  _$\alpha\in\Sigma$_ do
$\mathit{Sift}(u{\alpha(\mathtt{d}_{u}^{g})},\mathit{root}(CT))$ for each
$g\in{\cal G}_{\mathcal{V}(u)}(u,\alpha)$

Function  _Refine( $N$, $\vec{v}$)_ is

Replace $N$ by an inner node $N^{\prime}$ with
$\mathit{suff}(N^{\prime})=\vec{v}$

for  _$u\in\mathcal{U}^{\scalebox{0.3}[1.0]{$-$}1}(N)$_ do
$\mathit{Sift}(u,N^{\prime})$

Algorithm 1 Operations on the Classification Tree.

The insertion of a new prefix $u$ into the classification tree $CT$ is
performed by function $\mathit{Sift}$ (cf. Algorithm 1). It traverses the $CT$
from the root downwards. At each internal node $N$, it checks whether
$u\simeq_{\mathcal{V}(N)}\mathit{rp}(N^{\prime})$ for any child $N^{\prime}$
of $N$. If so, it continues the traversal at $N^{\prime}$, otherwise a new
child of $N$ is created as a leaf $N$ with $\mathit{rp}(N)=u$. When reaching a
leaf $N$, the mapping $\mathcal{U}$ is updated to reflect that $u$ has been
sifted to $N$. In the classification tree in Fig. 4, e.g., $\epsilon$ is the
representative prefix of inner nodes $\mathsf{push}(p_{1})$ and
$\mathsf{push}(p_{2})\mathsf{push}(p_{2})$ as it is the first prefix that was
sifted down this path. The short prefix $\mathsf{push}(0)$ at the second leaf
from right was sifted from the root to $\mathsf{push}(p_{1})$ and then to
$\mathsf{push}(p_{1})\mathsf{push}(p_{2})$ as
$\mathsf{push}(0)\simeq_{\\{\epsilon\\}}\epsilon$ and
$\mathsf{push}(0)\simeq_{\\{\epsilon,~{}\mathsf{push}(p_{1})\\}}\epsilon$.
Since, however, $\mathsf{push}(0)\not\simeq_{\mathcal{V}}\epsilon$ for
$\mathcal{V}=\\{\epsilon,~{}\mathsf{push}(p_{1}),\mathsf{push}(p_{1})\mathsf{push}(p_{2})\\}$,
a new leaf was created and $\mathsf{push}(0)$ was made the representative
prefix of the new leaf and a short prefix.

Initialize $CT$ as inner node $\mathit{root}(CT)$ with suffix $\epsilon$ and
${U}\leftarrow\emptyset$, $S_{p}\leftarrow\emptyset$

$\mathit{Sift}(\epsilon,\mathit{root}(CT))$

HYP: repeat

$\triangleright$ Check closedness

if  _exists leaf $N$ for which $\mathcal{U}^{\scalebox{0.3}[1.0]{$-$}1}(N)\cap
S_{p}=\emptyset$_ then // location

$\mathit{Expand}(u)$ for some $u\in\mathcal{U}^{\scalebox{0.3}[1.0]{$-$}1}(N)$

if  _$u\in S_{p}$ and $g\in{\cal G}_{\mathcal{V}(u)}(u,\alpha)$ but
$u{\alpha(\mathtt{d}_{u}^{g})}\notin{U}$_ then // transition

$\mathit{Sift}(u{\alpha(\mathtt{d}_{u}^{g})},\mathit{root}(CT))$

if  _$u{\alpha(\mathtt{d})}\in{U}$ s.t.
$\mathit{mem}_{\mathcal{V}\\!(\\!u\alpha\\!(\\!\mathtt{d}\\!)\\!)}(u{\alpha(\mathtt{d})})\\!\not\subseteq\\!\mathit{mem}_{\mathcal{V}(u)}(u)\\!\cup\\!\\{x_{|u]\\!+\\!1}\\}\\!$_
then // register

Let $\vec{v}\in\mathcal{V}(u{\alpha(\mathtt{d})})$ with
$\mathit{mem}_{\vec{v}}(u{\alpha(\mathtt{d})}))\not\subseteq(\mathit{mem}_{\mathcal{V}(u)}(u)\cup\\{x_{|u]+1}\\})$

$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$

$\triangleright$ Check consistency

if  _$u,u^{\prime}\in\mathcal{U}^{\scalebox{0.3}[1.0]{$-$}1}(L)\cap S_{p}$
with $u\simeq_{\mathcal{V}(N)}^{\gamma}u^{\prime}$ for leaf $N$ with
$u{\alpha(\mathtt{d}_{u}^{g})},u^{\prime}{\alpha(\mathtt{d}_{u^{\prime}}^{\gamma(g)})}\in{U}$
but
$\mathcal{U}(u{\alpha(\mathtt{d}_{u}^{g})})\neq\mathcal{U}(u^{\prime}{\alpha(\mathtt{d}_{u^{\prime}}^{\gamma(g)})})$
_ then // location

$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$ with
$\vec{v}=\mathit{suff}(\mathit{lca}(u{\alpha(\mathtt{d}_{u}^{g})},~{}u^{\prime}{\alpha(\mathtt{d}_{u^{\prime}}^{\gamma(g)})}))$

if  _$g\in{\cal G}_{\mathcal{V}(u)}(u,\alpha)$ and
$u{\alpha(\mathtt{d}_{u}^{g})},u{\alpha(\mathtt{d})}\in{U}$ with
$(u,\mathtt{d})\vDash g$ but
$\mathcal{U}(u{\alpha(\mathtt{d}_{u}^{g})})\neq\mathcal{U}(u{\alpha(\mathtt{d})})$_
then // transition(a)

$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$ with
$\vec{v}=\mathit{suff}(\mathit{lca}(u{\alpha(\mathtt{d}_{u}^{g})},~{}u{\alpha(\mathtt{d})}))$

if  _$u{\alpha(\mathtt{d}_{u}^{g})},u{\alpha(\mathtt{d})}\in{U}$ with
$u{\alpha(\mathtt{d}_{u}^{g})}\not\simeq_{\mathcal{V}(u{\alpha(\mathtt{d})})}^{\mathbf{id}}u{\alpha(\mathtt{d})}$_
then // transition(b)

$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$ with $\vec{v}$ s.t.
$u{\alpha(\mathtt{d}_{u}^{g})}\not\simeq_{\\{\vec{v}\\}}^{\mathbf{id}}u{\alpha(\mathtt{d})}$

if  _$u,u\alpha\in{U}$ with $u\simeq_{\mathcal{V}(u)}^{\gamma}u$ and no
extension $\gamma^{\prime}$ of $\gamma$ with
$u{\alpha(\mathtt{d})}\simeq_{\mathcal{V}(u{\alpha(\mathtt{d})})}^{\gamma^{\prime}}u{\alpha(\mathtt{d})}$_
then // register

$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$ with $\vec{v}$ s.t.
$u{\alpha(\mathtt{d})}\not\simeq_{\\{\vec{v}\\}}^{\gamma^{\prime}}u{\alpha(\mathtt{d})}$
for any $\gamma^{\prime}$

until  _closed and consistent_

$\mathcal{H}\leftarrow$ Hypothesis($CT$)

if  _$\exists w\in\Sigma^{+}\ s.t.\ \mathcal{H}(w)\neq\mathcal{L}(w)$_ then
$\mathit{Analyze}(w)$ and goto HYP else return $\mathcal{H}$

Algorithm 2 ${SL}^{\lambda}$ Learning.

The ${SL}^{\lambda}$ Algorithm. The core of the ${SL}^{\lambda}$ algorithm,
shown in Algorithm 2, initializes the classification tree to consist of one
(root) inner node, for the empty suffix (which classifies words as accepted or
rejected); ${U}$ and $S_{p}$ are empty. It then sifts the empty prefix
$\epsilon$, thereby entering it into ${U}$. Thereafter, Algorithm 2 repeats a
main loop in which $CT$ is checked for a number of closedness and consistency
properties. Whenever such a property is not satisfied, a corrective update is
made by adding information to $CT$. These corrective updates fall into two
categories, carried out by the following functions:

  * •

$\mathit{Expand}$ takes a prefix $u\in{U}$ and makes it into a short prefix.
Since each short prefix must have a set of one-symbol extensions in ${U}$, the
function forms one-symbol extensions of form $u\alpha(\mathtt{d}_{u}^{g})$,
which are entered into the classification tree by sifting.

  * •

$\mathit{Refine}$ takes a leaf node $N$ and a symbolic suffix $\vec{v}$; it
sifts the prefixes $u$ in $N$, thereby obtaining ${\cal L}[u,\vec{v}]$ from a
tree query. This can either split $N$ into several equivalence classes, refine
the initial guards or extend the set of registers in the location represented
by $N$.

Let us now describe the respective corrective updates in Algorithm 2.

Location Closedness is satisfied if each leaf contains a short prefix in
$S_{p}$. Whenever a leaf $N$ does not contain a short prefix in $S_{p}$, one
of its prefixes $u$ is chosen for inclusion in $S_{p}$ by calling
$\mathit{Expand}(u)$, which adds one-symbol extensions to ${U}$.

Transition Closedness is satisfied if for each short prefix $u$, action
$\alpha$, and initial guard in ${\cal G}_{\mathcal{V}(u)}(u,\alpha)$, the
extension $u{\alpha(\mathtt{d}_{u}^{g})}$ is in ${U}$. If this is not
satisfied, the missing $u{\alpha(\mathtt{d}_{u}^{g})}$ is added to ${U}$ by
sifting into $CT$.

Register Closedness is satisfied if for each pair of prefixes $u$ and
$u\alpha(\mathtt{d})$ in ${U}$, the memorable parameters found for $u$ contain
the memorable parameters revealed by the suffixes for $u\alpha(\mathtt{d})$,
except for $x_{|u]+1}$, where $|u]$ is the length of $u$. Register closedness
guarantees that in a hypothesis $\mathcal{H}$, values of registers in the
location of $u\alpha(\mathtt{d})$ can all be obtained by assignment from the
registers in location $u$ and the just received parameter. If it is not
satisfied, a suffix $\vec{v}$ for $u\alpha(\mathtt{d})$ which reveals a
missing register is prepended by $\alpha(p_{1})$ and added to the suffixes for
$u$, whereafter $\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$ will
reveal the missing parameter. Here, and in the following, we use
$\vec{\alpha}$ to denote $\alpha(p_{1})$, and $\vec{\alpha}\vec{v}$ to denote
the result
$\alpha(p_{1})\alpha_{2}^{\prime}(p_{2})\ldots\alpha_{m+1}^{\prime}(p_{m+1})$
of prepending $\vec{\alpha}$ to
$\vec{v}=\alpha_{1}^{\prime}(p_{1})\ldots\alpha_{m}^{\prime}(p_{m})$. If
possible, we try to choose a shortest $\vec{v}$, and also restrict the
parameters of $\vec{\alpha}\vec{v}$ to reduce the cost of the tree query for
${\cal L}[u,\vec{\alpha}\vec{v}]$.

Location Consistency. Analogously to consistency in the classic $L^{*}$
algorithm, we split a leaf containing two short prefixes $u$, $u^{\prime}$, in
case their corresponding extensions are not equivalent, i.e., there is a
$g\in{\cal G}_{\mathcal{V}(u)}(u,\alpha)$ such that
$\mathcal{U}(u\alpha(\mathtt{d}_{u}^{g}))\neq\mathcal{U}(u^{\prime}\alpha(\mathtt{d}_{u^{\prime}}^{\gamma(g)}))$.
The splitting is done by calling
$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$, where $\vec{v}$ is the
symbolic suffix labeling the common ancestor of the leaves of
$u\alpha(\mathtt{d}_{u}^{g})$ and
$u^{\prime}\alpha(\mathtt{d}_{u^{\prime}}^{\gamma(g)})$.

Transition Consistency is satisfied if all one-symbol extensions
$u\alpha(\mathtt{d})$ that satisfy some guard $g$ in ${\cal
G}_{\mathcal{V}(u)}(u,\alpha)$, are sifted to the same leaf as the extension
$u\alpha(\mathtt{d}_{u}^{g})$ with the representative data value
$\mathtt{d}_{u}^{g}$. If not, the guard $g$ should be split by calling
$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$, where $\vec{v}$ is the
symbolic suffix labeling the common ancestor of the leaves of
$u\alpha(\mathtt{d}_{u}^{g})$ and $u\alpha(\mathtt{d})$. A similar case
(Transition Consistency(b)) occurs when $u\alpha(\mathtt{d}_{u}^{g})$ and
$u\alpha(\mathtt{d})$ are sifted to the same leaf, but are not equivalent
under the identity mapping between registers. Also here, the guard $g$ should
be split by calling $\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$,
where $\vec{v}$ is a shortest suffix under which
$u\alpha(\mathtt{d}_{u}^{g})\not\simeq_{\\{\vec{v}\\}}^{\mathbf{id}}u\alpha(\mathtt{d})$.

Register Consistency. For some short prefix $u$ with memorable values
$\mathit{mem}_{\mathcal{V}(u)}(u)$, there may be symmetries in ${\cal
L}[u,\vec{v}]$ for some $\vec{v}\in\mathcal{V}(u)$, i.e., for some permutation
$\gamma$ on $\mathit{mem}_{\mathcal{V}(u)}(u)$ we have
$u\simeq_{\mathcal{V}(u)}^{\gamma}u$. It may be that this symmetry does not
exist in the SUL, but we did not yet add a suffix that disproves it (cf.
example in Appendix 0.A) Register consistency checks for the existence of such
suffixes by comparing symmetries in $u$ and its continuations
$u{\alpha(\mathtt{d})}$. If a symmetry between data values of $u$ does not
exist in $u\alpha$ while one or more of the data values are memorable in
$u\alpha$, we can construct a suffix that breaks the symmetry also for $u$.

Restricted Symbolic Suffixes. To reduce the number of membership queries for
tree queries of form ${\cal L}[u,\vec{v}]$, we impose, when possible,
restrictions to the parameters of $\vec{v}$, meaning that ${\cal
L}[u,\vec{v}]$ represents acceptance/rejection of $u\vec{v}$ _only for the
suffix parameters that satisfy the imposed restrictions_. An illustration was
given at the end of Section 2. A more detailed description is in Appendix 0.B.
Since a restricted symbolic suffix $\vec{v}^{\prime}$ represents fewer actual
suffixes than an unrestricted one $\vec{v}$, it has less separating power, so
suffixes should only be restricted if their separating power is sufficient.
The principles for adding restrictions are specific to the theory; we have
implemented them for the theory $\langle\mathbb{N},\\{=\\}\rangle$. There, we
consider two forms of restrictions on suffix parameters $p_{i}$:  (i)
$\mathit{fresh}(p_{i})$, meaning that $p_{i}$ is different from all other
preceding parameters in the prefix and suffix,  (ii) $p_{i}=p_{j}$, where
$j<i$, i.e., $p_{j}$ is an earlier parameter in the restricted suffix.  Let us
consider how restricted suffixes arise when prepending an action
$\vec{\alpha}$ to an existing suffix $\vec{v}$, in a call of form
$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$, in the case that $u$,
$\vec{\alpha}$, and $\vec{v}$ are chosen such that
$\mathit{mem}_{\vec{v}}(u{\alpha(\mathtt{d})}))$ contains a particular
memorable parameter. Let us denote the parameters of $\vec{\alpha}\vec{v}$ by
$p_{1},\cdots,p_{|\vec{v}|+1}$. The restriction of suffix
$\vec{\alpha}\vec{v}$ is then obtained by

  1. 1.

letting the parameter of $\vec{\alpha}$ be fresh if $\mathtt{d}$ is not equal
to a previous data value in $u$, and

  2. 2.

restricting each parameter $p_{i}$ with $i>1$ in $\vec{\alpha}\vec{v}$ to be
(i) fresh whenever $p_{i-1}$ is fresh in $\vec{v}$ or the branch taken in
${\cal L}[u{\alpha(\mathtt{d})},\vec{v}]$ for fresh $p_{i-1}$ reveals the
sought register, and  (ii) equal to a previous value $p_{j}$ in
$\vec{\alpha}\vec{v}$ if the branch taken in ${\cal
L}[u{\alpha(\mathtt{d})},\vec{v}]$ for $p_{i-1}$ equal to the corresponding
value reveals the sought register.

Hypothesis Construction. We can construct a hypothesis from a closed and
consistent classification tree. Location closedness ensures that every
transition has a defined source and target location, transition closedness
ensures that every transition that is observed by the tree queries we have
performed so far, is represented by a prefix, and register closedness ensures
that registers exist for all memorable data values in corresponding locations.
Location consistency, transition consistency, and register consistency ensure
that we can construct a unique (up to naming of locations and registers)
determinate register automaton eventhough there may exist multiple short
prefixes for one location and symmetries betweeen memorable data values.

We construct the register automaton
$\mathcal{A}=(L,l_{0},\mathcal{X},\Gamma,\lambda)$, where

  * •

$L$ is the set of leaves of $CT$, and $l_{0}$ is the leaf containing the empty
prefix $\epsilon$,

  * •

$\mathcal{X}$ maps each location $l\in L$ to $\mathit{mem}_{CT}(u)$, where $u$
is the representative short prefix of the leaf corresponding to $l$, and

  * •

$\lambda(l)=+$ if the leaf $l$ is in the accepting subtree of the root, else
$\lambda(l)=-$.

  * •

for every location $l$ with short prefix $u$, action $\alpha$, and guard $g$
in ${\cal G}_{\mathcal{V}(u)}(u,\alpha)$, there is a transition $\langle
l,\alpha(p),g,\pi,l^{\prime}\rangle$, where

    * –

$l^{\prime}=\mathcal{U}(u{\alpha(\mathtt{d}_{u}^{g})})$ is the target
location, and

    * –

$\pi$ (the assignment) is defined by $\gamma$ for which
$u{\alpha(\mathtt{d}_{u}^{g})}\simeq_{\mathcal{V}(u{\alpha(\mathtt{d}_{u}^{g})})}^{\gamma}\mathit{rp}(u{\alpha(\mathtt{d}_{u}^{g})})$

Function  _Analyze( $w$)_ is

for  _$|w|\geq i >0$_ do

for  _$u\in As(w_{1:i-1})$_ do

Let $u{\alpha(\mathtt{d}_{u}^{g})}\in{U}$ represent the last transition of
$w_{1:i}$ in $\mathcal{H}$

Let $\vec{v}=Acts(w_{i+1:|w|})$ (or $\epsilon$ for $i=|w|$)

if  _$u{\alpha(\mathtt{d}_{u}^{g})}\not\simeq_{\\{\vec{v}\\}}{u^{\prime}}$ for
all $u^{\prime}\in As(w_{1:i})$_ then // location

$\mathit{Expand}(u{\alpha(\mathtt{d}_{u}^{g})})$ and stop analysis of $w$

if  _initial guard $g$ in $\mathcal{L}({u},{\vec{\alpha}\vec{v}})$ but no
$u{\alpha(\mathtt{d}_{u}^{g})}\in{U}$_ then // transition

$\mathit{Sift}(u{\alpha(\mathtt{d}_{u}^{g})},\mathit{root}(CT))$ and stop
analysis of $w$

Algorithm 3 Analyze Counterexample.

Analysis of Counterexamples. When an equivalence query returns a
counterexample $w$, we process the counterexample as is shown in Algorithm 3.
From right to left, we split the counterexample at every index into a location
prefix $w_{1:i-1}$, a transition prefix $w_{1:i}$, and a suffix $w_{i+1:|w|}$.
We use the location and transition prefixes to find corresponding short
prefixes $u$ and prefixes $u{\alpha(\mathtt{d}_{u}^{g})}$ by tracing
$w_{1:i-1}$ and $w_{1:i}$ on the hypothesis. We write $As(w_{1:i})$ for the
short prefix corresponding to the location reached by $w_{1:i}$ in a
hypothesis and $Vals(w)$ for the sequence of actions of $w$. We can then
distinguish two cases: (1) The word $u{\alpha(\mathtt{d}_{u}^{g})}$ is
inequivalent to all corresponding short prefixes for the suffix of the
counterexample. In this case, we make $u{\alpha(\mathtt{d}_{u}^{g})}$ a short
prefix. (2) The tree query $\mathcal{L}({u},{\vec{\alpha}\vec{v}})$ shows a
new initial guard. In this case, we add the corresponding (new) prefix
$u{\alpha(\mathtt{d}_{u}^{g})}$ to the set of prefixes. If neither case
applies, we continue with the next index. Since $w$ is a counterexample, one
of the cases will apply for some index (cf. Lemma 1).

##  5 Correctness and Complexity

Let us now briefly discuss the correctness and query complexity of
${SL}^{\lambda}$. The correctness arguments are analogous to the arguments
presented for other active learning algorithms. One notable difference to
${SL}^{*}$ is that ${SL}^{\lambda}$ establishes register consistency instead
of relying on counterexamples for distinguishing symmetric registers. Proofs
and a more detailed discussionan be found in Appendix 0.C.

###### Lemma 1

A counterexample leads to a new short prefix or to a new prefix.

This is a direct consequence of Algorithm 3. Using a standard construction
that leverages properties of counterexamples (cf. [39, 10]), it can be shown
that one of the two cases in the algorithm will trigger for some index of the
counterexample. As long as expanding (or sifting) new prefixes does not
trigger a refinement, the current counterexample can be analyzed again, until
a refinement occurs.

Lemma 1 establishes progress towards a finite RA for a language $\mathcal{L}$.
Let $m$ be the length of the longest counterexample, $t$ the number of
transitions, $r$ the maximal number of registers at any location, and $n$ the
number of locations in the final model. ($t$ dominates both $n$ and $r$.)

###### Theorem 5.1

${SL}^{\lambda}$ infers a RA for regular data language $\mathcal{L}$ with
$O(t)$ equivalence queries and $O(t^{2}\,n^{r}+tmn\,m^{m})$ membership queries
for sifting words and analyzing counterexamples.

$O(t)$ is an improvement over the worst case estimate of $O(tr)$ equivalence
queries for ${SL}^{*}$ [10]. ${SL}^{\lambda}$ also improves the worst case
estimate for membership queries for sifting to $O(t^{2}\,n^{r})$ from
$O(t^{2}r\,n^{r}$) for filling the table in ${SL}^{*}$. For analyzing
counterexamples, ${SL}^{\lambda}$ replaces $O(trm\,m^{m})$ with
$O(tmn\,m^{m})$.

##  6 Evaluation

As mentioned, we have implemented the ${SL}^{\lambda}$ algorithm in the
publicly available RALib tool for learning register automata. RALib already
implemented the ${SL}^{*}$ algorithm [10] that uses an observation table as
its data structure. In order to evaluate the effect of analyzing
counterexamples as described in Section 4, we have also implemented the
${SL}^{CT}$ classification tree learning algorithm that uses the same
counterexample analysis technique as the ${SL}^{*}$ algorithm, i.e., adding
suffixes from counterexamples to the classification tree directly. We compare
the performance of the ${SL}^{\lambda}$ algorithm against that of ${SL}^{*}$
and ${SL}^{CT}$. All models, the experimental setup, and infrastructure for
executing the experiments are available on the paper’s artefact at Zenodo [41]
and updated versions on GitHub222https://github.com/LearnLib/ralib-
benchmarking.

Experimental Setup. We use two series of experiments: (1) A black-box learning
setup with random walks for finding counterexamples on small models from the
Automata Wiki [38] to establish a baseline comparison with other results and
to evaluate the impact of using non-minimal counterexamples. In these
experiments, we verify with a model checker that the inferred model is
equivalent to the SUL and we stop as soon as the correct model is produced by
a learning algorithm. (2) A white-box setup with a model checker for finding
short counterexamples to analyze the scalability of algorithms on (2a) $24$
consecutive hypotheses of the Mbed TLS 2.26.0 server,333We obtained these
hypotheses by extending the machinery of DTLS-Fuzzer [16], a publicly
available tool for learning state machine models of DTLS implementations. as
well as (2b) sets of randomly generated automata.444We used the algorithm of
Champarnaud and Paranthoën [11] to enumerate semantically distinct DFAs with a
specific alphabet and number of locations. We then replaced the alphabet
symbols with RA actions of arity one, and finally replaced a fraction of the
transitions with simple gadgets that store and compare data values. All
results were obtained on a MacBook Pro with an Apple M1 Pro CPU and $32$ GB of
memory, running macOS version $12.5.1$ and OpenJDK version $17.0.8.1$.

Table 1: Results on AutomataWiki Systems.

SUL | Resets (Learn) | Resets (Total) | CounterExs | WCT Learn [ms] | WCT Test [ms]
---|---|---|---|---|---
| $|Q|$ | $|\Gamma|$ | $|X|$ | $|C|$ | ${SL}^{*}$ | ${SL}^{\lambda}$ | ${SL}^{CT}$ | ${SL}^{*}$ | ${SL}^{\lambda}$ | ${SL}^{CT}$ | ${SL}^{*}$ | ${SL}^{\lambda}$ | ${SL}^{CT}$ | ${SL}^{*}$ | ${SL}^{\lambda}$ | ${SL}^{CT}$ | ${SL}^{*}$ | ${SL}^{\lambda}$ | ${SL}^{CT}$
channel-frame | 5 | 8 | 3 | 2 | 11 | 11 | 15 | 24 | 28 | 32 | 1 | 2 | 2 | 49 | 43 | 36 | 295 | 289 | 294
abp-receiver3 | 6 | 10 | 3 | 2 | 489 | 88 | 466 | 614 | 249 | 610 | 4 | 4 | 4 | 147 | 74 | 245 | 256 | 282 | 264
palindrome | 6 | 15 | 4 | 0 | 479 | 358 | 476 | 508 | 384 | 504 | 5 | 5 | 5 | 73 | 52 | 51 | 406 | 403 | 402
login | 12 | 19 | 4 | 0 | 436 | 244 | 433 | 509 | 300 | 512 | 3 | 2 | 3 | 86 | 54 | 67 | 301 | 303 | 310
abp-output | 30 | 50 | 1 | 2 | 363 | 208 | 311 | 590 | 4 552 | 6 151 | 5 | 11 | 11 | 142 | 151 | 696 | 260 | 175 | 154
sip | 30 | 72 | 2 | 0 | 487 | 233 | 345 | 934 | 3 633 | 2 772 | 9 | 15 | 16 | 370 | 347 | 353 | 194 | 149 | 160
fifo3 | 12 | 16 | 4 | 0 | 29 | 24 | 23 | 212 | 202 | 209 | 5 | 5 | 5 | 114 | 106 | 108 | 547 | 636 | 563
fifo5 | 18 | 24 | 6 | 0 | 66 | 55 | 60 | 435 | 434 | 468 | 6 | 7 | 7 | 1 303 | 1 144 | 1 451 | 575 | 600 | 584
fifo7 | 24 | 32 | 8 | 0 | 118 | 96 | 123 | 738 | 839 | 989 | 7 | 8 | 9 | 317 435 | 279 888 | 346 897 | 589 | 591 | 583

Results. Table 1 summarizes the results of the experiments in a black-box
learning setup. For every SUL, we report its complexity (in number of
locations $|Q|$, transitions $|\Gamma|$, registers $|X|$, and constants $|C|$)
and, for each learning algorithm, the number of resets (i.e., tests) during
the learning phase, total tests (incl. counterexample search), the number of
counterexamples found, and wall clock times (WCT) for learning and testing. In
Table 1, all numbers are averages from $20$ experiments. It can be seen that
the ${SL}^{\lambda}$ algorithm consistently outperforms the other two
algorithms w.r.t. the number of tests during learning. As can be expected, the
${SL}^{*}$ algorithm requires the fewest counterexamples. Execution times do
not show a consistent pattern for these small systems or a clear ‘winner’
between these three RA learning algorithms, but there is a strong correlation
between the number of learner tests and the time that learning requires. Due
to this, in most cases, ${SL}^{\lambda}$ is fastest overall.

The SULs of the previous set of experiments were all quite small
($|\Gamma|\leq 72$), and did not show any scalability differences between the
three algorithms. Also, with the exception of fifo, the benchmarks were not
parametric. In the following experiments, we scale the SULs which are learned.

Figure 5 shows the results of our experiments with DTLS models. For each
algorithm, the graphs show the relationship between the number of transitions
in each hypothesis model and the number of resets with restricted and
unrestricted suffixes (in the first two graphs), the number of counterexamples
($3^{rd}$ graph), and execution times ($4^{th}$ graph). It is evident that,
with increasing model complexity, the number of counterexamples grows linearly
for all algorithms at roughly the same rate, yet the number of resets grows
much more rapidly for ${SL}^{*}$ than it does for ${SL}^{CT}$ and
${SL}^{\lambda}$. In terms of time performance, the trend is even more
pronounced. For SULs with more that $100$ transitions, learning times grow
significantly worse for ${SL}^{*}$ than the other two algorithms, and
${SL}^{\lambda}$ clearly also beats ${SL}^{CT}$ on even bigger systems.

(a)  (b)  (c)  (d)

Figure 5: Number of resets (two leftmost graphs), counterexamples ($3^{rd}$
graph), and wall clock times ($4^{th}$ graph) for inferring models of the Mbed
TLS 2.26.0 server.

(a)  (b)  (c)

Figure 6: Resets for inferring models of generated SULs, scaling the number of
transitions through locations and actions as well as by increasing the
percentage of transitions with data operations using restricted and
unrestricted suffixes.

Finally, Fig. 6 shows the results of the experiments with randomly generated
automata. The graphs show how the number of resets scales with the number of
locations and actions (left) and the number of registers when using both
restricted (center) and unrestricted suffixes (right). The number of resets
grows much more rapidly for ${SL}^{*}$ than for the other algorithms. Not
restricting suffixes leads to a 2–4x increase in resets; notice the different
scales on the y-axis.

Overall, the experiments show a clear advantage of ${SL}^{\lambda}$ over
table-based RA learning algorithms in terms of the number of resets and
execution times for bigger systems. These results confirm the theoretical
properties of the algorithms and are consistent with the behavior of AAL
algorithms for FSMs.

##  7 Conclusion

We have presented ${SL}^{\lambda}$, a scalable tree-based algorithm for
register automata learning. ${SL}^{\lambda}$ reduces the membership queries
needed for inferring RA models by constructing short restricted suffixes
incrementally. This enables active learning in scenarios not feasible with
previous algorithms. We prove a reduction in the worst-case number of tests
and, via a practical evaluation, show performance improvements on both real-
world (i.e., on a complex network protocol) and synthetic models compared to
the state-of-the-art RA learning algorithm.

### Acknowledgements

This research was partially funded by the Swedish Research Council
(Vetenskapsrådet), the Swedish Foundation for Strategic Research through
project aSSIsT, the Knut and Alice Wallenberg Foundation through project
UPDATE, and the Deutsche Forschungsgemeinschaft (DFG, German Research
Foundation) projects 495857894 (STING) and 442146713 (NFDI4Ing).

## References

  * [1] Aarts, F., Jonsson, B., Uijen, J., Vaandrager, F.: Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods in System Design pp. 1–41 (2015). https://doi.org/10.1007/s10703-014-0216-x
  * [2] Aarts, F., Fiterau-Brostean, P., Kuppens, H., Vaandrager, F.: Learning register automata with fresh value generation. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) Theoretical Aspects of Computing - ICTAC 2015. LNCS, vol. 9399, pp. 165–183. Springer International Publishing, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_11
  * [3] Aarts, F., Heidarian, F., Kuppens, H., Olsen, P., Vaandrager, F.: Automata learning through counterexample guided abstraction refinement. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012: Formal Methods. LNCS, vol. 7436, pp. 10–27. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_4
  * [4] Aarts, F., Jonsson, B., Uijen, J., Vaandrager, F.: Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods in System Design 46(1), 1–41 (Feb 2015). https://doi.org/10.1007/s10703-014-0216-x
  * [5] Aarts, F., Kuppens, H., Tretmans, J., Vaandrager, F.W., Verwer, S.: Learning and testing the bounded retransmission protocol. In: Proceedings of the Eleventh International Conference on Grammatical Inference, ICGI 2012. JMLR Proceedings, vol. 21, pp. 4–18. JMLR.org (2012), http://proceedings.mlr.press/v21/aarts12a.html
  * [6] Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. In: Proc. $29^{th}$ ACM Symp. on Principles of Programming Languages. pp. 4–16. ACM (2002). https://doi.org/10.1145/503272.503275
  * [7] 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
  * [8] Bollig, B., Habermehl, P., Leucker, M., Monmege, B.: A fresh approach to learning register automata. In: Developments in Language Theory. LNCS, vol. 7907, pp. 118–130. Springer Verlag (2013). https://doi.org/10.1007/978-3-642-38771-5_12
  * [9] Cassel, S., Howar, F., Jonsson, B.: RALib: a LearnLib extension for inferring EFSMs. In: Proceedings of the 4th International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS). pp. 1–8 (2015), https://www.faculty.ece.vt.edu/chaowang/difts2015/papers/paper˙5.pdf
  * [10] Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. Formal Asp. Comput. 28(2), 233–263 (2016). https://doi.org/10.1007/s00165-016-0355-5
  * [11] Champarnaud, J.M., Paranthoën, T.: Random generation of DFAs. Theoretical Computer Science 330(2), 221–235 (Feb 2005). https://doi.org/10.1016/j.tcs.2004.03.072
  * [12] Drews, S., D’Antoni, L.: Learning symbolic automata. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 10205, pp. 173–189. Springer, Berlin, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_10
  * [13] Esparza, J., Leucker, M., Schlund, M.: Learning workflow Petri nets. Fundamenta Informaticae 113(3-4), 205–228 (2011). https://doi.org/10.3233/FI-2011-607
  * [14] Ferreira, T., Brewton, H., D’Antoni, L., Silva, A.: Prognosis: Closed-box analysis of network protocol implementations. In: ACM SIGCOMM 2021 Conference. pp. 762–774. ACM (Aug 2021). https://doi.org/10.1145/3452296.3472938
  * [15] Fiterau-Brostean, P., Howar, F.: Learning-based testing the sliding window behavior of TCP implementations. In: Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems - and - 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS. LNCS, vol. 10471, pp. 185–200. Springer (2017). https://doi.org/10.1007/978-3-319-67113-0_12
  * [16] Fiterau-Brostean, P., Jonsson, B., Sagonas, K., Tåquist, F.: DTLS-Fuzzer: A DTLS protocol state fuzzer. In: 15th IEEE Conference on Software Testing, Verification and Validation. pp. 456–458. ICST 2022, IEEE (Apr 2022). https://doi.org/10.1109/ICST53961.2022.00051
  * [17] Fiterau-Brostean, P., Jonsson, B., Sagonas, K., Tåquist, F.: Automata-based automated detection of state machine bugs in protocol implementations. In: Network and Distributed System Security Symposium. NDSS 2023, The Internet Society (Feb 2023), https://www.ndss-symposium.org/wp-content/uploads/2023/02/ndss2023˙s68˙paper.pdf
  * [18] Fiterău-Broştean, P., Jonsson, B., Merget, R., de Ruiter, J., Sagonas, K., Somorovsky, J.: Analysis of DTLS implementations using protocol state fuzzing. In: 29th USENIX Security Symposium (USENIX Security 20). pp. 2523–2540. USENIX Association (Aug 2020), https://www.usenix.org/conference/usenixsecurity20/presentation/fiterau-brostean
  * [19] Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. LNCS, vol. 9780, pp. 454–471. Springer International Publishing, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_25
  * [20] Fiterău-Broştean, P., Lenaerts, T., Poll, E., de Ruiter, J., Vaandrager, F., Verleg, P.: Model learning and model checking of SSH implementations. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software. pp. 142–151. Association for Computing Machinery, New York, NY, USA (Jul 2017). https://doi.org/10.1145/3092282.3092289
  * [21] Frohme, M., Steffen, B.: Compositional learning of mutually recursive procedural systems. International Journal on Software Tools for Technology Transfer 23(4), 521–543 (Aug 2021). https://doi.org/10.1007/s10009-021-00634-y
  * [22] Frohme, M., Steffen, B.: Never-stop context-free learning. In: Olderog, E.R., Steffen, B., Yi, W. (eds.) Model Checking, Synthesis, and Learning, LNCS, vol. 13030, pp. 164–185. Springer International Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-91384-7_9
  * [23] Garg, P., Löding, C., Madhusudan, P., Neider, D.: Learning universally quantified invariants of linear data structures. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. LNCS, vol. 8044, pp. 813–829. Springer, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_57
  * [24] Groz, R., Irfan, M.N., Oriat, C.: Algorithmic improvements on regular inference of software models and perspectives for security testing. In: Proc. ISoLA 2012, Part I. LNCS, vol. 7609, pp. 444–457. Springer (2012). https://doi.org/10.1007/978-3-642-34026-0_41
  * [25] Hagerer, A., Hungar, H., Niese, O., Steffen, B.: Model generation by moderated regular extrapolation. In: Kutsche, R.D., Weber, H. (eds.) Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002\. LNCS, vol. 2306, pp. 80–95. Springer Verlag (Apr 2002). https://doi.org/10.1007/3-540-45923-5_6
  * [26] de la Higuera, C.: A bibliographical study of grammatical inference. Pattern Recognition 38(9), 1332–1348 (Sep 2005). https://doi.org/10.1016/j.patcog.2005.01.003
  * [27] Howar, F., Steffen, B.: Active automata learning in practice. In: Bennaceur, A., Hähnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits, LNCS, vol. 11026, pp. 123–148. Springer International Publishing, Cham (2018). https://doi.org/10.1007/978-3-319-96562-8_5
  * [28] Howar, F., Steffen, B.: Active automata learning as black-box search and lazy partition refinement. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds.) A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. LNCS, vol. 13560, pp. 321–338. Springer (2022). https://doi.org/10.1007/978-3-031-15629-8_17
  * [29] Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 7148, pp. 251–266. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_17
  * [30] Hungar, H., Niese, O., Steffen, B.: Domain-specific optimization in automata learning. In: Computer Aided Verification, 15th International Conference. LNCS, vol. 2725, pp. 315–327 (Jul 2003). https://doi.org/10.1007/978-3-540-45069-6_31
  * [31] Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: A redundancy-free approach to active automata learning. In: Runtime Verification: 5th International Conference, RV 2014, Proceedings. LNCS, vol. 8734, pp. 307–322. Springer (Sep 2014). https://doi.org/10.1007/978-3-319-11164-3_26
  * [32] Kearns, M., Vazirani, U.: An Introduction to Computational Learning Theory. MIT Press (1994)
  * [33] Linard, A., de la Higuera, C., Vaandrager, F.: Learning unions of $k$-testable languages. In: Martín-Vide, C., Okhotin, A., Shapira, D. (eds.) Language and Automata Theory and Applications. LNCS, vol. 11417, pp. 328–339. Springer International Publishing, Cham (2019). https://doi.org/10.1007/978-3-030-13435-8_24
  * [34] Maler, O., Mens, I.E.: Learning regular languages over large alphabets. In: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference,. LNCS, vol. 8413, pp. 485–499. Springer (2014). https://doi.org/10.1007/978-3-642-54862-8_41
  * [35] Margaria, T., Niese, O., Raffelt, H., Steffen, B.: Efficient test-based model generation for legacy reactive systems. In: Proceedings of the Ninth IEEE International High-Level Design Validation and Test Workshop. pp. 95–100. IEEE, New York, NY, USA (Nov 2004). https://doi.org/10.1109/HLDVT.2004.1431246
  * [36] Merten, M., Howar, F., Steffen, B., Cassel, S., Jonsson, B.: Demonstrating learning of register automata. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 7214, pp. 466–471. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_32
  * [37] Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: Proc. $44^{th}$ ACM Symp. on Principles of Programming Languages. pp. 613–625. POPL ’17, ACM, New York, NY, USA (Jan 2017). https://doi.org/10.1145/3093333.3009879
  * [38] Neider, D., Smetsers, R., Vaandrager, F.W., Kuppens, H.: Benchmarks for automata learning and conformance testing. In: Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday. LNCS, vol. 11200, pp. 390–416. Springer (2018). https://doi.org/10.1007/978-3-030-22348-9_23
  * [39] Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993). https://doi.org/10.1006/inco.1993.1021
  * [40] de Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: 24th USENIX Security Symposium (USENIX Security 15). pp. 193–206. USENIX Association (Aug 2015), https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter
  * [41] Sagonas, K., Jonsson, B., Howar, F., Dierl, S., Fiterau-Brostean, P., Tåquist, F.: Reproduction artifact for TACAS 2024 paper “Scalable tree-based register automata learning” (Dec 2023). https://doi.org/10.5281/zenodo.10442556
  * [42] Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: An industrial experience report. In: Ábrahám, E., Huisman, M. (eds.) Integrated Formal Methods. LNCS, vol. 9681, pp. 311–325. Springer International Publishing, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_20
  * [43] Shahbaz, M., Groz, R.: Analysis and testing of black-box component-based systems by inferring partial models. Software Testing, Verification and Reliability 24(4), 253–288 (2014). https://doi.org/10.1002/stvr.1491
  * [44] Shu, G., Lee, D.: Testing security properties of protocol implementations - a machine learning based approach. In: 27th IEEE International Conference on Distributed Computing Systems (ICDCS 2007). IEEE Computer Society (2007). https://doi.org/10.1109/ICDCS.2007.147
  * [45] Sun, J., Xiao, H., Liu, Y., Lin, S.W., Qin, S.: TLV: abstraction through testing, learning, and validation. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering. pp. 698–709. Association for Computing Machinery, New York, NY, USA (Aug 2015). https://doi.org/10.1145/2786805.2786817
  * [46] Tappler, M., Aichernig, B.K., Bloem, R.: Model-based testing IoT communication via active automata learning. In: IEEE International Conference on Software Testing, Verification and Validation. pp. 276–287. IEEE Computer Society (Mar 2017). https://doi.org/10.1109/ICST.2017.32
  * [47] Vaandrager, F., Bloem, R., Ebrahimi, M.: Learning Mealy machines with one timer. In: Leporati, A., Martín-Vide, C., Shapira, D., Zandron, C. (eds.) Language and Automata Theory and Applications. LNCS, vol. 12638, pp. 157–170. Springer International Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-68195-1_13
  * [48] Vaandrager, F., Garhewal, B., Rot, J., Wißmann, T.: A new approach for active automata learning based on apartness. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 13243, pp. 223–243. Springer International Publishing, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_12
  * [49] Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86–95 (Jan 2017). https://doi.org/10.1145/2967606
  * [50] Volpato, M., Tretmans, J.: Active learning of nondeterministic systems from an ioco perspective. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. LNCS, vol. 8802, pp. 220–235. Springer, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45234-9_16
  * [51] Walkinshaw, N., Bogdanov, K., Derrick, J., París, J.: Increasing functional coverage by inductive testing: A case study. In: Testing Software and Systems - 22nd IFIP WG 6.1 International Conference, ICTSS 2010. LNCS, vol. 6435, pp. 126–141. Springer (2010). https://doi.org/10.1007/978-3-642-16573-3_10
  * [52] Yonesaki, N., Katayama, T.: Functional specification of synchronized processes based on modal logic. In: Proceedings of the 6th Int. Conference on Software Engineering. pp. 208–217. IEEE Computer Society Press (1982). https://doi.org/10.5555/800254.807763

##  Appendix 0.A Example: Symmetries in an SDT

$l_{0}$$l_{1}$$l_{2}$$l_{3}$$\frac{\alpha(p)~{}|~{}true}{x_{1}:=p}$$\frac{\alpha(p)~{}|~{}true}{x_{2}:=p}$$\frac{\beta(p)~{}|~{}x_{1}=p}{-}$$\frac{\beta(p)~{}|~{}x_{1}\neq
p}{x_{1}:=p;x_{2}:=x_{1}}$$\frac{\alpha(p)~{}|~{}x_{1}=p}{-}$$\frac{\alpha(p)~{}|~{}x_{2}=p}{-}$$\frac{\beta(p)~{}|~{}true}{x_{1}:=x_{2}}$

$\epsilon$$\alpha(p)$$\beta(p)$$\alpha(n)\beta(n)$$\underline{\epsilon}$$\underline{\beta(1)}$…$\underline{\alpha(1)}$
sym: $\\{(1)\\}$ $\alpha(1)\alpha(2)\beta(3)$ $\underline{\alpha(1)\alpha(2)}$
sym: $\\{(12)\\}$$\alpha(1)\beta(2)$
$\underline{\alpha(1)\alpha(2)\alpha(1)}$$\alpha(1)\alpha(2)\alpha(2)$$\alpha(1)\beta(1)$
{$x_{12}$}$x_{1}=p$$x_{2}=p$$else${$x_{12}$}$x_{1}=p$$else$

Figure 7: SUL (left) and Classification Tree (right) illustrating symmetry.

The classification tree in Fig. 7 (right) represents all locations and
transitions of the RA (left). For the words in leaf $\alpha(1)\alpha(2)$ there
are symmetries that could lead to an incorrect remapping. The symmetry is not
in the RA. A check for register consistency finds information to break it: in
word $\alpha(1)\alpha(2)\beta(3)$ only $2$ is memorable. This is a _register
inconsistency_ and can be resolved by refining the leaf of
$\alpha(1)\alpha(2)$ by restricted suffix $\beta(n)\beta(p)$.

##  Appendix 0.B Imposing Restrictions on Symbolic Suffixes

As described in Section 2, a tree query for a prefix $u$ and symbolic suffix
$\vec{v}$ can be realized by a bounded number of membership queries for
selected values of the data parameters of $\vec{v}$. The number of these
values can grow exponentially in the length of $\vec{v}$. In order to reduce
this number, we impose additional restrictions on the parameters of symbolic
suffixes. We consider two forms of restrictions on suffix parameters $p_{i}$:
(i) $\mathit{fresh}(p_{i})$, meaning that $p_{i}$ is different from all other
preceding parameters in the prefix and suffix,  (ii) $p_{i}=p_{j}$, where
$j<i$, i.e., $p_{j}$ is an earlier parameter in the suffix.  How these
restrictions are added to a symbolic suffix $\vec{v}$ differs depending on the
context. During analysis of counterexamples, symbolic suffixes are formed from
concrete prefixes and suffixes, so a direct comparison can be made between
parameters in the prefix and suffix. When adding a symbolic suffix
$\vec{\alpha}\vec{v}$ to the classification tree, e.g., in a call to
$\mathit{Refine}(\mathcal{U}(u),\vec{\alpha}\vec{v})$, the parameters of
$\vec{v}$ are symbolic, so comparisons between parameters in the prefix and
suffix must instead be done using tree queries. Let us explain how
restrictions are added for these two different contexts.

Restricting Suffixes During Counterexample Analysis. During analysis of a
counterexample $w=\alpha_{1}(\mathtt{d}_{1})\dots\alpha_{n}(\mathtt{d}_{n})$,
we split $w$ into a prefix
$\alpha_{1}(\mathtt{d}_{1})\dots\alpha_{k}(\mathtt{d}_{k})$ and a suffix
$v=\alpha_{k+1}(\mathtt{d}_{k+1})\dots\alpha_{n}(\mathtt{d}_{n})$. When
forming a symbolic suffix $\vec{v}$ from $v$, restrictions on the parameters
$p_{i}$ of $\vec{v}$ are obtained by

  * •

letting $p_{i}$ be fresh if $\mathtt{d}_{k+i}\neq\mathtt{d}_{j}$ for any
$j<i$.

  * •

letting $p_{i}$ equal a preceding parameter $p_{j}$ if
$\mathtt{d}_{k+i}=\mathtt{d}_{k+j}$, and $p_{j}$ is fresh.

For example, suppose that we find a counterexample
$\mathsf{push}(0)\mathsf{push}(1)\mathsf{pop}(1)\mathsf{pop}(0)$ for
hypothesis $\mathcal{H}_{0}$ of Fig. 3, and split it into prefix
$u=\mathsf{push}(0)$ and suffix
$\mathsf{push}(1)\mathsf{pop}(1)\mathsf{pop}(0)$. When forming the symbolic
suffix $\vec{v}=\mathsf{push}(p_{1})\mathsf{pop}(p_{2})\mathsf{pop}(p_{3})$,
we observe that $p_{1}$ can be fresh since the data value of
$\mathsf{push}(1)$ does not equal any preceding data value. Parameter $p_{2}$
can be restricted as equal to $p_{1}$ since the data value of
$\mathsf{pop}(1)$ is equal to that of $\mathsf{push}(1)$, and $p_{1}$ is
fresh. The last parameter $p_{3}$ cannot be restricted since the data value of
$\mathsf{pop}(0)$ is equal to a data value in the prefix, namely the data
value of $\mathsf{push}(0)$. With the restrictions $\langle
fresh(p_{1}),p_{2}=p_{1}\rangle$ on $\vec{v}$, only three membership queries
must be made when performing the tree query $\mathcal{L}({u},{\vec{v}})$, as
opposed to a total of fifteen membership queries that would be required if
$\vec{v}$ were unrestricted.

Restricting Suffixes Added to the Classification Tree. Whenever a symbolic
suffix is added to the $CT$, this suffix is formed by prepending a symbol
$\vec{\alpha}$ to a symbolic suffix $\vec{v}\in\mathcal{V}$. In this case,
since the parameters of $\vec{v}$ are symbolic, we cannot compare them
directly, so instead we compare guards from tree queries.

In the cases of register closedness or register consistency, the symbol
$\vec{\alpha}$ is formed from a concrete symbol ${\alpha(\mathtt{d})}$ in a
prefix $u{\alpha(\mathtt{d})}$. In these cases, $u$, $\vec{\alpha}$ and
$\vec{v}$ are chosen such that
$\mathit{mem}_{\vec{v}}(u{\alpha(\mathtt{d})}))$ contains particular memorable
parameters. The parameters of $\vec{\alpha}\vec{v}$ can be restricted by
examining the guards of ${\cal L}[u{\alpha(\mathtt{d})},\vec{v}]$. Let us
denote the parameter of $\vec{\alpha}$ as $p_{1}$ and the parameters of
$\vec{v}$ as $p_{2},\dots,p_{|\vec{v}|+1}$. The restrictions on suffix
$\vec{\alpha}\vec{v}$ are then obtained by:

  1. 1.

letting the parameter of $\vec{\alpha}$ be fresh if $\mathtt{d}$ is not equal
to any previous data value in $u$, and

  2. 2.

restricting each parameter $p_{i}$ with $i>1$ in $\vec{\alpha}\vec{v}$ to be
(i) fresh whenever $p_{i-1}$ is fresh in $\vec{v}$ or the branch taken in
${\cal L}[u{\alpha(\mathtt{d})},\vec{v}]$ for fresh $p_{i-1}$ reveals a sought
register, and  (ii) equal to a previous value $p_{j}$ in $\vec{\alpha}\vec{v}$
if the branch taken in ${\cal L}[u{\alpha(\mathtt{d})},\vec{v}]$ for $p_{i-1}$
which is equal to the corresponding value reveals a sought register.

As an example, assume that we have a prefix $\alpha(0)\alpha(1)$ and symbolic
suffix $\vec{v}=\alpha(p_{2})\alpha(p_{3})$. We want to form an extended
symbolic suffix $\vec{\alpha}\vec{v}=\alpha(p_{1})\alpha(p_{2})\alpha(p_{3})$,
given the tree query ${\cal L}[\alpha(0)\alpha(1),\vec{v}]$ shown in Fig.
8(left). The registers $x_{1}$ and $x_{2}$ are mapped to the data values 0 and
1, respectively, in the prefix. In this example, the symbolic suffix
$\vec{\alpha}\vec{v}$ is needed to reveal the memorable data value $x_{1}$.
First, we restrict $p_{1}$ to be fresh, since the data value of $\alpha(1)$
does not equal any preceding parameter. Second, we restrict $p_{2}$ to be
equal to $p_{1}$, as the tree query has guard $p_{2}=x_{2}$, and $x_{2}$
corresponds to the fresh parameter $p_{1}$. Finally, we note that $p_{3}$
cannot be restricted, as there is a guard $p_{3}=x_{1}$ and $x_{1}$ maps to a
data value in $u$.

{$x_{1},x_{2}$}$p_{2}=x_{2}$$p_{2}\neq x_{2}$$p_{3}=x_{1}$$p_{3}\neq
x_{1}$$p_{3}=x_{2}$$p_{3}\neq x_{2}$ (a) Tree query for prefix
$\alpha(0)\alpha(1)$.

{$x_{1}$}$p_{2}=x_{1}$$p_{2}\neq x_{1}$${\it true}$${\it true}$ (b) Tree query
for prefix $\alpha(0)$.

Figure 8: Tree queries for two prefixes with symbolic suffix
$\alpha(p_{2})\alpha(p_{3})$.

The case of transition consistency (b), where two prefixes
$u{\alpha(\mathtt{d})}$ and $u{\alpha(\mathtt{d}^{\prime})}$ lead to the same
location but are not equivalent under the identity mapping between registers,
is handled similarly to register consistency. Since
$u{\alpha(\mathtt{d})}\not\simeq_{\vec{v}}^{\mathbf{id}}u{\alpha(\mathtt{d}^{\prime})}$,
we need only consider one of ${\cal L}[u{\alpha(\mathtt{d})},\vec{v}]$ and
${\cal L}[u{\alpha(\mathtt{d}^{\prime})},\vec{v}]$ when imposing restrictions
on $\vec{\alpha}\vec{v}$, with the caveat that one of $\mathtt{d}$ and
$\mathtt{d}^{\prime}$ will be equal to a parameter in $u$ so the parameter of
$\vec{\alpha}$ cannot be restricted.

In the case of location consistency, we want to find a symbolic suffix
$\vec{\alpha}\vec{v}$ that separates two prefixes $u$ and $u^{\prime}$. As
such, when we restrict $\vec{\alpha}\vec{v}$, we must do so in a way such that
$\vec{\alpha}\vec{v}$ retains its ability to separate $u$ and $u^{\prime}$.
Assume that we have found two continuations $u{\alpha(\mathtt{d})}$ and
$u^{\prime}{\alpha(\mathtt{d}^{\prime})}$ which lead to different locations.
Let us denote the parameter of $\vec{\alpha}$ as $p_{1}$ and the parameters of
$\vec{v}$ as $p_{2},\cdots,p_{|\vec{v}|+1}$. Now, let $\tau\in Dom({\cal
L}[u{\alpha(\mathtt{d})},\vec{v}])$ be a
$(u{\alpha(\mathtt{d})},\vec{v})$-path and let $\tau^{\prime}\in Dom({\cal
L}[u^{\prime}{\alpha(\mathtt{d}^{\prime})},\vec{v}])$ be a
$(u^{\prime}{\alpha(\mathtt{d}^{\prime})}u,\vec{v})$-path such that  (i) the
conjunction of the guard expressions of $\tau$ and $\tau^{\prime}$ is
satisfied, and  (ii) ${\cal L}[u{\alpha(\mathtt{d})},\vec{v}](\tau)\neq{\cal
L}[u^{\prime}{\alpha(\mathtt{d}^{\prime})},\vec{v}](\tau^{\prime})$.  For each
such pair $\tau,\tau^{\prime}$ of paths, a restricted symbolic suffix
$\vec{\alpha}\vec{v}_{(\tau,\tau^{\prime})}$ is obtained by

  1. 1.

letting $p_{1}$ be fresh if $\mathtt{d}$ does not equal any data value in $u$
and $\mathtt{d}^{\prime}$ does not equal any data value of $u^{\prime}$,

  2. 2.

letting each parameter $p_{i}$ with $i>1$ be fresh if, in both $\tau$ and
$\tau^{\prime}$, the guard for $p_{i}$ is either ${\it true}$ or a disequality
guard, and

  3. 3.

restricting each parameter $p_{i}$ with $i>1$ as equal to a preceding
parameter $p_{j}$ if  (i) the only guard on $p_{i}$ in $\tau$ is
$p_{i}=p_{j}$,  (ii) the only guard on $p_{i}$ in $\tau^{\prime}$ is
$p_{i}=p_{j}$, $p_{i}\neq p_{j}$ or ${\it true}$, and  (iii) $p_{j}$is fresh.

We choose as our restricted suffix $\vec{\alpha}\vec{v}$ the
$\vec{\alpha}\vec{v}_{(\tau,\tau^{\prime})}$ with the smallest number of
unrestricted parameters. The case of transition consistency (a) is handled
similarly, with the only difference being that, in this case, $u=u^{\prime}$.

As an example, assume we have two prefixes
$u{\alpha(\mathtt{d})}=\alpha(0)\alpha(1)$ and
$u^{\prime}{\alpha(\mathtt{d}^{\prime})}=\alpha(0)$, which lead to different
locations with lowest common ancestor in $CT$ being
$\vec{v}=\alpha(p_{2})\alpha(p_{3})$. The SDTs representing ${\cal
L}[\alpha(0)\alpha(1),\vec{v}]$ and ${\cal L}[\alpha(0),\vec{v}]$ are shown in
Fig. 8. Note that in both SDTs, $x_{1}$ is mapped to the parameter of
$\alpha(0)$ and $x_{2}$ is mapped to the parameter of $\alpha(1)$. There are
two pairs of paths $(\tau,\tau^{\prime})$ to choose from which satisfy both
conditions (i) and (ii), namely  (1) $\tau=(p_{2}=x_{2},p_{3}=x_{1})$and
$\tau^{\prime}=(p_{2}=x_{2},p_{3}:{\it true})$, or  (2) $\tau=(p_{2}\neq
x_{2},p_{3}=x_{2})$and $\tau^{\prime}=(p_{2}\neq x_{2},p_{3}:{\it true})$.  We
can restrict $p_{1}$ as fresh, since $\mathtt{d}$ does not equal any parameter
in $u$ and $\mathtt{d}^{\prime}$ does not equal any parameter in $u^{\prime}$.
For (1), we can restrict $p_{2}=p_{1}$ as it is equal to the parameter
corresponding to $p_{1}$ in both $\tau$ and $\tau^{\prime}$ (the parameter of
$\alpha(1)$ for $\tau$ and of $\alpha(0)$ for $\tau^{\prime}$), and $p_{1}$ is
fresh. However, we cannot place any restriction on $p_{3}$, since, in $\tau$,
$p_{3}$ is equal to a data value in $u$ (namely, $x_{1}$). For (2), we can
restrict $p_{2}$ to be fresh, since the guard is a disequality guard for both
$\tau$ and $\tau^{\prime}$, and we can restrict $p_{3}$ to be equal to $p_{1}$
since $p_{3}$ is equal to $x_{2}$ (i.e., equal to $p_{1}$) in $\tau$ and
$p_{3}$ has a ${\it true}$ guard in $\tau^{\prime}$. Since we have one
unrestricted parameter in $\vec{\alpha}\vec{v}$ for (1), but none for (2), we
choose the set of restrictions of (2). Thus, we restrict $\vec{\alpha}\vec{v}$
by $\langle fresh(p_{1}),fresh(p_{2}),p_{3}=p_{1}\rangle$.

##  Appendix 0.C Correctness and Complexity Proofs

In this appendix, we establish the correctness and complexity properties of
${SL}^{\lambda}$.

Lemma 1.  A counterexample always leads to a new short prefix (Case 1 of
Algorithm 3) or new prefix (Case 2 of Algorithm 3).

###### Proof

We know that at every index $i$, for $u\in As(w_{1:i-1})$, it holds that

  1. 1.

$\mathcal{H}({u{\alpha(\mathtt{d}_{u}^{g})}},{\vec{v}})\equiv\mathcal{H}({u^{\prime}},{\vec{v}})$
and that

  2. 2.

$\mathcal{H}({u},{\vec{\alpha}\vec{v}})$ has a $g$-guarded subtree
$\mathcal{H}({u{\alpha(\mathtt{d}_{u}^{g})}},{\vec{v}})$.

We also know that
$\mathcal{L}({u_{m}},{\epsilon})\equiv\mathcal{H}({u_{m}},{\epsilon})$ for
$u_{m}\in As(w_{1:m})$ because $\epsilon$ is the symbolic suffix of the root
in the classification tree and determines if the location of $u_{m}$ is
accepting or rejecting. On the other hand,
$\mathcal{L}({\epsilon},{\vec{v}})\not\equiv\mathcal{H}({\epsilon},{\vec{v}})$
for $\vec{v}=w_{1:m}$ since $w$ is a counterexample.

As a consequence, at some index $i$ it must either be the case that
$\mathcal{L}({u{\alpha(\mathtt{d}_{u}^{g})}},{\vec{v}})\not\equiv\mathcal{L}({u^{\prime}},{\vec{v}})$
or that $\mathcal{L}({u},{\vec{\alpha}\vec{v}})$ has a $g^{\prime}$-guarded
subtree that is not present in $\mathcal{H}({u},{\vec{\alpha}\vec{v}})$. When
analyzing a counterexample, we make $u{\alpha(\mathtt{d}_{u}^{g})}$ a short
prefix (a prefix, respectively). Either a refinement occurs immediately, or
next time we arrive at the same check $u{\alpha(\mathtt{d}_{u}^{g})}$ will be
a short prefix (prefix, respectively) and the condition will not be satisfied.
The algorithm will continue with the next case or index of the counterexample
and the arguments given above apply.  $\sqcap$$\sqcup$

Let $m$ be the length of the longest counterexample, $t$ the number of
transitions, $r$ the maximal number of registers at any location, and $n$ the
number of locations in the final model.

Theorem 5.1.  ${SL}^{\lambda}$ infers a RA for regular data language
$\mathcal{L}$ with $O(t)$ equivalence queries and $O(t^{2}\,n^{r}+tmn\,m^{m})$
membership queries for sifting words and analyzing counterexamples.

###### Proof

Every counterexample will lead to progress: the counterexample will produce a
new transition or a new short prefix and a corresponding refinement is
guaranteed to occur before the next equivalence query. The canonic acceptor
has a finite number of locations and transitions. By construction, the final
model will accept $\mathcal{L}$.

The classification tree will have at most $n+2r+2t=O(t)$ inner nodes (since
$t\geq n>r$) created through refinement operations in Algorithm 2 on any path
to a leaf. Suffixes at these nodes tree have at most $r$ unrestricted
parameters. The size of ${U}$ is limited by $t+1$, resulting in at most
$O(t^{2})$ tree queries A tree query in the classification tree results in at
most $O(n^{r})$ membership queries as prefixes are of length $n$ or shorter.
The number of counterexamples is limited by $t$. For the longest
counterexample of length $m$, it can be necessary to compute $mn$ tree queries
that each can require $O(m^{m})$ membership queries in the worst case.
$\sqcap$$\sqcup$

This is an improvement over the worst case estimate of $O(tr)$ equivalence
queries for ${SL}^{*}$ [10]. ${SL}^{\lambda}$ also improves the worst case for
membership queries for sifting to $O(t^{2}\,n^{r})$ from $O(t^{2}r\,n^{r})$
for filling the table in ${SL}^{*}$.

For analyzing counterexamples, ${SL}^{\lambda}$ replaces ${SL}^{*}$’s
$O(trm\,m^{m})$ worst case estimate with $O(tmn\,m^{m})$, where $t$ dominates
$n$ and $r$.