Advanced automata minimization

We present an efficient algorithm to reduce the size of nondeter-ministic Büchi word automata, while retaining their language. Ad-ditionally, we describe methods to solve PSPACE-complete au-tomata problems like universality, equivalence and inclusion for much larger instances (1-3 orders of magnitude) than before. This can be used to scale up applications of automata in formal verifica-tion tools and decision procedures for logical theories. The algorithm is based on new transition pruning techniques. These use criteria based on combinations of backward and forward trace inclusions. Since these relations are themselves PSPACE-complete, we describe methods to compute good approximations of them in polynomial time. Extensive experiments show that the average-case complexity of our algorithm scales quadratically. The size reduction of the au-tomata depends very much on the class of instances, but our algo-rithm consistently outperforms all previous techniques by a wide margin. We tested our algorithm on Büchi automata derived from LTL-formulae, many classes of random automata and automata de-rived from mutual exclusion protocols, and compared its perfor-mance to the well-known automata tool GOAL [34]