  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.
