A tool for minimal NFA computation It is well known that minimizing an NFA for a fixed regular language is $PSPACE-Complete$.

As far as I know, there are no better than trivial algorithms for minimizing such NFA, but there's a little improvement if you consider symmetries.

I've a specific regular language I'd like to compute a minimal automaton for:

$$
L_{k-distinct} :=\{w = \sigma_1\sigma_2...\sigma_k \mid \forall i\in[k]: \sigma_i\in\Sigma ~\text{ and }~ \forall j\ne i: \sigma_j\ne\sigma_i \}$$

But at the moment I can't seem to close the gap between the automaton I know to build for it and the lower bound I can prove for it.

I thought it might be fruitful to use some tool that given a language (it is finite for all $k,n$), searches (exhaustively if needed) for the smallest automaton which accept it, and see what the automaton looks like for small values of $k,n$.

Does anyone know a tool which builds a minimal automaton for a given language?
The following paper reports on an implementation of the Kameda-Weiner algorithm for computing a minimal NFA, as well on an approach using a SAT solver. I don't know whether the implementation is available, but perhaps you can contact the authors about this.

Jaco Geldenhuys, Brink van der Merwe, and Lynette van Zijl. Reducing Nondeterministic Finite Automata with SAT Solvers. Revised Selected Papers from the 8th International Workshop on Finite-State Methods and Natural Language Processing (FSMNLP 2009), LNCS 6062, Springer, pages 81-92, 2010.