Grey-Box Learning of Register Automata

TL;DR

This paper introduces a grey-box approach to model learning of register automata, significantly improving scalability and enabling the learning of complex infinite-state systems by extracting parameter constraints from program runs.

Contribution

It presents new implementations of the tree and equivalence oracles that leverage constraints from run data, enhancing performance and extending the applicability of model learning to richer system classes.

Findings

Almost two orders of magnitude reduction in inputs sent to systems.

Successful learning of models like combination locks that black-box methods cannot handle.

Improved scalability demonstrated on Python standard library data structures.

Abstract

Model learning (a.k.a. active automata learning) is a highly effective technique for obtaining black-box finite state models of software components. Thus far, generalisation to infinite state systems with inputs/outputs that carry data parameters has been challenging. Existing model learning tools for infinite state systems face scalability problems and can only be applied to restricted classes of systems (register automata with equality/inequality). In this article, we show how we can boost the performance of model learning techniques by extracting the constraints on input and output parameters from a run, and making this grey-box information available to the learner. More specifically, we provide new implementations of the tree oracle and equivalence oracle from RALib, which use the derived constraints. We extract the constraints from runs of Python programs using an existing tainting library for Python, and compare our grey-box version of RALib with the existing black-box version on several benchmarks, including some data structures from Python's standard library. Our proof-of-principle implementation results in almost two orders of magnitude improvement in terms of numbers of inputs sent to the software system. Our approach, which can be generalised to richer model classes, also enables RALib to learn models that are out of reach of black-box techniques, such as combination locks.