Boolean Optimization and Verification of Automata and Circuits