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?