DFAMiner: Mining minimal separating DFAs from labelled samples

TL;DR

DFAMiner is a new passive learning tool that efficiently constructs minimal separating DFAs from labelled samples, with applications in regular model checking and parity game solving, outperforming existing tools.

Contribution

It introduces a linear-time algorithm for building a three-valued DFA and a SAT-based minimization approach for extracting minimal separating automata from samples.

Findings

Outperforms state-of-the-art tools on benchmark datasets

Can generate optimal separating automata for simple languages with up to 7 colours

Provides a foundation for lower bounds in parity game solving

Abstract

We propose DFAMiner, a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. We first propose a simple and linear-time algorithm that incrementally constructs a three-valued DFA (3DFA) from a set of labelled samples given in the usual lexicographical order. This 3DFA has accepting and rejecting states as well as don't-care states, so that it can exactly recognise the labelled examples. We then apply our tool to mining a minimal separating DFA for the labelled samples by minimising the constructed automata via a reduction to solving SAT problems. Empirical evaluation shows that our tool outperforms current state-of-the-art tools significantly on standard benchmarks for learning minimal separating DFAs from samples. Progress in the efficient construction of separating DFAs can also lead to finding the lower bound of parity game solving, where we show that DFAMiner can create optimal separating automata for simple languages with up to 7 colours. Future improvements might offer inroads to better data structures.