Grammatical Inference as a Satisfiability Modulo Theories Problem

TL;DR

This paper reformulates the problem of learning minimal automata from labeled sequences as a satisfiability modulo theories problem, introducing encodings that outperform existing methods for small models.

Contribution

It presents novel SMT-based encodings for deterministic finite automata, Moore, and Mealy machines, advancing automata learning techniques.

Findings

Encodings improve learning efficiency over state-of-the-art methods

Effective for small automata models

Experimental results validate practical usefulness

Abstract

The problem of learning a minimal consistent model from a set of labeled sequences of symbols is addressed from a satisfiability modulo theories perspective. We present two encodings for deterministic finite automata and extend one of these for Moore and Mealy machines. Our experimental results show that these encodings improve upon the state-of-the-art, and are useful in practice for learning small models.