About LearnLib
LearnLib is a framework for automata learning, implemented in Java.
Work on LearnLib was partially supported by the European Union FET Project CONNECT: Emergent Connectors for Eternal Software Intensive Networked Systems (http://connect-forever.eu/).
Automata learning
Automata learning tries to automatically construct a finite automaton that matches the behavior of a given target automaton on the basis of (systematic) observation. This complements other automatic learning techniques which aim at the construction of invariants.
Active learning assumes an omniscient teacher which is able to answer membership and equivalence queries. A membership query tests whether a string (a potential run) is contained in the target automatons language (its set of runs), and an equivalence query compares the hypothesis automaton with the target automaton for language equivalence, in order to determine whether the learning procedure was successfully completed.
Making automata learning practical
In any practical attempt of learning legacy systems, equivalence queries can only be treated approximately, but membership queries can be answered by testing the target systems. LearnLib therefore provides a number of heuristics and techniques for this approximation.
A platform for experimenting with different learning algorithms and for statistically analyzing their characteristics in terms of required number and size of e.g., membership queries, run time, and memory consumption, is also provided. This concerns in particular the analysis of the impact of the various techniques for optimizations.
LearnLib contains learning algorithms of different flavor, mostly variants and extensions of Angluin's algorithm L*.
Learning reactive systems
Angluin's algorithm works on deterministic finite state machines, which, as
usual, consist of a finite set of states Q, a finite (input) alphabet Σ, a
transition function
Typical reactive systems do not terminate and are therefore not modelled appropriately with accepting states. It turned out that Mealy machines, which adequately model input/output behavior provide a much better modelling, which is not only more concise, but can also be learned much faster.
The learning algorithms can be freely combined with a number of filters, optimizing the number of required membership queries, and with an adequate approximate solver for equivalence queries. Whereas these approximate solvers are necessary whenever one attempts to learn a legacy system, they can can be replaced by a perfect equivalence checker for the statistical analysis of learning scenarios using existing or generated target models. LearnLib provides a bisimulation checker for this purpose.