Minimization of Symbolic Automata

Symbolic automata theory lifts classical automata theory to rich alphabet theories. It does so by replacing an explicit alphabet with an alphabet described implicitly by a Boolean algebra. We study here one of the core problems, minimization, of automata. We introduce a new minimization algorithm for symbolic automata that takes advantage of state-of-the-art constraint solving techniques for automata analysis that are both expressive and efficient, even for very large and infinite alphabets.