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 or deterministic finite automata. 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 article, we present \({SL}^{\lambda }\), an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of membership queries 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 prove that \({SL}^{\lambda }\) is guaranteed to learn an acceptor, in the form of a register automaton with n locations and t transitions, for a given data language of finite index, and that it can do so with at most \(O(t^2 \, (2n)^n + m t^2 \, m^m)\) membership queries and O(t) equivalence queries, where m is the length of the longest counterexample received during learning. 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. Experiments on a series of benchmarks show that it reduces the number of membership queries by up to an order of magnitude, and also shows substantial asymptotic improvements in bigger systems.
1 Introduction
Model Learning, also known as Active Automata Learning (AAL) [8, 65, 74], 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 [28, 29, 40, 66, 71], mining APIs [7], supporting model-based testing [42, 73, 79] and conformance testing [2]. The AAL algorithms employed in these works are efficient and supported by various domain-specific optimizations (e.g., [48]), 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 Finite State Machine (EFSM) models [1, 13, 17] 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 [23, 55]. Finally, there exist extensions of AAL to EFSM models with guards and state variables, such as Register Automata (RA) [3, 4, 17, 18, 46]. While their potential has been shown by being able to uncover critical bugs in e.g., TCP implementations [27, 31], their learning algorithms do not scale beyond small and well curated experiments.
In this article, we follow the third line of works and address the scalability of register automata learning algorithms. The main challenge when scaling active automata learning algorithms is reducing the number of tests that learners perform on a SUL. Generally, these tests are sequences of actions of the form uv, where u is the prefix and v the suffix of the sequence. Tests uv and \(u' v\) are then used to determine whether prefixes u and \(u'\) 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., \(\textsf{push}(1)\,\textsf{push}(2)\), and suffixes are sequences of actions with symbolic parameters, e.g., \(\textsf{pop}(p_1)\,\textsf{pop}(p_2)\), that, when instantiated, can incur a number of tests that is exponential in the length of the suffix. Examples of tests that combine this prefix and suffix include \(\textsf{push}(1)\,\textsf{push}(2)\,\textsf{pop}(2)\,\textsf{pop}(1)\), \(\textsf{push}(1)\,\textsf{push}(2)\,\textsf{pop}(2)\,\textsf{pop}(3)\), \(\textsf{push}(1)\,\textsf{push}(2)\,\textsf{pop}(1)\,\textsf{pop}(2)\), and so on. Such tests are used for identifying dependencies between prefix values and suffix parameters, and for distinguishing prefixes based on suffixes. To make register automata learning scalable, it is crucial to reduce the number of tests as much as possible. This can be done along several dimensions: First, it is important to reduce the number of tested prefix-suffix combinations. Second, when using suffixes in tests, shorter suffixes should be preferred over longer ones. 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 article, we present the \({SL}^{\lambda }\) algorithm, an active automata learning algorithm, which infers a register automaton that accepts an unknown data language \(\mathcal {L}\) using a minimally adequate teacher (MAT). Such a teacher answers two types of queries about \(\mathcal {L}\): A membership query (i.e., a test) asks whether some data word w is in \(\mathcal {L}\). An equivalence query asks whether some register automaton \(\mathcal {H}\) accepts \(\mathcal {L}\), and is answered either by yes or by a counterexample from the symmetric difference of \(\mathcal {L}\) and \(\mathcal {L}(\mathcal {H})\). The \({SL}^{\lambda } \) algorithm achieves scalability by optimizing the use of tests and suffixes in tests along 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 [49, 51] where it proved very successful for reducing the number of tests. We also adopt the technique of computing suffixes incrementally from inconsistencies in order to keep them short [45, 49]. This has not been studied for RAs before and leads to an improved worst case complexity compared to state-of-the-art approaches. Finally, we show how suffixes can be restricted to relevant data dependencies, which is essential for achieving scalability. We prove that our \({SL}^{\lambda }\) algorithm, when presented with a data language \(\mathcal {L}\) of finite index, is guaranteed to infer an RA which accepts \(\mathcal {L}\), using at most \(O(t^2 \, (2n)^n + m t^2 \, m^m)\) membership queries (tests) and O(t) equivalence queries (searches for counterexamples), where n and t are the number of locations and transitions in the final model, and m is the length of the longest counterexample received during learning.
We have implemented \({SL}^{\lambda }\) as a new algorithm in RALib.Footnote 1 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}^{*}\) [17] 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.
Outline
We present the key ideas in tree-based learning of register automata informally in the next section (Sect. 2), and provide formal definitions of basic concepts in Sect. 3. The main section of this article (Sect. 4) contains the description of the \({SL}^{\lambda }\) algorithm, how register automata are constructed and how counterexamples are analyzed, and an extension of \({SL}^{\lambda }\) for the inequality theory. Subsequently, we demonstrate the algorithm on an example (Sect. 5), and prove statements about its correctness and complexity in Sect. 6. We then introduce optimizations which impose restrictions on symbolic suffixes (Sect. 7). We present our implementation and evaluate its performance in Sect. 8. The article ends with a discussion of related works (Sect. 9) and concluding remarks (Sect. 10).
Differences from the TACAS 2024 Paper
A shorter version of this article, appears in the proceedings of TACAS 2024 with the title “Scalable Tree-based Register Automata Learning” [22]. Compared to that paper, this article (i) contains a more extensive description of the \({SL}^{\lambda }\) algorithm, especially w.r.t. how symbolic decision trees are constructed (Sect. 4.4) and how counterexamples are analyzed (Sect. 4.5); (ii) an extension of \({SL}^{\lambda }\) for the inequality theory (Sect. 4.6); (iii) a new section that illustrates the use of the algorithm (Sect. 5); (iv) a new section describing suffix optimizations (Sect. 7); and (v) a section presenting publicly available supporting infrastructure that we have used in our evaluation (Sect. 8.3). Last but not least, this article contains a significantly expanded section with correctness and complexity properties of the algorithm as well as formal proofs for them.
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 \(\textsf{push}\) and \(\textsf{pop}\), both of which take one natural number as a parameter. The operation \(\textsf{push}(\texttt {d} )\) succeeds if the stack is not full, i.e., contains at most one element; the operation \(\textsf{pop}(\texttt {d} )\) succeeds if the last pushed and not yet popped element is \(\texttt {d} \). Let a symbol denote an operation with data value, such as \(\textsf{push}(1)\), and let \(\mathcal {L}_{\textit{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}_{\textit{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 does not belong to \(\mathcal {L}_{\textit{Stack} }\), e.g. a word where a third element is pushed, or a non-top element is popped. In each location, registers contain the elements in the stack: for \(i= 0,1,2\), location \(l_i\) has i registers, named \(x_1\) and \(x_2\), where the register with the highest index contains the topmost stack element.
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 (\(\textsf{push}\) and \(\textsf{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 register automaton \(\mathcal {H}\) accepts \(\mathcal {L}\); if so, the query is answered by yes, otherwise by a counterexample, which is a word on which \(\mathcal {L}(\mathcal {H})\) 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'\) iff \(uv \in \mathcal {L}\Leftrightarrow u'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 \(\textsf{push}(0)\), and symbolic suffix \(\varvec{v}\), say \(\textsf{push}(p_1)\textsf{pop}(p_2)\), membership in \(\mathcal {L}\) of words of the form \(u\varvec{v}\) depends on the relation between the data values of u and the parameters \(p_1,p_2\) of \(\varvec{v}\); in \({SL}^{\lambda } \) this dependency is represented by a function \(\mathcal{L}[u,\varvec{v}]\) with arguments \(x_1\) (representing the data value of u), \(p_1\), and \(p_2\). Letting + stand for accept or member and − for reject or non-member, we have \(\mathcal{L}[u,\varvec{v}](x_1,p_1,p_2)\) is + iff \(p_2 = p_1\) and − otherwise. In the \({SL}^{\lambda } \) algorithm, such functions are represented as decision trees of a specific form.
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 \({ true}\)), and thereafter the constraint on \(p_2\) (a comparison with \(p_1\)). Two prefixes u, \(u'\) are then equivalent w.r.t. \(\mathcal {V}\) if \(\mathcal{L}[u,\varvec{v}]\) and \(\mathcal{L}[u',\varvec{v}]\) are “isomorphic modulo renaming of registers” for all \(\varvec{v}\in \mathcal {V}\). Details are presented in Sect. 4.
Functions of the form \(\mathcal{L}[u,\varvec{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 \(\varvec{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 Sect. 7.
Initially, \(S_p\) and \(\mathcal {V}\) contain only the empty sequence \(\epsilon \). Since \(\epsilon \) is a short prefix, one-symbol extensions, \(\textsf{push}(0)\) and \(\textsf{pop}(0)\), are entered into \({U}\). Tree queries are performed for the prefixes in \({U}\) and the empty suffix, revealing that \(\textsf{push}(0)\) is accepted and \(\textsf{pop}(0)\) is rejected. Thus, \(\textsf{push}(0)\) cannot be distinguished from \(\epsilon \), but \(\textsf{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 \(\textsf{pop}(0)\), in this case \(\textsf{pop}(0)\textsf{push}(1)\) and \(\textsf{pop}(0)\textsf{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.
This hypothesis is then subject to validation. Assume that validation finds the counterexample \(\textsf{push}(0)\textsf{push}(1)\textsf{push}(2)\), which is accepted by \(\mathcal {H}_0\) but is not in \(\mathcal {L}_{\textit{Stack} }\). Analysis of this counterexample reveals that \(\epsilon \) and \(\textsf{push}(0)\) are inequivalent, since they are separated by the suffix \(\textsf{push}(p_1)\textsf{push}(p_2)\) (since the concatenation of \(\epsilon \) and \(\textsf{push}(p_1)\textsf{push}(p_2)\) is accepted for all \(p_1,p_2\) but \(\textsf{push}(0)\cdot \textsf{push}(1)\textsf{push}(2)\) is always rejected for all \(p_1,p_2\)). It could seem natural to add \(\textsf{push}(p_1)\textsf{push}(p_2)\) to \(\mathcal {V}\), but \({SL}^{\lambda } \) will not do that, since it follows the principle (from the \(L^\lambda \) algorithm [45]) 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 \(\textsf{push}(p_1)\textsf{push}(p_2)\) as a suffix, \({SL}^{\lambda } \) enters the prefix \(\textsf{push}(0)\) into \(S_p\), and adds one-symbol extensions of \(\textsf{push}(0)\), in this case \(\textsf{push}(0)\textsf{push}(1)\) and \(\textsf{push}(0)\textsf{pop}(1)\), to \({U}\). It then notes that \(\textsf{push}(0)\textsf{push}(1)\) is inequivalent to both \(\epsilon \) and \(\textsf{push}(0)\), separated by the suffix \(\textsf{push}(p_1)\). Again, \(\textsf{push}(0)\textsf{push}(1)\) is therefore promoted to a short prefix, and its one-symbol extensions, \(\textsf{push}(0)\textsf{push}(1)\textsf{push}(2)\) and \(\textsf{push}(0)\textsf{push}(1)\textsf{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.
The \(\textsf{push}\)-extensions of \(\epsilon \) and \(\textsf{push}(0)\textsf{push}(1)\) (i.e., \(\textsf{push}(0)\) and \(\textsf{push}(0)\textsf{push}(1)\textsf{push}(2)\), respectively) are separated by the empty suffix. Hence, these two prefixes are separated by the suffix \(\textsf{push}(p_1)\), a one-symbol extension of \(\epsilon \) which is added to \(\mathcal {V}\).
-
2.
The \(\textsf{push}\)-extensions of \(\epsilon \) and \(\textsf{push}(0)\) (i.e., \(\textsf{push}(0)\) and \(\textsf{push}(0)\textsf{push}(1)\), respectively) are separated by the suffix \(\textsf{push}(p_1)\). Hence, \(\epsilon \) and \(\textsf{push}(0)\) are separated by \(\textsf{push}(p_1)\textsf{push}(p_2)\), formed by prepending a symbol to the just added suffix \(\textsf{push}(p_1)\), which is added to \(\mathcal {V}\).
After adding the suffixes, the closedness and consistency criteria of \({SL}^{\lambda } \) are satisfied (see Sect. 4.3), implying that we can form hypothesis \(\mathcal {H}_1\) in Fig. 3(right, top). Assume that the validation of \(\mathcal {H}_1\) finds counterexample \(\textsf{push}(0)\textsf{pop}(0)\), which is in \(\mathcal {L}_{\textit{Stack} }\), but rejected by \(\mathcal {H}_1\). This counterexample reveals that after \(\textsf{push}(0)\), the two continuations \(\textsf{pop}(0)\) and \(\textsf{pop}(1)\) lead to inequivalent locations (separated by suffix \(\epsilon \)), suggesting to refine the \(\textsf{pop}(p)\)-transition after \(\textsf{push}(0)\). To this end, \(\mathcal {V}\) is extended by a suffix formed by prepending \(\textsf{pop}(p)\) to the empty suffix, and a tree query is invoked for \(\mathcal{L}[\textsf{push}(0),\textsf{pop}(p_1)]\), which is + iff \(p_1 = x_1\) and − otherwise. Since \(\mathcal{L}[\textsf{push}(0),\textsf{pop}(p_1)]\) makes a test for \(x_1\), which represents the data value of \(\textsf{push}(0)\), we infer that the data parameter of the \(\textsf{push}(0)\)-prefix must be remembered in a register, and that the \(\textsf{pop}(p)\)-transition must be split into two with guards \((x_1 \ne p)\) and \((x_1 = p)\). The resulting hypothesis, \(\mathcal {H}_2\), is shown in Fig. 3(right, bottom). \(\mathcal {H}_2\) is then subject to another round of validation; the subsequent hypothesis construction reveals the \(\textsf{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 \(\varvec{v}\) and induces a subtree for each equivalence class w.r.t. \(\varvec{v}\), whose leaves contain prefixes in this equivalence class. For example, in Fig. 4, which shows a classification tree corresponding to hypothesis \(\mathcal {H}_1\), the nodes are labeled by the suffixes \(\epsilon \), \(\textsf{push}(p_1)\) and \(\textsf{push}(p_1)\textsf{push}(p_2)\), which separate the leaves into four equivalence classes corresponding to the four locations of \(\mathcal {H}_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.
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 \(\textsf{push}(0)\textsf{push}(1)\textsf{push}(2)\) for \(\mathcal {H}_0\) shows that \(\epsilon \) and \(\textsf{push}(0)\) are inequivalent. To separate these, we need not naïvely consider all possible dependencies between parameters in the prefix and symbolic suffix \(\textsf{push}(p_1)\textsf{push}(p_2)\); but we can restrict the set of instantiations 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 \(\textsf{push}(0)\), and the tree query for prefix \(\textsf{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}\). In this article, we will consider the theories: (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 with special pre-defined constant values).
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 one; our techniques can be extended to handle actions with arbitrary arities. A data symbol is a term of form \(\alpha (\texttt {d} )\), where \(\alpha \) is an action and \(\texttt {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. For a word \(w= \alpha _1(d_1) \ldots \alpha _n(d_n)\), let \(Acts(w)\) denote its sequence of actions \(\alpha _1 \ldots \alpha _n\), let \(Vals(w)\) denote its sequence of data values \(d_1 \ldots d_n\), and let \(w_{i:j}\) denote \(\alpha _i(d_i) \ldots \alpha _j(d_j)\) for \(1 \le i \le j \le n\). Let \(|w|\) denote the number of data symbols in \(w\). Two words \(w= \alpha _1(\texttt {d} _1) \ldots \alpha _n(\texttt {d} _n)\) and \(w'= \alpha _1(\texttt {d} _1') \ldots \alpha _{n}(\texttt {d} _{n}')\) with the same sequences of actions are \(\mathcal {R}\)-indistinguishable, denoted \(w\approx _{\mathcal {R}} w'\), if \(R(\texttt {d} _{i_1},\ldots ,\texttt {d} _{i_j}) \Leftrightarrow R(\texttt {d} _{i_1}', \ldots , \texttt {d} _{i_j}')\) for all j-ary relations \(R \in \mathcal {R}\) and indices \(i_1, \cdots , i_j\) 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'\) implies \(w\in \mathcal {L}\Leftrightarrow w'\in \mathcal {L}\). We often represent data languages as mappings from the set of words to \(\lbrace +,-\rbrace \), 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 \(\lbrace x_{i_1}, \ldots ,x_{i_m}\rbrace \) to \(\lbrace x_{j_1}, \ldots ,x_{j_n}\rbrace \cup \lbrace p\rbrace \), 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, with \(\mathcal {X}(l_0)\) being the empty set,
-
\(\Gamma \) is a finite set of transitions, each of form \(\langle l,\alpha (p),g,\pi ,l'\rangle \), where
-
\(l\in L\) is a source location and \(l' \in L\) is a target location,
-
\(\alpha (p)\) is a parameterized symbol,
-
g, the guard, is a constraint over p and \(\mathcal {X}(l)\),
-
\(\pi \), the assignment, is a mapping from \(\mathcal {X}(l')\) to \(\mathcal {X}(l) \cup \lbrace p\rbrace \), and
-
-
\(\lambda \) maps each \(l\in L\) to \(\lbrace +,-\rbrace \), where + denotes accept and − reject. \(\square \)
A state of a register automaton \(\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 (\texttt {d} )} \langle l',\mu '\rangle \), transfers the state of \(\mathcal {A}\) from \(\langle l,\mu \rangle \) to \(\langle l',\mu '\rangle \) on input of the data symbol \(\alpha (\texttt {d} )\) if there is a transition \(\langle l,\alpha (p),g,\pi ,l'\rangle \in \Gamma \) such that (i) \(\mu ~\models ~ g[\texttt {d} /p]\), i.e., \(\texttt {d} \) satisfies the guard g under the valuation \(\mu \), and (ii) \(\mu '\) is defined by \(\mu '(x_i) = \mu (x_j)\) if \(\pi (x_i)= x_j\), otherwise \(\mu '(x_i) = \texttt {d} \) if \(\pi (x_i) = p\). A run of \(\mathcal {A}\) over a data word \(w= \alpha (\texttt {d} _1)\ldots \alpha (\texttt {d} _n)\) is a sequence of steps of \(\mathcal {A}\)
Note that \(\mu _0\) is the empty valuation, since \(l_0\) has no registers. 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 data language \(\mathcal {L}(\mathcal {A})\) of \(\mathcal {A}\) as the set of words accepted by \(\mathcal {A}\). We sometimes write \(\mathcal {A}(w) = +\) for \(w \in \mathcal {L}(\mathcal {A})\) and \(\mathcal {A}(w) = -\) for \(w \not \in \mathcal {L}(\mathcal {A})\). We require register automata to be determinate, meaning that there is no data word over which they have 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.
Symbolic Decision Trees
The functions, of form \(\mathcal{L}[u,\varvec{v}]\), that result from tree queries, should represent how the language \(\mathcal {L}\) processes instantiations of \(\varvec{v}\) after the prefix u. Since \({SL}^{\lambda } \) is intended to construct register automata, 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 data word \(u = \alpha _1(\texttt {d} _1)\ldots \alpha _k(\texttt {d} _k)\), let \(\mu _{u}\) be the valuation with domain \(\lbrace x_1, \ldots , x_{k}\rbrace \) such that \(\mu _{u}(x_i) = d_i\) for \(i = 1, \ldots , k\). A u-guard is a constraint g over \(x_1, \ldots , x_{k}\) and the formal parameter p. We sometimes write \((u,\texttt {d} )\models g\) for \(\mu _{u} \models g[\texttt {d} /p]\), i.e., that the data value \(\texttt {d} \) satisfies the guard g after the prefix u. We require that to each u-guard g is assigned a unique representative data value, denoted \(\texttt {d} _{u}^{g}\), which satisfies \((u,\texttt {d} _{u}^{g})\models g\), Thus, each u-guard must have at least one satisfying instantiation of the formal parameter p. Moreover, we require that (i) \(\texttt {d} _{u}^{g}\) must not be equal to a data value in u unless that is necessitated by g (i.e., g is an equality guard), and (ii) if some other u-guard \(g'\) satisfies \(\mu _{u} \models (g' \Rightarrow g)\) and \((u,\texttt {d} _{u}^{g})\models g'\) then \(\texttt {d} _{u}^{g'} = \texttt {d} _{u}^{g}\). In the \({SL}^{\lambda }\) algorithm, each one-symbol extension of form \(u{\alpha (\texttt {d} )}\) is formed to let \(\texttt {d} \) satisfy a specific guard g; we then always choose \(\texttt {d} \) as \(\texttt {d} _{u}^{g}\).
A symbolic suffix is a data word in which data values are replaced by (distinct) formal parameters \(p_1, \ldots , p_{m}\). For a data word \(u = \alpha _1(\texttt {d} _1)\ldots \alpha _k(\texttt {d} _k)\) and a symbolic suffix \(\varvec{v}= \alpha _1'(p_1)\ldots \alpha _m'(p_m)\), a \((u,\varvec{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 \({G}_{\tau }\), as \(g_{1} \wedge \cdots \wedge g_{m}\). A \((u,\varvec{v})\)-tree \(T\) is a mapping from a set \(Dom(T)\) of \((u,\varvec{v})\)-paths to \(\lbrace +,-\rbrace \). For example, Fig. 2 shows a \((u, \varvec{v})\)-tree where \(u=\textsf{push}(\texttt {d} _1)\) and \(\varvec{v}=\textsf{push}(p_1)\textsf{pop}(p_2)\). This \((u, \varvec{v})\)-tree contains the paths \(\tau _1 = (true,\, p_2=p_1)\), which maps to +, and \(\tau _2 = (true,\, p_2 \ne p_1)\), which maps to −. For a \((u, \varvec{v})\)-path \(\tau = g_1,\ldots ,g_m\), we refer to \(g_1\) as the initial guard of \(\tau \). For a \((u, \varvec{v})\)-tree \(T\), we refer to the set of initial guards of its \((u, \varvec{v})\)-paths \(\tau \in Dom(T)\) as the initial guards of \(T\). For example, the \((u, \varvec{v})\)-tree in Fig. 2 has the one initial guard \({ true}\). Write \(\overline{\texttt {d} }\) for \(\texttt {d} _1, \ldots , \texttt {d} _{k}\), \(\overline{\texttt {d} '}\) for \(\texttt {d} '_1, \ldots , \texttt {d} '_{m}\), \(\overline{x}\) for \(x_1, \ldots , x_{k}\), and \(\overline{p}\) for \(p_1, \ldots , p_{m}\). A \((u,\varvec{v})\)-tree \(T\) can be seen as a function from valuations of \(\overline{x},\overline{p}\) to \(\lbrace +,-\rbrace \), defined by \(T(\overline{x},\overline{p}) = T(\tau )\) whenever \(\tau \in Dom(T)\) and \({G}_{\tau }(\overline{x},\overline{p})\) holds. That is, for data values \(\overline{\texttt {d} }\) and \(\overline{\texttt {d} '}\) and each \((u,\varvec{v})\)-path \(\tau \), we have \(T(\overline{\texttt {d} },\overline{\texttt {d} '}) = T(\tau )\) whenever \({G}_{\tau }(\overline{\texttt {d} },\overline{\texttt {d} '})\) is true. In Fig. 2, \(T(0,1,1) = +\) since \({G}_{\tau _1}(0,1,1) = (true \wedge 1 = 1)\) holds and \(T(\tau _1)=+\). If \(\mathcal {L}\) is a data language, then \(\mathcal{L}[u,\varvec{v}]\) is a \((u,\varvec{v})\)-tree representing membership in \(\mathcal {L}\) in the sense that for any values of \(\texttt {d} '_1, \ldots , \texttt {d} '_{m}\) we have \(\mathcal{L}[u,\varvec{v}](\overline{\texttt {d} },\overline{\texttt {d} '}) = +\) iff \(u\alpha _1'(\texttt {d} '_1)\ldots \alpha _m'(\texttt {d} '_m) \in \mathcal {L}\), and \(\mathcal{L}[u,\varvec{v}](\overline{\texttt {d} },\overline{\texttt {d} '}) = -\) iff \(u\alpha _1'(\texttt {d} '_1)\ldots \alpha _m'(\texttt {d} '_m) \not \in \mathcal {L}\). For example, if \(\mathcal {L}\) is the language \(\mathcal {L}_{\textit{Stack} }\) of the stack in Fig. 1, then the \((u, \varvec{v})\)-tree in Fig. 2 reveals that \(\textsf{push}(0)\textsf{push}(1)\textsf{pop}(1) \in \mathcal {L}\) as \(\mathcal{L}[u,\varvec{v}](0,1,1) = +\), but \(\textsf{push}(0)\textsf{push}(1)\textsf{pop}(2)\not \in \mathcal {L}\) as \(\mathcal{L}[u,\varvec{v}](0,1,2)=-\). Two \((u,\varvec{v})\)-trees, \(T\) and \(T'\), are equivalent denoted \(T\equiv T'\), if \(Dom(T) = Dom(T')\) and \(T(\tau ) = T'(\tau )\) for each \(\tau \in Dom(T)\).
\({SL}^{\lambda }\) generates \((u,\varvec{v})\)-trees \(\mathcal{L}[u,\varvec{v}]\) representing membership in the language \(\mathcal {L}\) to be learned through so-called tree queries. Intuitively a tree query constructs \(\mathcal{L}[u,\varvec{v}]\) by performing membership queries for each equivalence class of words of form \(u \alpha _1'(\texttt {d} _{1}') \ldots \alpha _m'(\texttt {d} _m')\) (where \(\texttt {d} _1', \ldots , \texttt {d} _m'\) range over \(\mathcal {D}\)) and organizing the results into a tree. Thereafter, starting from the leaves, outgoing branches are merged with as large guards as possible as long as all concerned suffixes are correctly classified. A more detailed description appears after the next paragraph.
From the \((u,\varvec{v})\)-trees of form \(\mathcal{L}[u,\varvec{v}]\), constructed by 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 \(\mathcal{L}[u,\varvec{v}]\); the outgoing guards from the location reached by u can be derived from the initial guards in the trees \(\mathcal{L}[u,\varvec{v}]\), since the initial guards represent the constraints that are used when processing the first symbol of \(\varvec{v}\). Let \(\textit{mem} _{\varvec{v}}(u)\), the set of memorable parameters, denote the set of registers among \(\lbrace x_1, \ldots , x_{|u|}\rbrace \) that occur on some \((u,\varvec{v})\)-path in \(Dom(\mathcal{L}[u,\varvec{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 a set \(\mathcal {V}\) of symbolic suffixes, define \(\textit{mem} _{\mathcal {V}}(u)\) as \(\cup _{\varvec{v}\in \mathcal {V}} \textit{mem} _{\varvec{v}}(u)\). For a prefix u and symbolic suffix \(\varvec{v}\) whose first action is \(\alpha \), let \(\mathcal{G}_{\lbrace \varvec{v}\rbrace }(u,\alpha )\) denote the initial guards in the \((u,\varvec{v})\)-tree \(\mathcal{L}[u,\varvec{v}]\), with \(p_1\) replaced by p. For a set \(\mathcal {V}\), let \(\mathcal{G}_{\mathcal {V}}(u,\alpha )\) denote the set of conjunctions of guards in \(\mathcal{G}_{\lbrace \varvec{v}\rbrace }(u,\alpha )\) for \(\varvec{v}\in \mathcal {V}\) with first action \(\alpha \).
Constructing Symbolic Decision Trees
Let us here describe how \((u,\varvec{v})\)-trees are constructed in the theories \(\langle \mathbb {N}, \{=\} \rangle \) with equality and \(\langle \mathbb {R}, \{ < \} \rangle \) with inequality. Fix a prefix \(u = \alpha _1(\texttt {d} _1) \ldots \alpha _k(\texttt {d} _k)\). Define the potential of u, denoted \({ pot}(u)\), as the sequence of positions of first occurrences of data values in u, sorted according to their data values. More precisely, \({ pot}(u)\) is the sequence \(i_1, \ldots , i_n\) of indices in \(\lbrace 1, \ldots , k\rbrace \) such that \(\texttt {d} _{i_j}\) is the first occurrence of data value \(\texttt {d} _{i_j}\) in u, ordered such that \(\texttt {d} _{i_1}< \texttt {d} _{i_2}< \ldots < \texttt {d} _{i_n}\). For instance, if u is \(\alpha _1(5) \alpha _2(9)\alpha _3(3) \alpha _4(5)\), then \({ pot}(u)\) is 3, 1, 2. Our construction will use u-guards which are either of form \(p = x_{i_j}\) for \(i_j \in { pot}(u)\), or
-
in the theory with equality: of form \(\displaystyle \bigwedge _{l \in J} p \ne x_{l} \) for some \(J \subseteq { pot}(u)\) (note that this reduces to \({ true}\) if J is empty),
-
in the theory with inequality: of form \(x_{i_j} \sim p \sim ' x_{i_l}\) for \(i_j, i_l \in { pot}(u)\) with \(j < l\), or of form \(p \sim x_{i_j}\) or \(x_{i_j} \sim p\) for \(i_j \in { pot}(u)\), where \(\sim , \sim ' \in \lbrace <, \le \rbrace \).
Let \(\varvec{v}\) be a symbolic suffix \(\varvec{v}= \alpha _1'(p_{1}) \ldots \alpha _m'(p_m)\). Define \(\textit{tl} (\varvec{v})\) as \(\alpha _2'(p_{1}) \ldots \alpha _m'(p_{m{-}\!1})\). For a data value \(\texttt {d} \), a u-guard g, and a \((u\alpha _1'(\texttt {d} ),\textit{tl} (\varvec{v}))\)-path \(\tau = g_1, \ldots , g_{m{-}\!1}\), define \({g};{\tau }\) as the \((u,\varvec{v})\)-path which puts g in front of \(\tau \). More precisely, \({g};{\tau }\) is defined as \(g[p_1/p], g_1', \ldots , g_{m{-}\!1}'\), where each \(g_j'\) is obtained from \(g_j\) by replacing \(x_{|u|{0.6}{+}\!1}\) by \(p_1\) and \(p_i\) by \(p_{i{0.6}{+}\!1}\) for \(i = 1, \ldots , m_{i{-}\!1}\).
Definition 2
(SDT-construction) For a prefix \(u = \alpha _1(\texttt {d} _1) \ldots \alpha _k(\texttt {d} _k)\) and a symbolic suffix \(\varvec{v}= \alpha _1'(p_{1}) \ldots \alpha _m'(p_m)\), the \((u,\varvec{v})\)-tree \(\mathcal{L}[u,\varvec{v}]\) is defined recursively as follows.
-
If \(\varvec{v}= \epsilon \), the domain of \(\mathcal{L}[u,\varvec{v}]\) is the empty path, which is mapped to + or −, depending on whether \(u \in \mathcal {L}\) or not.
-
If \(\varvec{v}\not = \epsilon \), then let G be the set of maximal u-guards g such that for all \(u\alpha _1'(\texttt {d} _{k{0.6}{+}\!1})\) such that \(\texttt {d} _{k{0.6}{+}\!1}\) satisfies g after u (i.e., \((u,\texttt {d} _{k{0.6}{+}\!1})\models g\)) it holds that
-
for all suffixes of form \(\alpha _2'(\texttt {d} _{2}') \ldots \alpha _m'(\texttt {d} _m')\), the word \(u\alpha _1'(\texttt {d} _{k{0.6}{+}\!1}) \alpha _2'(\texttt {d} _2') \ldots \alpha _m'(\texttt {d} _m')\) is correctly classified by the subtree \(\mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})](x_1, \ldots , x_{k{0.6}{+}\!1},p_1, \ldots , p_{m{-}\!1})\) with \(\texttt {d} _1, \ldots , \texttt {d} _{k{0.6}{+}\!1}\) for \(x_1, \ldots , x_{k{0.6}{+}\!1}\) and \(\texttt {d} _2', \ldots , \texttt {d} _{m}'\) for \(p_1, \ldots , p_{m{-}\!1}\), and that
-
for each \((u\alpha _{1}'(\texttt {d} _{u}^{g}), \textit{tl} (\varvec{v}))\)-path \(\tau = g_1, \ldots , g_{m{-}\!1}\) in \(Dom(\mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})])\), there is a suffix of form \(\alpha _2'(\texttt {d} _2') \ldots \alpha _m'(\texttt {d} _m')\) which satisfies \(\tau \) with \(\texttt {d} _1, \ldots , \texttt {d} _{k{0.6}{+}\!1}\) for \(x_1, \ldots , x_{k{0.6}{+}\!1}\) and \(\texttt {d} _2', \ldots , \texttt {d} _{m}'\) for \(p_1, \ldots , p_{m{-}\!1}\).
Then
-
\(Dom(\mathcal{L}[u,\varvec{v}]) = \lbrace {g};{\tau } ~:~ g \in G \hbox { and } \tau \in Dom(\mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})])\rbrace \), and
-
\(\mathcal{L}[u,\varvec{v}]({g};{\tau }) = \mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})](\tau )\) for \({g};{\tau } \in Dom(\mathcal{L}[u,\varvec{v}])\). \(\square \)
-
Intuitively, \(\mathcal{L}[u,\varvec{v}]\) is constructed by letting its initial outgoing branches correspond to guards g that are as large as possible, while still correctly classifying all suffixes. Each outgoing branch with guard g leads to the subtree \(\mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})](\tau )\). In the construction, the check whether \(\mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})]\) correctly classifies all suffixes after all \(u\alpha _1'(\texttt {d} _{i{0.6}{+}\!1})\) with \((u,\texttt {d} _{k{0.6}{+}\!1})\models g\) (i.e., not only after \(u\alpha _1'(\texttt {d} _{u}^{g})\)) needs only be performed once for each equivalence class of \(u\alpha _1'(\texttt {d} _{k{0.6}{+}\!1})\) w.r.t. \(\approx _{\mathcal {R}}\). One way to perform this check is to construct \(\mathcal{L}[u\alpha _{1}'(\texttt {d} ),\textit{tl} (\varvec{v})]\) for a representative data value \(\texttt {d} \) in each equivalence class, and compare it to \(\mathcal{L}[u\alpha _{1}'(\texttt {d} _{u}^{g}),\textit{tl} (\varvec{v})]\).
Let us illustrate the construction of SDTs on the decision tree in Fig. 2, which shows \(\mathcal{L}[u,\varvec{v}]\) for \(u = \textsf{push}(0)\) and \(\varvec{v}= \textsf{push}(p_1)\textsf{pop}(p_2)\), with \(\mathcal {L}\) being the language of the stack of Fig. 1. If \(\texttt {d} _{u}^{{ true}} = 1\), then the middle node in the tree is the root of the subtree \(\mathcal{L}[u\textsf{push}(1),\textsf{pop}(p_1)]\), which has two branches, corresponding to the two maximal guards: \(p = x_2\), representing \(u\textsf{push}(1)\textsf{pop}(1)\) (accepted) and \(p \ne x_2\) representing \(u\textsf{push}(0)\textsf{pop}(\texttt {d} _2))\) for all other \(\texttt {d} _2\) (rejected). For the guard \(p = x_2\) there is only one test case, but for the guard \(p \ne x_2\) there are two equivalence classes, corresponding to the data values 0 and 2, which are both rejected, so the two equivalence classes are covered by the guard \(p \ne x_2\). Let us now move one level up, to the root of the tree. We have already constructed the subtree after \(u\textsf{push}(1)\). There is potentially another subtree corresponding to the guard \(p = x_1\) with representative data value 0. However, all results of this tree are covered by those of the subtree after \(u\textsf{push}(1)\), hence \({ true}\) is a maximal guard which satisfies the criteria in Definition 2.
Equivalence
For a mapping \(\gamma \) on registers, we define its extension to \((u,\varvec{v})\)-paths in the natural way. For a \((u,\varvec{v})\)-tree \(T\), we define \(\gamma (T)\) by \(Dom(\gamma (T)) = \lbrace \gamma (\tau ) ~:~ \tau \in Dom(T)\rbrace \) and \(\gamma (T)(\gamma (\tau )) = T(\tau )\). Let \(u \equiv _{\mathcal {V}} u'\) denote that \(\mathcal{L}[u,\varvec{v}]\equiv \mathcal{L}[u^{\prime },\varvec{v}]\), for all \(\varvec{v}\in \mathcal {V}\). Let \(u \simeq _{\mathcal {V}}^{\gamma } u^{\prime }\) denote that \(\gamma \) is a bijection from \(\textit{mem} _{\mathcal {V}}(u)\) to \(\textit{mem} _{\mathcal {V}}(u')\) such that for all \(\varvec{v}\in \mathcal {V}\) we have \(\gamma (\mathcal{L}[u,\varvec{v}])\equiv \mathcal{L}[u',\varvec{v}]\). Let \(u \simeq _{\mathcal {V}}^{\phantom {a}} u^{\prime }\) denote that \(u \simeq _{\mathcal {V}}^{\gamma } u^{\prime }\) for some bijection \(\gamma \). Intuitively, two words u and \(u'\) are equivalent if there is a bijection \(\gamma \) which, for each \(\varvec{v}\in \mathcal {V}\), transforms \(\mathcal{L}[u,\varvec{v}]\) to \(\mathcal{L}[u',\varvec{v}]\), Note that in general, when \(u \simeq _{\mathcal {V}}^{\phantom {a}} u^{\prime }\), there can be several such bijections in case \(\mathcal{L}[u,\varvec{v}]\) is symmetric w.r.t. some of its registers.
Definition 3
We define the data language \(\mathcal {L}\) to have finite index if \(\simeq _{\Sigma ^*}^{\phantom {a}}\) has a finite number of equivalence classes. \(\square \)
Recall that \(\Sigma ^*\) is the set of all symbolic suffixes. Definition 3 is a natural generalization of the concept of regular languages to the setting of data languages. The \({SL}^{\lambda } \) algorithm, presented in the next section, learns a data language with finite index using membership queries and equivalence queries.
4 The \(SL^\lambda \) Learning Algorithm
In this section, we present the learning model (Sect. 4.1), the main building blocks of \({SL}^{\lambda } \) (Sect. 4.2), an overview of the main algorithm (Sect. 4.3), the construction of hypothesis register automata (Sect. 4.4), the analysis of counterexamples (Sect. 4.5), and an extension for the theory with inequalities (Sect. 4.6). Given a data language \(\mathcal {L}\) of finite index, the \({SL}^{\lambda } \) algorithm will construct a register automaton that accepts \(\mathcal {L}\) using a finite sequence of membership and equivalence queries.
4.1 Learning Model
The \({SL}^{\lambda } \) algorithm is an active automata learning algorithm. It infers a register automaton that accepts an unknown data language \(\mathcal {L}\) over some set \(\Sigma \) of actions with the help of a minimally adequate teacher (MAT). The teacher answers two types of queries about \(\mathcal {L}\): membership queries and equivalence queries. A membership query asks if some data word w is in \(\mathcal {L}\) and is answered with yes or no. As discussed in the previous section, the \({SL}^{\lambda } \) algorithm uses membership queries to compute symbolic decision trees in tree queries. An equivalence query asks if some register automaton \(\mathcal {H}\) accepts \(\mathcal {L}\). If this is not the case, the teacher provides a counterexample from the symmetric difference of \(\mathcal {L}\) and \(\mathcal {L}(\mathcal {H})\). The \({SL}^{\lambda } \) algorithm uses counterexamples to refine \(\mathcal {H}\) by finding new locations, transitions, and/or registers.
The MAT learning model was introduced by Dana Angluin in 1987 when she showed that regular languages can be inferred efficiently from memberhip and equivalence queries [8] and has since proven to be a very useful model for separating two phases of the active learning process: constructing a hypothesis and validating this hypothesis.
In order to actually infer models of black box systems, the \({SL}^{\lambda } \) algorithm must be combined with a teacher. The teacher answers membership queries by testing the system. Since in a black box setting equivalence queries cannot be decided, a teacher will typically approximate equivalence queries by means of random testing or conformance testing. In such scenarios, often resets (i.e., sum of membership queries and tests for approximating equivalence queries) and input symbols sent to the system under learning are considered as performance metrics, instead of membership queries and equivalence queries.
4.2 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) a set of one-symbol extensions of the prefixes in \(S_p\), representing transitions; we use \({U}\), called the set of prefixes, to represent the union of \(S_p\) and the set of one-symbol extensions, and (iii) a suffix-closed set \(\mathcal {V}\) of symbolic suffixes.
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}\). For an inner node \(N\), let \(\textit{suff} (N)\) be its symbolic suffix, and for each node \(N\) let \(\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)}^{\phantom {a}}\) and leads to a node \(N'\), to which is assigned a representative prefix in its corresponding equivalence class. The representative prefix of \(N'\), denoted \(\textit{rp} (N')\), is chosen as the prefix that was first entered into the set of prefixes labeling \(N'\) when \(N'\) was a leaf (note that \(N'\) may still be a leaf). Each leaf node \(N\) is labeled by a set of prefixes, which are all in the same equivalence class of \(\simeq _{\mathcal {V}(N)}^{\phantom {a}}\). Thus, two prefixes that label different leaves, \(N\) and \(N'\), are guaranteed to be inequivalent, since they are separated by the symbolic suffixes in \(\mathcal {V}(\textit{lca} (N,~ N'))\), where \(\textit{lca} (N,~ N')\) is the lowest common ancestor node of \(N\) and \(N'\). We let \(\mathcal {U}\) denote the mapping, which maps each prefix \(u \in {U}\) to the classification tree leaf where it is contained. Thus, \(\mathcal {U}^{-1}(N)\) is the set of prefixes labeling \(N\). We let \(\mathcal {V}(u)\) denote \(\mathcal {V}(\mathcal {U}(u))\).
The insertion of a new prefix u into the classification tree CT is performed by procedure \(\textit{Sift} \) (cf. Algorithm 1). The procedure traverses CT from the root downwards. At each internal node \(N\), it checks whether \(u \simeq _{\mathcal {V}(N)}^{\phantom {a}} \textit{rp} (N')\) for any child \(N'\) of \(N\). If so, it continues the traversal at \(N'\) (Line 7), otherwise a new child of \(N\) is created as a leaf node \(N^{\textit{new} }\) with \(\textit{rp} (N^{\textit{new} }) = u\) (Line 10). When reaching a leaf \(N\), the mapping \(\mathcal {U}\) is updated to reflect that u has been sifted to \(N\) (Line 3). For illustration, in the classification tree in Fig. 4, \(\epsilon \) is the representative prefix of inner nodes \(\textsf{push}(p_1)\) and \(\textsf{push}(p_1)\textsf{push}(p_2)\) as it is the first prefix that was sifted down this path. The short prefix \(\textsf{push}(0)\) at the second leaf from right was sifted from the root to \(\textsf{push}(p_1)\) and then to \(\textsf{push}(p_1)\textsf{push}(p_2)\) as \(\textsf{push}(0) \simeq _{ \lbrace \epsilon \rbrace }^{\phantom {a}} \epsilon \) and \(\textsf{push}(0) \simeq _{ \lbrace \epsilon ,~\textsf{push}(p_1)\rbrace }^{\phantom {a}} \epsilon \). Since, however, \(\textsf{push}(0) \not \simeq _{ \mathcal {V} }^{\phantom {a}} \epsilon \) for \(\mathcal {V}= \lbrace \epsilon ,~\textsf{push}(p_1), \textsf{push}(p_1)\textsf{push}(p_2)\rbrace \), a new leaf was created and \(\textsf{push}(0)\) was made the representative prefix of the new leaf.
4.3 The \({SL}^{\lambda }\) Algorithm
The core of the \({SL}^{\lambda }\) algorithm, shown in Algorithm 2 on the next page, 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 (Line 1). It then sifts the empty prefix \(\epsilon \), thereby entering it into \({U}\) (Line 2). Thereafter, Algorithm 2 repeats a main loop in which CT is checked for a number of closedness and consistency properties (Line 3). 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 two procedures whose code is shown in Algorithm 1:
-
\(\textit{Expand} \) takes a prefix \(u \in {U}\) as argument. If u is not already in \({U}\) it is sifted (Line 13). Thereafter, u is entered into the set \(S_p\) of short prefixes (Line 14). Since each short prefix must have a set of one-symbol extensions in \({U}\), the procedure forms one-symbol extensions of form \(u\alpha (\texttt {d} _{u}^{g})\), which are entered into the classification tree by sifting (Line 17).
-
\(\textit{Refine} \) takes as arguments a leaf node \(N\) and a symbolic suffix \(\varvec{v}\). It replaces \(N\) by a new node \(N'\) labeled by \(\varvec{v}\) (Line 20) and sifts each prefix u in \(N\) (Line 21). The sifting will, among other things, construct \(\mathcal{L}[u,\varvec{v}]\) from a tree query. This can result in one or several of the following: (i) splitting the old node \(N\) into several equivalence classes which become children of \(N'\), (ii) refining the initial guards of \(N\), (iii) extending the set of registers in the location represented by \(N\), or (iv) reducing the set of symmetries between registers in that location.
Let us return to Algorithm 2 and consider the closedness and consistency properties that are checked starting at Line 3. In general, location and transition closedness ensure that CT is extended with prefixes for new locations and transitions that are discovered during the execution of the algorithm. However, the corresponding corrective updates do not always split any leaf in CT to form new locations, nor do they add guards to form new transitions. As a result, a leaf in CT may contain multiple short prefixes that are inequivalent, but have not yet been separated by a suffix. This is the job of the corrective action for location consistency, which splits leaves whenever a separating suffix can be formed. Similarly, a leaf may contain multiple one-symbol extensions that satisfy the same guard, which has not yet been split by a suffix; this is the job for transition consistency. In \({SL}^{\lambda }\), such a separating suffix can only be formed as a one-symbol extension of an existing suffix; this is the principle by which \({SL}^{\lambda } \) produces short suffixes, e.g., in comparison to \({SL}^{*} \).
Let us now describe the respective corrective updates in Algorithm 2. For a symbolic suffix \(\varvec{v}= \alpha _1'(p_1)\ldots \alpha _m'(p_m)\) and a parameterized symbol \(\varvec{\alpha }= \alpha (p)\), we use \(\varvec{\alpha }\varvec{v}\) to denote the extension of \(\varvec{v}\) by \(\varvec{\alpha }\) (i.e., \(\alpha (p_1) \alpha _1'(p_2)\ldots \alpha _m'(p_{m{0.6}{+}\!1})\)).
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\) (Line 4), one of its prefixes u is chosen for inclusion in \(S_p\) by calling \(\textit{Expand} (u)\) in Line 5, which also adds one-symbol extensions of u to \({U}\).
Transition Closedness is satisfied if for each short prefix u, action \(\alpha \), and initial guard g in \(\mathcal{G}_{\mathcal {V}(u)}(u,\alpha )\), the extension \(u{\alpha (\texttt {d} _{u}^{g})}\), using the representative data value \(\texttt {d} _{u}^{g}\), is in \({U}\). If this is not satisfied (Line 6), the missing \(u{\alpha (\texttt {d} _{u}^{g})}\) is added to \({U}\) by sifting into CT (Line 7).
Register Closedness is satisfied if for each pair of prefixes u and \(u\alpha (\texttt {d} )\) in \({U}\), the memorable parameters found for u contain the memorable parameters revealed by the suffixes for \(u\alpha (\texttt {d} )\), except for \(x_{|u|+1}\) (recall that \(|u|\) is the length of u). Register closedness guarantees that in a hypothesis \(\mathcal {H}\), values of registers in the location of \(u\alpha (\texttt {d} )\) can all be obtained by assignment from the registers in location u and the data value received in the transition between the locations represented by u and \(u\alpha (\texttt {d} )\). If it is not satisfied (Line 8), a symbolic suffix \(\varvec{v}\) for \(u\alpha (\texttt {d} )\) which reveals a missing register is prepended by \(\alpha (p_1)\) and added to the suffixes for u by calling \(\textit{Refine} (\mathcal {U}(u), \varvec{\alpha }\varvec{v})\), which will reveal the missing parameter (Line 9). For example, consider the classification tree in Fig. 11. Assume that \(u = \textsf{push}(0)\textsf{push}(1)\), \(\alpha (\texttt {d} )=\textsf{pop}(1)\) and \(\varvec{v}=\textsf{pop}(p_1)\). The suffix \(\varvec{v}\) reveals that register \(x_1=0\) is memorable, since \(\mathcal{L}[u\alpha (\texttt {d} ),\varvec{v}]\) contains the guard \(p_1=x_1\). The register \(x_1\) is not in the set of memorable parameters \(\textit{mem} _{\mathcal {V}(\!u)}(u)\), nor is it in \(\{x_3\}\), so we add the new suffix \(\varvec{\alpha }\varvec{v}= \textsf{pop}(p_1)\textsf{pop}(p_2)\) to \(\textsf{push}(0)\textsf{push}(1)\). If possible, we try to choose a shortest \(\varvec{v}\), and also restrict the parameters of \(\varvec{\alpha }\varvec{v}\) to reduce the cost of the tree query for \(\mathcal{L}[u,\varvec{\alpha }\varvec{v}]\), as will be elaborated in Sect. 7.
Location Consistency Analogously to consistency in the classic \(L^*\) algorithm, we split a leaf containing two short prefixes u, \(u'\) with \(u \simeq _{\mathcal {V}(N)}^{\gamma } u'\) in case their corresponding extensions are not equivalent, i.e., there is a \(g \in \mathcal{G}_{\mathcal {V}(u)}(u,\alpha )\) such that \(\mathcal {U}(u\alpha (\texttt {d} _{u}^{g})) \ne \mathcal {U}(u'\alpha (\texttt {d} _{u'}^{\gamma (g)}))\) (Line 10). For example, consider the classification tree in Fig. 9(top). The right node contains the two short prefixes \(\textsf{push}(0)\) and \(\textsf{push}(0)\textsf{push}(1)\). Their \(\textsf{push}\)-extensions with initial guard true (i.e., \(\textsf{push}(0)\textsf{push}(1)\) and \(\textsf{push}(0)\textsf{push}(1)\textsf{push}(2)\), respectively) are in different leaves — the \(\textsf{push}\)-extension of \(\textsf{push}(0)\) is in the left leaf while the \(\textsf{push}\)-extension of \(\textsf{push}(0)\textsf{push}(1)\) is in the right leaf. The splitting is done by calling \(\textit{Refine} (\mathcal {U}(u), \varvec{\alpha }\varvec{v})\), where \(\varvec{v}\) is the symbolic suffix labeling the common ancestor of the leaves of \(u\alpha (\texttt {d} _{u}^{g})\) and \(u'\alpha (\texttt {d} _{u'}^{\gamma (g)})\) (Line 11).
Transition Consistency is satisfied if all one-symbol extensions \(u\alpha (\texttt {d} )\) that satisfy some guard g in \(\mathcal{G}_{\mathcal {V}(u)}(u,\alpha )\) are sifted to the same leaf as the extension \(u\alpha (\texttt {d} _{u}^{g})\), and furthermore \(u{\alpha (\texttt {d} _{u}^{g})} \simeq _{\mathcal {V}(u{\alpha (\texttt {d} _{u}^{g})})}^{\textbf{id}} u{\alpha (\texttt {d} )}\). Transition consistency comes in two versions. Transition Consistency(a) considers the case when \(u\alpha (\texttt {d} )\) and \(u\alpha (\texttt {d} _{u}^{g})\) are sifted to different locations (Line 12). Then, the guard g should be split by calling \(\textit{Refine} (\mathcal {U}(u), \varvec{\alpha }\varvec{v})\), where \(\varvec{v}\) is the symbolic suffix labeling the common ancestor of the leaves of \(u\alpha (\texttt {d} _{u}^{g})\) and \(u\alpha (\texttt {d} )\) (Line 13). Transition Consistency(b) occurs when \(u\alpha (\texttt {d} _{u}^{g})\) and \(u\alpha (\texttt {d} )\) are sifted to the same leaf, but are not equivalent under the identity mapping between registers for some \(\varvec{v}\in \mathcal {V}(u{\alpha (\texttt {d} _{u}^{g})})\), and a tree query \(\mathcal{L}[u,\varvec{\alpha }\varvec{v}]\) reveals a different set of initial guards \(\mathcal{G}_{\lbrace \varvec{\alpha }\varvec{v}\rbrace }(u,\alpha )\) from those in \(\mathcal{G}_{\mathcal {V}(u)}(u,\alpha )\) (Line 14). Also here, the guard g should be split by calling \(\textit{Refine} (\mathcal {U}(u), \varvec{\alpha }\varvec{v})\) (Line 15). As an example of this special case of transition consistency, consider the language \(\mathcal {L}_{max}\) defined by the acceptor shown in Fig. 5, which computes the maximum of two input values.
Assume that location \(l_1\) has representative prefix \(\textsf{in}(0)\). Assume further that the classification tree contains prefixes \(u=\textsf{in}(0)\), \(u\alpha (\texttt {d} _u^{true})=\textsf{in}(0)\textsf{in}(1)\) and \(u\alpha (\texttt {d} )=\textsf{in}(0)\textsf{in}(-1)\). The prefixes \(u\alpha (\texttt {d} _u^{true})\) and \(u\alpha (\texttt {d} )\) both sift to location \(l_2\). However, the prefixes are not equivalent under the identity mapping for suffix \(\textsf{max}(p_1)\) as \(p_1\) is compared to \(x_1\) for \(u\alpha (\texttt {d} _u^{true})\), but to \(x_2\) for \(u\alpha (\texttt {d} )\). The \(g=true\) guard for the \(\textsf{in}\)-extension of \(\textsf{in}(0)\) must be split into the guards \(g_1=(p_1 \ge x_1)\) and \(g_2=(p_2 \le x_1)\) by a call to \(\textit{Refine} (\mathcal {U}(\textsf{in}(0)), \textsf{in}(p_1)\textsf{max}(p_2))\).
Register Consistency For some short prefix u with memorable values \(\textit{mem} _{\mathcal {V}(u)}(u)\), there may be symmetries in \(\mathcal{L}[u,\varvec{v}]\) for all \(\varvec{v}\in \mathcal {V}(u)\), i.e., for some nontrivial permutation \(\gamma \) on \(\textit{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 canonical acceptor for \(\mathcal {L}\), but we did not yet add a suffix that disproves it. Register consistency checks for the existence of such suffixes by comparing symmetries in u with the symmetries in its continuations \(u{\alpha (\texttt {d} )}\). If \(\gamma \) is a symmetry between memorable data values of u, but its restriction to the memorable data values of an extension \(u\alpha (\texttt {d} )\) is no longer a symmetry (Line 16), we can construct a suffix that breaks the symmetry \(\gamma \) also for u (Line 17). As an example, consider the classification tree in the right part of Fig. 6, representing the locations and transitions of an intermediate RA of the acceptor shown in the left part of Fig. 6. For the words in the leaf containing \(\alpha (1)\alpha (2)\), corresponding to location \(l_2\), there are symmetries for \(\simeq _{\lbrace \alpha (p_1)\rbrace }^{}\); namely, the tree query \(\mathcal{L}[\alpha (1)\alpha (2),\alpha (p_1)]\) is accepting both for \(p_1=x_1\) and for \(p_1=x_2\), exhibiting the symmetry \(\alpha (1)\alpha (2) \simeq _{\lbrace \alpha (p_1)\rbrace }^{\gamma } \alpha (1)\alpha (2)\), under the bijection \(\gamma = \lbrace x_1 \leftrightarrow x_2\rbrace \). However, this symmetry is not present in the continuation \(\alpha (1)\alpha (2)\beta (3)\), since the tree query \(\mathcal{L}[\alpha (1)\alpha (2)\beta (3),\beta (p_1)]\) reveals that only \(x_2\) is memorable. We must therefore construct a new symbolic suffix to break the symmetry in \(\alpha (1)\alpha (2)\). We do this by constructing a new suffix \(\beta (p_1)\beta (p_2)\) by prepending the suffix \(\beta (p_1)\), which breaks the symmetry in \(\alpha (1)\alpha (2)\), thereby resolving the register inconsistency.
We remark here that one difference to the \({SL}^{*}\) algorithm [17] is that \({SL}^{\lambda }\) establishes register consistency instead of relying on counterexamples for distinguishing symmetric registers.
4.4 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 even though there may exist multiple short prefixes for one location and symmetries between memorable data values.
Definition 4
(Hypothesis Construction) Let CT be a closed and consistent classification tree. Then the hypothesis automaton \(\mathcal {H}(CT)\) is the register automaton \((L, l_0, \mathcal {X}, \Gamma , \lambda )\), where
-
\(L\) is the set of leaves of CT,
-
\(l_0\) is the leaf containing the empty prefix \(\epsilon \),
-
\(\mathcal {X}\) maps each location \(l\in L\) to \(\textit{mem} _{\mathcal {V}(u)}(u)\); here and below we let u be \(\textit{rp} (l)\),
-
\(\lambda (l)=+\) if the leaf \(l\) is in the accepting subtree of the root, else \(\lambda (l)=-\), and
-
for each location \(l\), each action \(\alpha \), and guard g in \(\mathcal{G}_{\mathcal {V}(u)}(u,\alpha )\), there is a transition \(\langle l,\alpha (p),g,\pi ,l'\rangle \) such that \(u'=\textit{rp} (l')\) and
-
\(l' = \mathcal {U}(u{\alpha (\texttt {d} _{u}^{g})})\) is the target location, and
-
\(\pi : \textit{mem} _{\mathcal {V}(u')}(u') \rightarrow (\textit{mem} _{\mathcal {V}(u)}(u) \, \cup \, \lbrace p\rbrace )\) is defined as \([x_{{|u|+1}} \mapsto p] \circ \gamma ^{-1}\) for some \(\gamma \) with \(u\alpha (\texttt {d} _{u}^{g}) \simeq _{\mathcal {V}}^{\gamma } u'\). \(\square \)
-
In the above definition, recall that \(\textit{rp} (l)\) is the representative prefix of node \(l\), and that \(\textit{mem} _{\mathcal {V}(u)}(u)\) is the set of registers (memorable parameters) of u in CT.
4.5 Analysis of Counterexamples
When an equivalence query returns a counterexample w over which \(\mathcal {H}\) has a misclassifying initialized run
we process it as shown in Algorithm 3. Since each leaf can contain several short prefixes, the above run corresponds, in general, to several possible sequences of short prefixes \(u_0, u_1, \ldots , u_n\), with \(l_i = \mathcal {U}(u_i)\) for \(i = 0, \ldots , n\), implying that the i-th transition \( \langle l_{i{-}\!1},\mu _{i{-}\!1}\rangle \xrightarrow {\alpha _i(\texttt {d} _i)} \langle l_i,\mu _i\rangle \) corresponds to possibly several short prefixs \(u_{i{-}\!1}\) with \(l_{i{-}\!1} = \mathcal {U}(u_{i{-}\!1})\), several one-symbol extensions \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) with \(l_{i} = \mathcal {U}(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')})\) of each \(u_{i{-}\!1}\), and several short prefixes \(u_i\) with \(l_i = \mathcal {U}(u_i)\). Let \(g_i\) be the guard of the transition in the hypothesis, from which \( \langle l_{i{-}\!1},\mu _{i{-}\!1}\rangle \xrightarrow {\alpha _i(\texttt {d} _i)} \langle l_i,\mu _i\rangle \) is derived. The objective of Algorithm 3 is to find, for some index i from n down to 1, a one-symbol extension \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) of some short prefix \(u_{i{-}\!1} \in \mathcal {U}^{{-}1}(l_{i{-}\!1})\) satisfying some guard corresponding to \(g_i\), which is either (i) inequivalent to all other one-symbol extensions of \(u_{i{-}\!1}\) in \(l_i\), implying that a new guard must be created, or (ii) inequivalent to all short prefixes in \(l_i\), implying that a new location must be created.
For Algorithm 3, we introduce some new notation for mappings between prefixes. For each prefix u in a leaf \(N\), we let \(\rho _{u}\) denote a bijection under which \(u \simeq _{\mathcal {V}(N)}^{\rho _{u}} \textit{rp} (N)\). Furthermore, we will let \(\rho _{u \mapsto u'}\) denote the bijection \(\rho _{u'}^{-1} \circ \rho _{u}\) such that if \(u \simeq _{\mathcal {V}(N)}^{\rho _{u}} \textit{rp} (N)\) and \(u' \simeq _{\mathcal {V}(N)}^{\rho _{u'}} \textit{rp} (N)\) then \(u \simeq _{\mathcal {V}(N)}^{\rho _{u \mapsto u'}} u'\). Thus, \(\simeq _{\mathcal {V}(N)}^{\rho _{u \mapsto u'}}\) specializes to \(\rho _{u}\) if \(u'\) is the representative prefix, and to \(\rho _{u'}^{-1}\) if u is the representative prefix.
For each \(u_{i{-}\!1}\) with \(l_{i{-}\!1} = \mathcal {U}(u_{i{-}\!1})\) and \(\varvec{v}_{i{-}\!1} = \alpha _i \alpha _{i{0.6}{+}\!1} \cdots \alpha _n\), Algorithm 3 constructs \(\mathcal{L}[u_{i{-}\!1},\varvec{v}_{i{-}\!1}]\) (in the for loop of Line 6). For brevity, we often omit the formal parameters in suffixes. The algorithm must then find one or several guards \(g_i'\) in \(\mathcal{G}_{\lbrace \varvec{v}_{i{-}\!1}\rbrace }(u_{i{-}\!1},\alpha _i)\) which correspond to \(g_i\). The correspondence between registers of \(u_{i{-}\!1}\) and data values in \(w_{1:i{-}\!1}\) is given by the valuation \(\mu _{i{-}\!1} \circ \rho _{u_{i{-}\!1}}\) If all registers in \(\textit{mem} _{\lbrace \varvec{v}_{i{-}\!1}\rbrace }(u_{i{-}\!1})\) are already present in \(\textit{mem} _{\mathcal {V}(l_{i{-}\!1})}(u_{i{-}\!1})\), then we can evaluate the guards in \(\mathcal{G}_{\lbrace \varvec{v}_{i{-}\!1}\rbrace }(u_{i{-}\!1},\alpha _i)\) under the valuation \(\mu _{i{-}\!1} \circ \rho _{u_{i{-}\!1}}\) and select a guard satisfied by \(\texttt {d} _i\) as \(g_i'\). If, however, \(\textit{mem} _{\lbrace \varvec{v}_{i{-}\!1}\rbrace }(u_{i{-}\!1})\) does contain new registers, we must consider that it is unknown how registers in \(\textit{mem} _{\lbrace \varvec{v}_{i{-}\!1}\rbrace }(u_{i{-}\!1}) \setminus \textit{mem} _{\mathcal {V}(l_{i{-}\!1})}(u_{i{-}\!1})\) correspond to data values in \(w_{1:i{-}\!1}\). We must then consider all possible \(g_i'\) for which there is an extension \(\nu _i\) of \(\mu _{i{-}\!1} \circ \rho _{u_{i{-}\!1}}\) with domain \((\textit{mem} _{\lbrace \varvec{v}_{i{-}\!1}\rbrace }(u_{i{-}\!1}) \cup \textit{mem} _{\mathcal {V}(l_{i{-}\!1})}(u_{i{-}\!1}))\) and range \(w_{1:i{-}\!1}\), such that \(\nu _i \models g_i'[\texttt {d} _i/p_1]\) (Line 7). For each such \(g_i'\), the guard \((\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')\) characterizes the data values that may correspond to \(\texttt {d} _i\) in w. Algorithm 3 thus searches for a one-symbol extension of \(u_{i{-}\!1}\) satisfying the guard \((\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')\) for which a discrepancy is found of one of the following two forms:
- New Transition.:
-
There is no one-symbol extension \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) of \(u_{i{-}\!1}\) in the leaf of \(l_i\) which is equivalent to \(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\) (Line 8). This signifies that \(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\) corresponds to a new, previously unknown, transition from \(l_{i{-}\!1}\) to \(l_i\). In this case, we add \(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\) to \({U}\) by sifting it (Line 9). The sifting can result in several subsequent outcomes:
-
\(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\) creates a new leaf. Then it will eventually induce a new location, by location closedness.
-
\(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\) sifts to a leaf different from that of \(l_i\). This will eventually induce a new transition, following transition(a)-consistency.
-
\(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\) sifts to the leaf of \(l_i\). This will eventually induce a new transition, either
-
(i)
following transition(b)-consistency, since it has already been checked that for all \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')} \in \mathcal {U}^{{-}1}(l_i)\), implying (since \(g_i'\) is the guard induced by \(\lbrace \varvec{v}_i\rbrace \)), or
-
(ii)
following register consistency if \(u_{i{-}\!1} \simeq _{\mathcal {V}(u_{i{-}\!1})}^{\gamma } u_{i{-}\!1}\) for some symmetries \(\gamma \) which are not witnessing \(u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})} \simeq _{\lbrace \varvec{v}_i\rbrace }^{} u_{i{-}\!1}{\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{(\rho _{u_{i{-}\!1}}^{-1}(g_i) \wedge g_i')})}\).
-
(i)
- New Location.:
-
A one-symbol extension \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) already in \(l_i\) is inequivalent to all short prefixes in \(l_i\) (Line 12). In this case, we make \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) a new short prefix, and expand it (Line 13). This new prefix will eventually induce a new location, by the rule for location consistency. This can either happen immediately, if there are one-symbol extensions that separate \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) from the already exiting short prefixes in \(l_i\). Otherwise, if no refinement results from making \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) a new short prefix, then when the counterexample w is analyzed again, a one-symbol extension of \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) will be added to location \(l_{i{0.6}{+}\!1}\), and so on, until a sufficiently long extension of \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) will induce a location by location consistency; when this happens, the location consistency will propagate the creation of new locations backwards until \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) induces a new location. An illustration of this mechanism was presented in Sect. 2, when we discussed how the counterexample to the hypothesis \(\mathcal {H}_0\) is processed.
If neither case applies, we continue with the next index. Since the run is misclassifying, one of the cases will apply for some index, as established in Lemma 6.
4.6 Extension for the Theory with Inequalities
In the theory \(\langle \mathbb {R}, \{ < \} \rangle \) of real numbers with inequality, Algorithm 2 should be modified to handle the following situation: Let \(N\) be a leaf node in CT with representative prefix u, and let \(\mathcal {V}(N)\) contain two symbolic suffixes \(\varvec{v}\) and \(\varvec{v}'\) with the same first action \(\alpha \). Recall that the guards \(\mathcal{G}_{\mathcal {V}(N)}(u,\alpha )\) on \(\alpha \)-transitions from the location induced by \(N\) are constructed as the pairwise conjunctions of a guard in \(\mathcal{G}_{\lbrace \varvec{v}\rbrace }(u,\alpha )\) with a guard in \(\mathcal{G}_{\lbrace \varvec{v}'\rbrace }(u,\alpha )\). In the case that the sets \(\mathcal{G}_{\lbrace \varvec{v}\rbrace }(u,\alpha )\) and \(\mathcal{G}_{\lbrace \varvec{v}'\rbrace }(u,\alpha )\) are different, it may happen that some of these conjunctions, say g, are unsatisfiable after u, but satisfiable after another prefix \(u'\) which is also in \(N\). We then need a mechanism for constructing \(\alpha \)-transitions with guard g from the location induced by \(N\), in spite of the fact that such a transition cannot be obtained from any one-symbol extension of u. It should be noted that a situation like this one is not expected to occur very frequently; for example, it does not arise in any of the benchmarks of Sect. 8.
As an example, assume that \(\mathcal{G}_{\lbrace \varvec{v}\rbrace }(u,\alpha ) = \mathcal{G}_{\lbrace \varvec{v}\rbrace }(u',\alpha ) = \lbrace p < x_1, p\ge x_1\rbrace \) and that \(\mathcal{G}_{\lbrace \varvec{v}'\rbrace }(u,\alpha ) = \mathcal{G}_{\lbrace \varvec{v}'\rbrace }(u,\alpha ) = \lbrace p < x_2, p\ge x_2\rbrace \). The pairwise conjunctions of these sets of guards are: (1) \(p< x_1 \wedge p < x_2\), (2) \(x_2 \le p < x_1\), (3) \(x_1 \le p < x_2\), and (4) \(x_1 \le p \wedge x_2 \le p\). Now, if \(u = \alpha _1(3)\alpha _2(5)\) and \(u' = \alpha _1(5)\alpha _2(3)\), then conjunction (2) is unsatisfiable after u and conjunction (3) is unsatisfiable after \(u'\). If u is the representative prefix in its node, then there is no extended prefix of form \(u\alpha (\texttt {d} )\) to represent the guard \(x_2 \le p < x_1\). On the other hand, since \(u'\) is equivalent to u and has an extension for the guard \(x_2 \le p < x_1\), then, since the location represented by u is also reachable via \(u'\), it must have an outgoing transition for this guard.
To address this situation, the set of prefixes in CT is extended to optionally include a set of auxiliary prefixes (APs), whose function is to provide one-symbol extensions for guards that are not satisfiable after any of the (regular) short prefixes in a location. Thus, if the hypothesis construction finds a guard g that is unsatisfiable after \(\textit{rp} (l)\) (such as the guard \(x_2 \le p < x_1\) after u above), then a transition is derived from \(u'\alpha (\texttt {d} _{u'}^{g})\) if there is an AP \(u' \in \mathcal {U}^{{-}1}(l)\) after which g is satisfiable. If there is no such AP, then a transition for g is generated, leading to the sink location. In the just described example, the prefix \(u'\) can be included as an AP which is sifted into the same leaf as u, and a one-symbol extension of \(u'\) can induce a transition for the guard \(x_2 \le p < x_1\).
Auxiliary prefixes are entered into CT during counterexample analysis as follows. If, when analyzing the i-th transition in a misclassifying run, CT contains no short prefix of form \(u_{i{-}\!1}\alpha _i(\texttt {d} _{u_{i{-}\!1}}^{g_i})\) that induces a transition from \(l_{i{-}\!1}\) for guard \(g_i\), the corresponding prefix \(w_{1:i{-}\!1}\) of the counterexample is sifted into CT as an auxiliary prefix. If \(w_{1:i{-}\!1}\) is sifted to the same leaf as u, then its extension \(w_{1:i{-}\!1}\alpha (\texttt {d} _{w_{1:i{-}\!1}}^{g})\) is also sifted to determine the corresponding target location. After entering CT, an AP is treated in the same way as ordinary prefixes, but with certain restrictions:
-
1.
Their influence on hypothesis construction is limited to providing one-symbol extensions when ordinary short suffixes cannot, as described above.
-
2.
They can never be promoted to a short prefix by an Expand operation (this would violate the principle that short prefixes can be organized into a spanning tree). Should a leaf \(N\) happen to contain only APs, then one of these APs is considered as a counterexample, and Algorithm 3 is invoked to extend CT, considering that the counterexample consists of that AP followed by the symbolic suffix that made \(N\) contain only APs. This will eventually introduce a regular short prefix into CP for node \(N\), which fits into the spanning tree.
5 Demonstration
In Sect. 2 we gave an intuition of how \({SL}^{\lambda }\) learns the acceptor shown in Fig. 1 for the language \(\mathcal {L}_{Stack}\) of a stack of capacity two. In this section, we return to \(\mathcal {L}_{Stack}\) for a full demonstration of the \({SL}^{\lambda }\) algorithm. We will demonstrate how \({SL}^{\lambda }\) uses counterexamples to find new locations and transitions and how to handle register closedness. This demonstration will consider only \(\langle \mathbb {N}, \{=\}\rangle \), the theory of natural numbers with equality. The algorithm begins by initializing the data structures, setting \({U}=\emptyset \) and \(S_p=\emptyset \), and letting CT consist of a single inner node labeled by the suffix \(\epsilon \). We sift the prefix \(\epsilon \) into CT, which results in a new leaf node, \(\mathcal {U}(\epsilon )\), being created. We then enter the main loop of Algorithm 2. The check for location closedness reveals that \(\mathcal {U}(\epsilon )\) does not contain a short prefix in \(S_p\), so we call \(\textit{Expand} (\epsilon )\), and sift \(\textsf{push}(0)\) and \(\textsf{pop}(0)\) into CT. After an additional check for location closedness, we end up with a CT as shown in Fig. 7. At this point, all of the closedness and consistency checks pass, so we exit the main loop and construct the initial hypothesis \(\mathcal {H}_0\), shown in Fig. 3.
New Locations and Location Consistency
Assume that after validation, the counterexample \(w=\textsf{push}(3)\textsf{push}(7)\textsf{push}(5)\) is found, with a misclassifying run
which shows that a run of w over \(\mathcal {H}_0\) transitions to location \(\mathcal {U}(\epsilon )\). This run is misclassifying, since \(\mathcal {U}(\epsilon )\) is an accepting location, whereas w is rejected by \(\mathcal {L}\). As per Algorithm 3, we analyze each transition of this misclassifying run from right to left. Let us illustrate the first run of Algorithm 3, initially considering only the location cases (Line 12 of Algorithm 3). The transition case will be covered later on in the demonstration. Table 1 shows a breakdown of \(\varvec{v}_i\), \(u_{i{-}\!1}\), \(u_{i{-}\!1}{\alpha _i(\texttt {d} _i')}\) and \(u_i\), as well as the SDTs of \(\mathcal{L}[u_{i{-}\!1}{\alpha _i(\texttt {d} _i')},\varvec{v}_i]\) and \(\mathcal{L}[u_i,\varvec{v}_i]\), for each i. For this initial hypothesis, the misclassifying run only touches the leaf \(\mathcal {U}(\epsilon )\), which contains only a single short prefix, \(\epsilon \). Hence \(u_i = \epsilon \) for each i.
For \(u_0{\alpha _1(\texttt {d} _1')}=\textsf{push}(0)\) and \(\varvec{v}_1=\textsf{push}(p_1)\textsf{push}(p_2)\) we find that \(\mathcal{L}[u_0{\alpha _1(\texttt {d} _1')},\varvec{v}_1]\) looks like , whereas, for all choices of \(u_1\) (i.e., \(\epsilon \)), \(\mathcal{L}[u_1,\varvec{v}_1]\) looks like . Since these SDTs are not equivalent under any bijection, thereby satisfying the condition of Line 12 of Algorithm 3, we have found the discrepancy \(\textsf{push}(0) \not \simeq _{\lbrace \textsf{push}(p_1)\textsf{push}(p_2)\rbrace }^{\phantom {a}} \epsilon \), so we call \(\textit{Expand} (\textsf{push}(0))\) (in Line 13 of Algorithm 3), resulting in CT as shown in Fig. 8.
At this point, all consistency checks of Algorithm 2 pass, so while we know that \(\textsf{push}(0)\) is not the same location as \(\epsilon \), we do not yet have a symbolic suffix that will separate \(\textsf{push}(0)\) and \(\epsilon \). We continue with the counterexample analysis. The run
is still a misclassifying run, so we analyze each transition of this run from right to left, as shown in Table 2.
We find that \(\mathcal{L}[\textsf{push}(0)\textsf{push}(1),\textsf{push}(p_1)]\) looks like , whereas \(\mathcal{L}[\epsilon ,\textsf{push}(p_1)]\) and \(\mathcal{L}[\textsf{push}(0),\textsf{push}(p_1)]\) both look like . Since \(\textsf{push}(0)\textsf{push}(1) \not \simeq _{\lbrace \textsf{push}(p_1)\rbrace }^{\phantom {a}} u_2\) for all \(u_2 \in \mathcal {U}(\textsf{push}(0)\textsf{push}(1))\), we have found a discrepancy, and call \(\textit{Expand} (\textsf{push}(0)\textsf{push}(1))\). This results in CT as in Fig. 9 (top).
After expanding \(\textsf{push}(0)\textsf{push}(1)\), it is still the case that \(\textsf{push}(0) \simeq _{\mathcal {V}(\textsf{push}(0))}^{\phantom {a}} \textsf{push}(0)\textsf{push}(1)\). However, note that when examining the \(\textsf{push}\)-continuations, we find that \(\mathcal {U}(\textsf{push}(0)\textsf{push}(1)) \ne \mathcal {U}(\textsf{push}(0)\textsf{push}(1)\textsf{push}(2))\). The \(\textsf{push}\)-continuation of \(\textsf{push}(0)\) is in leaf \(\mathcal {U}(\epsilon )\), while the \(\textsf{push}\)-continuation of \(\textsf{push}(0)\textsf{push}(1)\) is in leaf \(\mathcal {U}(\textsf{pop}(0))\). CT therefore violates location consistency (Line 10 of Algorithm 2). We construct a separating symbolic suffix \(\varvec{\alpha }\varvec{v}=\textsf{push}(p_1)\) by concatenating the action \(\textsf{push}\) and the suffix of the lowest common ancestor, \(\epsilon \). We then add the separating suffix to \(\mathcal {U}(\textsf{push}(0))\) with a call to \(\textit{Refine} (\mathcal {U}(\textsf{push}(0)), \textsf{push}(p_1))\), resulting in the classification tree as shown in Fig. 9 (bottom). Note that \(\textsf{push}(0)\textsf{push}(1)\) has now been split from \(\mathcal {U}(\textsf{push}(0))\) into its own leaf.
But there is still a location inconsistency. While \(\epsilon \simeq _{\mathcal {V}(\epsilon )}^{\phantom {a}} \textsf{push}(0)\), when examining the \(\textsf{push}\)-continuations, we find that \(\mathcal {U}(\textsf{push}(0)) \ne \mathcal {U}(\textsf{push}(0)\textsf{push}(1))\). We construct a separating suffix \(\varvec{\alpha }\varvec{v}=\textsf{push}(p_1)\textsf{push}(p_2)\) by appending the \(\textsf{push}\) action with the suffix of the lowest common ancestor of \(\textsf{push}(0)\) and \(\textsf{push}(0)\textsf{push}(1)\), which is \(\textsf{push}(p_1)\). After adding the new separating suffix to \(\mathcal {U}(\epsilon )\) with a call to \(\textit{Refine} (\mathcal {U}(\epsilon ), \textsf{push}(p_1)\textsf{push}(p_2))\), we end up with a classification tree CT as was shown in Fig. 4. Now CT is closed and consistent, so we can construct the next hypothesis, \(\mathcal {H}_1\), which was shown in Fig. 3. At this point, \(\mathcal {H}_1(w) = \mathcal {L}(w)\), so \(w = \textsf{push}(3)\textsf{push}(7)\textsf{push}(5)\) is no longer a counterexample.
New Transitions and Transition Consistency
Assume that in the validation of \(\mathcal {H}_1\), \({SL}^{\lambda }\) finds a counterexample \(w=\textsf{push}(5)\textsf{pop}(5)\), which is accepted by \(\mathcal {L}_{Stack}\) but rejected by \(\mathcal {H}_1\). We have a misclassifying run
and, once again, we analyze the counterexample by examining the transitions from right to left.
Let us examine the transition at index \(i=2\). The tree query \(\mathcal{L}[\textsf{push}(5),\textsf{pop}(p_1)]\) reveals the initial guards
Replacing \(p_1\) with 5, there is no extension of \(\mu _1\) (i.e., \(\emptyset \)) such that \(5 \ne x_1\) is satisfied, but there is an extension \(\{x_1 \mapsto 5\}\) of \(\mu _1\) for which \(5 = x_1\) is satisfied, so we let \(g_2' = (p_1 = x_1)\) at Line 7 of Algorithm 3. The corresponding transition in \(\mathcal {H}_1\),
has guard \(g_2=true\) (Line 5 of Algorithm 3). The conjunction, \({ true}\wedge (p_1 = x_1)\), of \(\rho _{\textsf{push}(0)}^{-1}(g_2)\) and \(g_2'\) has representative data value \(\texttt {d} _{\textsf{push}(0)}^{{ true}\wedge (p_1 = x_1)}=0\), so \(u_1{\alpha _2(\texttt {d} _{\textsf{push}(0)}^{{ true}\wedge (p_1 = x_1)})} = \textsf{push}(0)\textsf{pop}(0)\).
As seen in Fig. 9, the only prefix of form \(\textsf{push}(0){\textsf{pop}(d_2')}\) in \(\mathcal {U}^{{-}1}(\textsf{pop}(0))\) is \(\textsf{push}(0)\textsf{pop}(1)\). A tree query reveals that , whereas . We therefore conclude (Line 8 of Algorithm 3) that \(\textsf{push}(0)\textsf{pop}(0)\) corresponds to a new, previously unknown, transition. Therefore, we sift \(\textsf{push}(0)\textsf{pop}(0)\) into CT, which ends up as shown in Fig. 10(top).
Now we have a case of transition inconsistency, type (a), according to Line 12 of Algorithm 2. Note that the data values of both \(\textsf{pop}\)-continuations (\(\textsf{push}(0)\textsf{pop}(1)\) and \(\textsf{push}(0)\textsf{pop}(0)\)) are satisfied by the guard true for the corresponding transition in \(\mathcal {H}_1\). However, \(\textsf{push}(0)\textsf{pop}(1) \in \mathcal {U}^{{-}1}(\textsf{pop}(0))\), while \(\textsf{push}(0)\textsf{pop}(0) \in \mathcal {U}^{{-}1}(\epsilon )\). In other words, \(\mathcal {U}(\textsf{push}(0)\textsf{pop}(1)) \ne \mathcal {U}(\textsf{push}(0)\textsf{pop}(0))\). We resolve the inconsistency by constructing a symbolic suffix \(\varvec{\alpha }\varvec{v}=\textsf{pop}(p_1)\) by concatenating the \(\textsf{pop}\) action and the lowest common ancestor of \(\mathcal {U}(\textsf{pop}(0))\) and \(\mathcal {U}(\epsilon )\), i.e., \(\epsilon \). After a call to \(\textit{Refine} (\mathcal {U}(\textsf{push}(0)), \textsf{pop}(p_1))\), we end up with a classification tree CT as shown in Fig. 10(bottom). At this point, CT is closed and consistent, so we can construct the next hypothesis \(\mathcal {H}_2\), shown in Fig. 3(bottom).
The other \(\textsf{pop}\) transition from \(l_3\) to \(l_2\) can be found in a similar manner through the analysis of e.g., the counterexample \(\textsf{push}(3)\textsf{push}(7)\textsf{pop}(7)\textsf{pop}(3)\).
Register Closedness
Let us fast forward a bit and assume that, through counterexample analysis, we have discovered all of the locations and transitions of the acceptor in Fig. 1, resulting in a classification tree CT as shown in Fig. 11. Now CT is location and transition closed and consistent. However, it is not register closed (Line 8 of Algorithm 2). A tree query for \(\textsf{push}(0)\textsf{push}(1)\) with suffix \(\textsf{pop}(p_1)\) reveals that \(x_2\) is memorable. The other suffixes of \(\textsf{push}(0)\textsf{push}(1)\) (\(\epsilon \) and \(\textsf{push}(p_1)\)) do not reveal any registers at all, from which we conclude that \(x_2\) is the only memorable register for \(\textsf{push}(0)\textsf{push}(1)\). However, for the \(\textsf{pop}\)-continuation \(\textsf{push}(0)\textsf{push}(1)\textsf{pop}(1)\), we find that \(x_1\) is memorable. Since \(x_1\) is not in \(\textit{mem} _{\mathcal {V}(\textsf{push}(0)\textsf{push}(1))}(\textsf{push}(0)\textsf{push}(1))\), we must find a suffix revealing \(x_1\) for \(\textsf{push}(0)\textsf{push}(1)\). We construct this suffix analogously to the location and transition consistency cases above. The register \(x_1\) is revealed for \(\textsf{push}(0)\textsf{push}(1)\textsf{pop}(1)\) by suffix \(\varvec{v}=\textsf{pop}(p_1)\) and lost in the \(\textsf{pop}\)-continuation of \(\textsf{push}(0)\textsf{push}(1)\), so we construct suffix \(\varvec{\alpha }\varvec{v}=\textsf{pop}(p_1)\textsf{pop}(p_2)\). Adding this suffix with a call to \(\textit{Refine} (\textsf{push}(0)\textsf{push}(1),\textsf{pop}(p_1)\textsf{pop}(p_2))\) results in a classification tree as shown in Fig. 12.
After all this, the classification tree is closed and consistent, allowing us to construct the acceptor shown in Fig. 1.
6 Correctness and Complexity
In this section, we provide the correctness arguments and query complexity of \({SL}^{\lambda }\).
6.1 Correctness
The correctness arguments are analogous to the arguments presented for other active learning algorithms.
Theorem 1
\({SL}^{\lambda }\) infers a register automaton for data language \(\mathcal {L}\) of finite index using a finite number of membership and equivalence queries.
To prove Theorem 1, we will first prove the following invariants, each in a separate lemma, establishing correspondences between CT and \(\mathcal {L}\) after each round of counterexample analysis.
-
1.
\({SL}^{\lambda } \) correctly partitions \({U}\) into equivalence classes induced by the suffixes in \(\mathcal {V}\).
-
2.
If \(u,u' \in S_p\) and \(\mathcal {U}(u)=\mathcal {U}(u')\), then there exists a suffix separating u and \(u'\).
-
3.
For any short prefix \(u \in S_p\), \(\alpha \in \Sigma \) and \(g\in \mathcal{G}_{\mathcal {V}(u)}(u,\alpha )\), for each \(u{\alpha (\texttt {d} )}\) in \(\mathcal {U}(u{\alpha (\texttt {d} _{u}^{g})})\), there is a u-guard \(g'\) and symbolic suffix \(\varvec{v}\) such that
-
\(\texttt {d} \) is \(\texttt {d} _{u}^{g'}\), and
-
for all \(\texttt {d} '\) different from \(\texttt {d} \) with \(u{\alpha (\texttt {d} ')}\) in \(\mathcal {U}(u{\alpha (\texttt {d} _{u}^{g})})\).
-
We begin with the first lemma, which loosely states that two prefixes in CT are equivalent w.r.t. the symbolic suffixes used to sift them if and only if they are in the same leaf.
Lemma 2
Let \(N\) be a leaf, \(u \in \mathcal {U}^{{-}1}(N)\) and \(u' \in {U}\). Then \(u' \in \mathcal {U}^{{-}1}(N)\) iff \(u' \simeq _{\mathcal {V}(N)}^{\phantom {a}} u\).
Proof
We will prove that \(u' \in \mathcal {U}^{{-}1}(N)\) iff \(u' \simeq _{\mathcal {V}(N)}^{\phantom {a}} \textit{rp} (N)\); the proof of Lemma 2 follows from transitivity. Let \(N_0,\ldots ,N_k\) be the k ancestors of \(N\), ordered from the root to the immediate ancestor of N, and let \(N_{k+1}\) denote \(N\). This means that \(\mathcal {V}(N)=\lbrace \textit{suff} (N_i) ~:~ 0 \le i \le k\rbrace \). From the definition of \(\textit{Sift} \), it follows that
We will first prove, by contradiction, that \(u'\in \mathcal {U}^{{-}1}(N)\) implies \(u' \simeq _{\mathcal {V}(N)}^{\phantom {a}} \textit{rp} (N)\). Assume that \(u'\in \mathcal {U}^{{-}1}(N)\) but \(u' \not \simeq _{\mathcal {V}(N)}^{\phantom {a}} \textit{rp} (N)\). Then, there must exist a node \(N_i\) with \(0\le i\le k\) s.t. \(u' \not \simeq _{\textit{suff} (N_i)}^{\phantom {a}} \textit{rp} (N)\). From Eq. (1), it follows that \(u' \not \simeq _{\textit{suff} (N_i)}^{\phantom {a}} \textit{rp} (N_{i+1})\). But that means, from the definition of \(\textit{Sift} \), that \(u'\) could not have been sifted to \(N_{i+1}\). This contradicts, if \(i1\) in \(\varvec{\alpha }\varvec{v}\) to be
-
1.
fresh whenever \(p_{j-1}\) is fresh in \(\varvec{v}\) or the branch taken in \(\mathcal{L}[u{\alpha (\texttt {d} )},\varvec{v}]\) for fresh \(p_{j-1}\) reveals a sought register, or
-
2.
equal to a previous value \(p_{j'}\) in \(\varvec{\alpha }\varvec{v}\) if the branch taken in \(\mathcal{L}[u{\alpha (\texttt {d} )},\varvec{v}]\) when \(p_{j-1}\) is equal to the corresponding parameter (\(p_{j'-1}\) or \(\texttt {d} \)) in \({\alpha (\texttt {d} )}\varvec{v}\) reveals a sought register.
-
1.
As an illustration, assume that the prefix \(u\alpha (\texttt {d} )\) is \(\alpha (0)\alpha (1)\) and the symbolic suffix \(\varvec{v}\) is \(\alpha (p_2)\alpha (p_3)\) (in which we have proactively renamed the parameters to prepare its extension). Assume that \(\mathcal{L}[u{\alpha (\texttt {d} )},\varvec{v}]\), shown in Fig. 13, reveals the register \(x_1\) in \(\alpha (0)\alpha (1)\), i.e., \(x_1 \in \textit{mem} _{\varvec{v}}(\alpha (0)\alpha (1))\), but that \(x_1\) is not (yet) a register of \(\alpha (0)\). By the rule for register closedness (Line 9 of Algorithm 2), we should form the extended symbolic suffix \(\varvec{\alpha }\varvec{v}= \alpha (p_1)\alpha (p_2)\alpha (p_3)\) and construct \(\mathcal{L}[\alpha (0),\varvec{\alpha }\varvec{v}]\) to ensure that \(x_1 \in \textit{mem} _{\varvec{\alpha }\varvec{v}}(\alpha (0))\). Let us now investigate which restrictions can be imposed on \(\varvec{\alpha }\varvec{v}\). First, we can restrict \(p_1\) to be fresh, since the first data value in \(\varvec{\alpha }\varvec{v}\) does not equal any parameter in the prefix \(\alpha (0)\). Second, we can restrict \(p_2\) to be equal to \(p_1\), since the branch taken under this restriction in \(\mathcal{L}[u\alpha (\texttt {d} ),\varvec{v}]\) (the top one in Fig. 13) reveals the register \(x_1\). Finally, we note that \(p_3\) cannot be restricted as it does not satisfy either of the conditions (a) or (b). With the restrictions \(\textit{fresh} (p_1)\) on \(p_1\) and \(p_2=p_1\) on \(p_2\) in \(\varvec{\alpha }\varvec{v}\), three membership queries are required to compute \(\mathcal{L}[\alpha (0),\varvec{\alpha }\varvec{v}]\), as opposed to the fifteen required for an unrestricted \(\varvec{\alpha }\varvec{v}\).
The case of transition consistency (b), where two extended prefixes \(u{\alpha (\texttt {d} )}\) and \(u{\alpha (\texttt {d} ')}\) are in the same leaf but are not equivalent under the identity mapping between registers, is handled similarly to register consistency. Since \(u{\alpha (\texttt {d} )}\) and \(u{\alpha (\texttt {d} ')}\) are in the same leaf, \(\mathcal{L}[u{\alpha (\texttt {d} )},\varvec{v}]\) and \(\mathcal{L}[u{\alpha (\texttt {d} ')},\varvec{v}]\) are equivalent, but not under the identity mapping between registers. We therefore need only consider one of \(\mathcal{L}[u{\alpha (\texttt {d} )},\varvec{v}]\) and \(\mathcal{L}[u{\alpha (\texttt {d} ')},\varvec{v}]\) when imposing restrictions on \(\varvec{\alpha }\varvec{v}\). Note that in this case, one of \(\texttt {d} \) and \(\texttt {d} '\) will be equal to a parameter in u (since we are in the equality theory) so the parameter \(p_1\) of \(\varvec{\alpha }\) can not be restricted.
In the case of location consistency, we want to find a symbolic suffix \(\varvec{\alpha }\varvec{v}\) that separates two prefixes u and \(u'\). Therefore, when we restrict \(\varvec{\alpha }\varvec{v}\), we must do so in a way such that \(\varvec{\alpha }\varvec{v}\) retains its ability to separate u and \(u'\). Our overall strategy for this case is to impose restrictions of the forms we consider as long as the resulting decision trees separate u and \(u'\). The case of transition consistency (a) is handled similarly, with the only difference being that, in this case, \(u=u'\).
We finally remark that our optimizations can be made more aggressive by considering additional forms of restrictions, such as letting a parameter in the suffix be equal to a register, but such restrictions are left for future work.
8 Evaluation
We have implemented the \({SL}^{\lambda }\) algorithm in the publicly available RALib tool for learning register automata. RALib already implemented the \({SL}^{*}\) algorithm [17] that uses an observation table as its data structure. In order to evaluate the effect of analyzing counterexamples as described in Sect. 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. In this section, we compare the performance of \({SL}^{\lambda }\) against that of \({SL}^{*}\) and \({SL}^{CT}\) in three sets of experiments.
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. All models, the experimental setup, and infrastructure for executing the experiments are available on the artifact of the TACAS 2024 paper at Zenodo [67]. Possibly updated versions of them can be found on GitHubFootnote 2.
In all experiments, we report the number of resets, aggregating membership queries during learning and tests for approximating equivalence queries.
8.1 Evaluation on Black-box Automata Wiki Models
The first set of experiments examines \({SL}^{\lambda }\) ’s performance on the RA models contained in the Automata Wiki [62]. These include automata derived from real-world case studies, as well as models of protocols and data structures. We note that these models are quite small (at most 30 states and 72 transitions). We use a black-box learning setup with random walks for finding counterexamples to establish a baseline and demonstrate the impact of using non-minimal counterexamples.
In this set of experiments, equivalence queries were approximated by randomly extending words from the current set U of prefixes, covering all transitions of the current hypothesis, while comparing the behavior of the system under learning (SUL) and the hypothesis. We fixed a maximal number of these random walks, a maximal length of a walk, a probability of stopping after a step, and a probability of using a fresh data value in a step. The concrete configurations differ for different classes of systems (e.g., different probabilities for fresh values are used for models of data structures and models of protocols). As the counterexamples which are found may be longer or have more equal data values than necessary, we tried to remove equalities and shorten counterexamples heuristically before using them in a learning algorithm. We verified with a model checker that the inferred model is equivalent to the SUL, and stopped each experiment as soon as the correct model was produced by a learning algorithm.
Table 3 summarizes the results; all numbers are averages from 20 experiments. 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 during the learning phase (i.e., membership queries), the number of total resets (i.e., membership queries and tests for counterexample search), the number of counterexamples found, and wall clock times (WCT) for learning and testing. It can be seen that the \({SL}^{\lambda }\) algorithm consistently outperforms the other two algorithms in terms of 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 overall the fastest algorithm.
As mentioned, the SULs of this set of experiments are quite small (\(|\Gamma | \le 72\)). Also, with the exception of fifo, the benchmarks were not parametric. In the following sets of experiments, we scale up the SULs which are learned.
8.2 Evaluation on White-box Mbed TLS Models
To assess the algorithms on a realistic system, we benchmarked them on 24 consecutive hypotheses of the Mbed TLS 2.26.0 server implementation generated by using DTLS-Fuzzer [30], a publicly available tool for learning state machine models of DTLS implementations. The DTLS (Datagram Transport Layer Security) protocol is a variation of TLS over UDP. Widely used in wireless networks, DTLS is the primary protocol for securing IoT applications, with MbedTLS being one of its main implementations. Owing to its importance, DTLS, specifically version 1.2, has been extensively studied for the security of its implementations [24, 28, 29]. We applied RALib with \({SL}^{*}\) to learn the server implementation of MbedTLS 2.26.0. In this application, we employed the test harness developed for classical model learning of DTLS implementations [28], adapting them for register automata learning by making the supported inputs and outputs parametric. We stopped learning after three weeks seeing that it had not yet converged to a final model. We then used the competing algorithms to re-learn the 24 hypothesis models that learning generated. These experiments used a white-box learning setup, using a model checker for finding short counterexamples to analyze the examined algorithms’ performance and scalability.
Figure 14 shows the results of this set of experiments. 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 than 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.
8.3 Evaluation on White-Box Synthetic Models
The third set of experiments uses synthesized families of models. Purely random generation of transition structures is likely to yield automata that collapse into semantically identical automata that exhibit little complexity. For the synthesis process, we therefore first applied the Champarnaud and Paranthoën DFA synthesis algorithm [19] This algorithm results in automata that are almost certain to not collapse, i.e., a generation campaign will generate semantically different automata for the same alphabet and location set sizes. We then convert the resulting DFA into a simple RA without registers by replacing all DFA transitions with RA transitions. For each transition, the input symbol \(\alpha \) is replaced with a parameterized symbol \(\alpha (p)\) and a uniform guard (here, true) is used. The conversion process adds no registers to the RA, i.e., we add no assignments.
We then enhance the register automaton by inserting gadgets, i.e., mini-RAs that are difficult to learn. In each gadget, we select a most distant location, i.e., a location that has the maximum distance from the initial location w.r.t. @ the graph structure. To insert a gadget into a target RA, we first define a percentage of transitions in the target to replace. We then select a random subset (of correct size) of the target’s transitions that do not share sources or targets. Each transition is then replaced with a copy of the gadget, such that the gadget’s initial location corresponds to the transition’s source and its most distant location corresponds to the transition’s target. The gadgets are defined programatically; the layout used by us in shown in Fig. 15.
We then varied 1) the size of the base automaton and 2) the replacement share, i.e., the number of gadgets inserted into the base automaton. These experiments also used a white-box learning setup.
Figure 16 shows the results of the experiments with synthesized automata. The graphs show: (i) how the number of resets scales with the number of locations and actions (left) and (ii) the number of registers when using both restricted (center) and unrestricted suffixes (right). It can be observed that the number of resets grows much more rapidly for \({SL}^{*}\) than for the other algorithms. Not restricting suffixes leads to a 2–4\(\times \) increase in resets; notice the different scales on the y-axis.
8.4 Discussion
Overall, the experiments show a clear advantage of \({SL}^{\lambda }\) over table-based register automata learning algorithms in terms of the number of resets and execution times for bigger systems. They also show that the \({SL}^{*}\) algorithm needs fewer counterexamples on randomly generated systems where one symbolic suffix may distinguish many locations. This trend is less pronounced for the DTLS models. Finally, as can be seen in the experiments with the fifo models, learning is exponential in the number of registers in the worst case.
These results confirm the theoretical properties of the algorithms and are consistent with the behavior of active automata learning algorithms for FSMs.
9 Related Work
The main contribution of this work is a tree-based active automata learning algorithm for register automata. Related works focus on similar classes of automata and corresponding learning algorithms.
Classes of Extended Finite State Machines
Extended finite state machines (EFSMs) extend the control structure that can be expressed by finite automata with concepts for modeling data-dependent behavior (e.g., state variables, action parameters, transition guards, and update operations). Different classes of EFSMs differ in the concrete concepts they support and their respective expressivity. With arbitrary data operations, it becomes possible to completely encode the control states of a system in variables. Introducing data structures (e.g., stacks or counters) quickly leads to Turing complete models [58]. To establish useful notions of accepted languages and canonical models as well as decidability of interesting properties, it is necessary to restrict expressivity.
Register automata (RA) are automata models over infinite alphabets that usually restrict the operations on data (i.e., inputs from an infinite set) to storing and comparing. In their seminal work [50], Kaminski and Francez introduce finite-memory automata that can store inputs in uniquely-valued registers and compare register values and inputs for equality. Benedikt et al. [11] define a variant: minimal memory automata maintain one set of active registers per location and only store so-called memorable data values (i.e., values that affect acceptance when changed), a concept that is also fundamental for inferring RA models from observations. Nominal automata have the same expressivity, but rely on data symmetries (permutations on the data domain), instead of encoding data-related behavior explicitly [12]
Neven et al. [63] studied the relation between register automata, so-called pebble automata, and logics on strings over infinite alphabets. Their work [63] and work by Kaminski and Francez [50] established a number of results on the (un)decidability of non-emptiness and universality for variants of the studied automata. Murawski et al. [61] presented a polynomial-time algorithm for deciding language equivalence for some deterministic sub-classes. Recently, Balachander et al. [9] showed that equivalence can be decided in polynomial time for register automata with permutations, i.e. minimal memory automata with reassignments between uniquely valued registers.
Our work focuses on succinct canonical register automata [15], which are exactly as expressive as simple deterministic finite memory automata [21] but can be exponentially more succinct [15] by (a) allowing reassignments between registers and (b) by not requiring unique values in registers. The latter property allows succinct register automata to also be exponentially smaller than many other flavors of register automata. Additionally, while most automata classes that are derived from finite memory automata rely on very restricted transition guards (transitions can be enabled when a read value is not in any register or when a read value equals a particular register), succinct register automata use conjunctions and disjunctions of tests for equality, disequalities, and order between register values and input values as guards.
Some other works of the area focus on more expressive classes of register automata. Chen et al. [20] define register automata with linear arithmetic, allowing tests for equality and ordering as well as linear arithmetic on registers. They show that non-emptiness is decidable for this class of automata, while equivalence, commutativity, and reachability are undecidable. Alur et al. [6] introduce cost register automata that combine write-only registers and arithmetic operations to characterize a class of regular functions. Vaandrager and Midya [75] prove a Myhill-Nerode theorem for register automata with n-ary relations in guards and symbolic trace languages. While we focus on register automata with tests for equality and order in this work, it should be possible to extend the \({SL}^{\lambda }\) algorithm to some of these classes of automata, especially to classes where accepted languages induce finite equivalence relations over words.
Automata Learning Algorithms for Expressive Models
Active automata learning algorithms have been studied for almost four decades by now. For a broad overview of active automata learning, we refer the reader to the survey paper of de la Higuera [43] from 2005 and to a more recent paper by Howar and Steffen [44].
Applications of AAL are diverse. Active learning enables the generation of behavioral models for software [69, 72], e.g. for network protocol implementations [28, 66], enabling security analyses and model checking [5, 32, 33]. The models which are learned can be used in testing [56, 70] and to enable formal analyses of systems [74]. Finally, active automata learning can be combined with passive learning approaches to support life-long learning [35]. More theoretical advances include the use of Galois connections to model SUL-oracle mappers [52] and the introduction of apartness [77], to formalize state distinction.
Learning beyond FSMs has been investigated for many models aside from register automata. For example, algorithms have been presented for workflow Petri nets [26], data automata [37], generic nondeterministic transition systems [78], symbolic automata [23, 54], automata with timers [14, 76], sub-classes of timed automata [38], session automata [13], and systems of procedural automata [36]. Recent work [59] presents an adaptation of the algorithm to infer finite-state models of NetKAT programs in the form of symbolic automata.
Sakamoto [68] presented the first active learning algorithm for simple finite memory automata. The algorithm internally uses the classic \(L^*\) algorithm [8] to learn a finite state acceptor on a (growing) finite subset of the infinite alphabet and computes a deterministic finite memory automaton from the obtained hypothesis once it is closed under permutations on the alphabet. To the best of our knowledge, this algorithm was never implemented and evaluated. Recently, Frank et al. [34] proposed a similar technique for inferring so-called bar automata. These algorithms [34, 68] have polynomial query complexity, but on classes of models that are exponentially bigger than succinct register automata.
Active learning algorithms for nominal automata, which extend FSMs to infinite alphabets and infinite sets of states, use a similar approach based on permutation-closedness and a finite representation of the input alphabet [60]. However, the approach uses symbolic prefixes and suffixes. While the expressivity of nominal DFAs is equivalent to that of deterministic register automata with equality, one algorithm in the paper infers a subclass of nominal NFA, which are more expressive than deterministic register automata and also allow for a more compact representation than nominal DFA in some cases. On the other hand, nominal automata do not represent registers symbolically but through permutations on infinite sets of states, leading to big models (e.g., by not being able to store the same data value twice) and expensive active learning algorithms, as reported in experimental evaluations [60]. Recently, Balachander et al. presented the first passive learning algorithm for regular data languages [10], essentially extending RPNI [64] with the ability to infer memorable data values [11].
Most closely related to the work presented in this article are the bespoke RA learning algorithms [17, 47, 57] implemented in RALib [16]. The main difference between these algorithms and the work presented here is we use a tree-based data structure instead of an observation table and adapt the \(L^\lambda \) handling of counterexamples [45] instead of adding suffixes from counterexamples to the data structure. An alternative approach to the inference of succinct register automata has been performed by combining a FSM learner with the Tomte front-end [3, 4]. Tomte maintains and refines an abstraction that maps symbolic RA transitions to a finite alphabet for the learning algorithm.
Several other works also rely on two steps or components: a learning algorithm for finite state machines and an approach for inferring symbolic data constraints: Lorenzoli et al. [53] combine Daikon [25] with state merging in a passive learning setting. Ferreira et al. [27] combine a Mealy machine learner with a bespoke inference of data constraints in a second step. Groz et al. [39] extend the hW algorithm [41] for inferring finite automata with membership queries and equivalence queries in a learning model without resets to EFSMs by using (growing) finite sets of data values during learning and genetic programming (aka symbolic regression) to infer data constraints and register updates.
10 Conclusion
We have presented \({SL}^{\lambda }\), a scalable tree-based algorithm for register automata learning. In comparison to previous algorithms for the same task, \({SL}^{\lambda }\) reduces the number of membership queries needed for inferring RA models by (i) organizing prefixes and suffixes into a classification tree, (ii) constructing suffixes incrementally from inconsistencies in order to keep them short, and (iii) restricting suffixes by ignoring irrelevant data dependencies. We prove a reduction in the worst-case number of tests and show, using our implementation of \({SL}^{\lambda }\) in RALib, performance improvements on both synthetic and real-world models (i.e., of a complex network protocol implementation) compared to the state-of-the-art RA learning algorithm.
There are several directions for future work, including to develop (i) specializations of RA learning algorithms for specific theories or classes of systems, (ii) passive algorithms for inferring register automata based on concepts that underly \({SL}^{\lambda }\), and (iii) more efficient strategies for identifying counterexamples in equivalence queries.
Data Availability
The conference version of this article and thus also this one comes with a publicly available artifact: Sagonas, K., Jonsson, B., Howar, F., Dierl, S., Fiterău-Broştean, P., Tåquist, F.: Reproduction artifact for TACAS 2024 paper “Scalable tree-based register automata learning”, December 2023. Available at https://doi.org/10.5281/zenodo.10442556 In addition, the implementation of all algorithms described in the paper are publicly available in RALib (https://github.com/LearnLib/ralib
Notes
RALib is available at https://github.com/LearnLib/ralib
References
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, 1–41 (2015) https://doi.org/10.1007/s10703-014-0216-x
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, College Park, MA, USA (2012). http://proceedings.mlr.press/v21/aarts12a.html
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
Aarts, F., Fiterău-Broştean, 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, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_11
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 (2015). https://doi.org/10.1007/s10703-014-0216-x
Alur, R., D’Antoni, L., Deshmukh, J.V., Raghothaman, M., Yuan, Y.: Regular functions and cost register automata. In: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’13, pp. 13–22. IEEE Computer Society, Los Alamitos, CA (2013). https://doi.org/10.1109/LICS.2013.65
Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’02, pp. 4–16. ACM, New York, NY, USA (2002). https://doi.org/10.1145/503272.503275
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987). https://doi.org/10.1016/0890-5401(87)90052-6
Balachander, M., Filiot, E., Gentilini, R., Tzevelekos, N.: Register automata with permutations. In: 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol. 345, pp. 14–11418. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2025). https://doi.org/10.4230/LIPIcs.MFCS.2025.14
Balachander, M., Filiot, E., Gentilini, R.: Passive learning of regular data languages in polynomial time and data. In: 35th International Conference on Concurrency Theory (CONCUR). Leibniz International Proceedings in Informatics (LIPIcs), vol. 311, pp. 10–11021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2024). https://doi.org/10.4230/LIPIcs.CONCUR.2024.10
Benedikt, M., Ley, C., Puppis, G.: What you must remember when processing data words. In: Proceedings 4th Alberto Mendelzon International Workshop on Foundations of Data Management. CEUR Workshop Proceedings, vol. 619 (2010). http://ceur-ws.org/Vol-619/paper11.pdf
Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Logical Methods in Computer Science (2014). https://doi.org/10.2168/LMCS-10(3:4)2014
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, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38771-5_12
Bruyère, V., Garhewal, B., Pérez, G.A., Staquet, G., Vaandrager, F.W.: Active learning of Mealy machines with timers. In: Prabhakar, P., Vandin, A. (eds.) International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. LNCS, vol. 16143, pp. 42–61. Springer, Cham (2025). https://doi.org/10.1007/978-3-032-05792-1_3
Cassel, S., Howar, F., Jonsson, B., Merten, M., Steffen, B.: A succinct canonical register automaton model. J. Log. Algebr. Meth. Program. 84(1), 54–66 (2015). https://doi.org/10.1016/j.jlamp.2014.07.004
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
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
Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Extending automata learning to extended finite state machines. In: Bennaceur, A., Hähnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits - International Dagstuhl Seminar 16172, Revised Papers. LNCS, vol. 11026, pp. 149–177. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96562-8_6
Champarnaud, J.-M., Paranthoën, T.: Random generation of DFAs. Theoret. Comput. Sci. 330(2), 221–235 (2005). https://doi.org/10.1016/j.tcs.2004.03.072
Chen, Y., Lengál, O., Tan, T., Wu, Z.: Register automata with linear arithmetic. In: Proceedings of the 32nd ACM/IEEE Symposium on Logic in Computer Science. LICS ’17, pp. 1–12. IEEE Computer Society, Los Alamitos, CA (2017). https://doi.org/10.1109/LICS.2017.8005111
Dierl, S., Howar, F.: A taxonomy and reductions for common register automata formalisms. In: Model Checking, Synthesis, and Learning. LNCS, vol. 13030, pp. 186–218. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-91384-7_10
Dierl, S., Fiterău-Broştean, P., Howar, F., Jonsson, B., Sagonas, K., Tåquist, F.: Scalable tree-based register automata learning. In: Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Proceedings, Part II. LNCS, vol. 14571, pp. 87–108. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-57249-4_5
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
Erinola, N., Maehren, M., Merget, R., Somorovsky, J., Schwenk, J.: Exploring the unknown \(\{\)DTLS\(\}\) universe: Analysis of the \(\{\)DTLS\(\}\) server ecosystem on the internet. In: 32nd USENIX Security Symposium (USENIX Security 23), pp. 4859–4876. USENIX Association, Anaheim, CA (2023). https://www.usenix.org/conference/usenixsecurity23/presentation/erinola
Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007). https://doi.org/10.1016/j.scico.2007.01.015
Esparza, J., Leucker, M., Schlund, M.: Learning workflow Petri nets. Fund. Inform. 113(3–4), 205–228 (2011). https://doi.org/10.3233/FI-2011-607
Ferreira, T., Brewton, H., D’Antoni, L., Silva, A.: Prognosis: Closed-box analysis of network protocol implementations. In: Proceedings of the 2021 ACM SIGCOMM 2021 Conference, pp. 762–774. ACM, New York, NY, USA (2021). https://doi.org/10.1145/3452296.3472938
Fiterău-Broştean, P., Jonsson, B., Merget, R., 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, Boston, MA, USA (2020). https://www.usenix.org/conference/usenixsecurity20/presentation/fiterau-brostean
Fiterău-Broştean, 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, San Diego, CA, USA (2023). https://www.ndss-symposium.org/wp-content/uploads/2023/02/ndss2023_s68_paper.pdf
Fiterău-Broştean, 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. ICST 2022, pp. 456–458. IEEE, Valencia, Spain (2022). https://doi.org/10.1109/ICST53961.2022.00051
Fiterău-Broştean, 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, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_12
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, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_25
Fiterău-Broştean, P., Lenaerts, T., Poll, E., 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. ACM, New York, NY, USA (2017). https://doi.org/10.1145/3092282.3092289
Frank, F., Milius, S., Rot, J., Urbat, H.: Learning Automata with Name Allocation (2025). arXiv:2502.11947
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, Cham (2021). https://doi.org/10.1007/978-3-030-91384-7_9
Frohme, M., Steffen, B.: Compositional learning of mutually recursive procedural systems. Int. J. Softw. Tools Technol. Transfer 23(4), 521–543 (2021). https://doi.org/10.1007/s10009-021-00634-y
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
Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of event-recording automata using timed decision trees. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006 – Concurrency Theory. LNCS, vol. 4137, pp. 435–449. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11817949_29
Groz, R., Oriat, C., Vega, G., Silva Simão, A., Foster, M., Walkinshaw, N.: Active inference of extended finite state models of software systems. In: Coste, F., Ouardi, F., Rabusseau, G. (eds.) Proceedings of 16th Edition of the International Conference on Grammatical Inference. Proceedings of Machine Learning Research, vol. 217, pp. 265–269. ML Research Press, Cambridge, MA (2023). https://proceedings.mlr.press/v217/groz23a/groz23a.pdf
Groz, R., Irfan, M.-N., Oriat, C.: Algorithmic improvements on regular inference of software models and perspectives for security testing. In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2012. LNCS, vol. 7609, pp. 444–457. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34026-0_33
Groz, R., Brémond, N., Silva Simão, A., Oriat, C.: hW-inference: A heuristic approach to retrieve models through black box testing. J. Syst. Softw. (2020). https://doi.org/10.1016/J.JSS.2019.110426
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, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45923-5_6
Higuera, C.: A bibliographical study of grammatical inference. Pattern Recogn. 38(9), 1332–1348 (2005). https://doi.org/10.1016/j.patcog.2005.01.003
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, Cham (2018). https://doi.org/10.1007/978-3-319-96562-8_5
Howar, F., Steffen, B.: Active automata learning as black-box search and lazy partition refinement. In: Jansen, N., Stoelinga, M., Bos, P. (eds.) A Journey from Process Algebra Via Timed Automata to Model Learning. LNCS, vol. 13560, pp. 321–338. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15629-8_17
Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. LNCS, vol. 7148, pp. 251–266. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_17
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
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 (2003). https://doi.org/10.1007/978-3-540-45069-6_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, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_26
Kaminski, M., Francez, N.: Finite-memory automata. Theoret. Comput. Sci. 134(2), 329–363 (1994). https://doi.org/10.1016/0304-3975(94)90242-9
Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge, MA, USA (1994)
Linard, A., 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, Cham (2019). https://doi.org/10.1007/978-3-030-13435-8_24
Lorenzoli, D., Mariani, L., Pezzè, M.: Automatic generation of software behavioral models. In: Proceedings of the 30th International Conference on Software Engineering. ICSE ’08, pp. 501–510. ACM, New York, NY, USA (2008). https://doi.org/10.1145/1368088.1368157
Maler, O., Mens, I.: A generic algorithm for learning symbolic automata from membership queries. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 146–169. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_8
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, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_41
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 (2004). https://doi.org/10.1109/HLDVT.2004.1431246
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
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Englewood Cliffs, NJ (1967)
Moeller, M., Ferreira, T., Lu, T., Foster, N., Silva, A.: Active learning of symbolic netkat automata. Proc. ACM Program. Lang. 9(PLDI), 1119–1142 (2025). https://doi.org/10.1145/3729295
Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: Proc. \(44^th\) ACM Symp. on Principles of Programming Languages. POPL ’17, pp. 613–625. ACM, New York, NY, USA (2017). https://doi.org/10.1145/3093333.3009879
Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: Polynomial-time equivalence testing for deterministic fresh-register automata. In: 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 117, pp. 72–17214. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2018). https://doi.org/10.4230/LIPIcs.MFCS.2018.72
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, Cham (2018). https://doi.org/10.1007/978-3-030-22348-9_23
Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403–435 (2004). https://doi.org/10.1145/1013560.1013562
Oncina, J., García, P.: Inferring regular languages in polynomial update time. In: Pattern Recognition and Image Analysis. Series in Machine Perception and Artificial Intelligence, vol. 1, pp. 49–61. World Scientific, Singapore (1992). https://doi.org/10.1142/9789812797902_0004
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput. 103(2), 299–347 (1993). https://doi.org/10.1006/inco.1993.1021
Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 193–206. USENIX Association, Washington, D.C., USA (2015). https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter
Sagonas, K., Jonsson, B., Howar, F., Dierl, S., Fiterău-Broştean, P., Tåquist, F.: Reproduction Artifact for TACAS 2024 paper “Scalable Tree-based Register Automata Learning” (2023). https://doi.org/10.5281/zenodo.10442556
Sakamoto, H.: Learning simple deterministic finite-memory automata. In: Algorithmic Learning Theory. ALT ’97. LNCS, vol. 1316, pp. 416–431. Springer, Berlin, Heidelberg (1997). https://doi.org/10.1007/3-540-63577-7_58
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, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_20
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
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, p. 25. IEEE Computer Society, Los Alamitos, CA (2007). https://doi.org/10.1109/ICDCS.2007.147
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. ACM, New York, NY, USA (2015). https://doi.org/10.1145/2786805.2786817
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, Tokyo, Japan (2017). https://doi.org/10.1109/ICST.2017.32
Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86–95 (2017). https://doi.org/10.1145/2967606
Vaandrager, F.W., Midya, A.: A Myhill-Nerode theorem for register automata and symbolic trace languages. Theor. Comput. Sci. 912, 37–55 (2022). https://doi.org/10.1016/j.tcs.2022.01.015
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, Cham (2021). https://doi.org/10.1007/978-3-030-68195-1_13
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, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_12
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
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, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16573-3_10
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). We thank these funding agencies and our anonymous reviewers for their comments.
Funding
Open access funding provided by Uppsala University.
Author information
Authors and Affiliations
Contributions
All authors have contributed to the preparation (writing and reviewing) of the article and to the design of the algorithms. Most credit for the implementation and of the proofs of algorithms’ correctness goes to Fredrik Tåquist. Credit for the tool that synthesizes automata that is described in Sect. 8.3 goes to Simon Dierl.
Corresponding author
Ethics declarations
Competing interests
The authors declare no competing interests.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/
About this article
Cite this article
Dierl, S., Fiterău-Broştean, P., Howar, F. et al. \({SL}^{\lambda }\): A Scalable Algorithm for Register Automata Learning. J Autom Reasoning 70, 14 (2026). https://doi.org/10.1007/s10817-026-09758-9
Received:
Accepted:
Published:
Version of record:
DOI: https://doi.org/10.1007/s10817-026-09758-9