Source code and data relevant for the paper 'Model Learning as a Satisfiability Modulo Theories Problem'

Abstract

This datasets belongs to the following paper: Model Learning as a Satisfiability Modulo Theories Problem. URL = http://www.sws.cs.ru.nl/publications/papers/fvaan/SMT/main.pdf

The dataset contains the source code of the tool implementing the SMT-based approach described in the paper, the setups/scripts used to run experiments and experimental logs.

Paper Abstract: We explore an approach to model learning that is based on using satisfiability modulo theories (SMT) solvers. To that end, we explain how DFAs, Mealy machines and register automata, and observations of their behavior can be encoded as logic formulas. An SMT solver is then tasked with finding an assignment for such a formula, from which we can extract an automaton of minimal size. We provide an implementation of this approach which we use to conduct experiments on a series of benchmarks. These experiments address both the scalability of the approach and its performance relative to existing active learning tools.