$${SL}^{\lambda }$$: A Scalable Algorithm for Register Automata Learning

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 }$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>SL</mml:mi> </mml:mrow> <mml:mi>λ</mml:mi> </mml:msup> </mml:math> , 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 }$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>SL</mml:mi> </mml:mrow> <mml:mi>λ</mml:mi> </mml:msup> </mml:math> 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)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>O</mml:mi> <mml:mo>(</mml:mo> <mml:msup> <mml:mi>t</mml:mi> <mml:mn>2</mml:mn> </mml:msup> <mml:mspace/> <mml:msup> <mml:mrow> <mml:mo>(</mml:mo> <mml:mn>2</mml:mn> <mml:mi>n</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> <mml:mi>n</mml:mi> </mml:msup> <mml:mo>+</mml:mo> <mml:mi>m</mml:mi> <mml:msup> <mml:mi>t</mml:mi> <mml:mn>2</mml:mn> </mml:msup> <mml:mspace/> <mml:msup> <mml:mi>m</mml:mi> <mml:mi>m</mml:mi> </mml:msup> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> membership queries and O ( t ) equivalence queries, where m is the length of the longest counterexample received during learning. We have implemented $${SL}^{\lambda }$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>SL</mml:mi> </mml:mrow> <mml:mi>λ</mml:mi> </mml:msup> </mml:math> as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mmultiscripts> <mml:mrow> <mml:mi>SL</mml:mi> </mml:mrow> <mml:mrow/> <mml:mrow> <mml:mrow/> <mml:mo>∗</mml:mo> </mml:mrow> </mml:mmultiscripts> </mml:math> , 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.