SAT-Based Minimization of Deterministic \omega -Automata.

We describe a tool that inputs a deterministic $$\\omega $$-automaton with any acceptance condition, and synthesizes an equivalent $$\\omega $$-automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exists. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal $$\\omega $$-automata equivalent to given properties, for different acceptance conditions.