Optimizing Buchi automata

We describe a family of optimizations for a translation from a linear temporal logic to Buchi automata. Such optimized automata can enhance the efficiency of explicit state model checking, as practiced in tools such as SPIN. Some of our optimizations are applied during preprocessing of temporal formulas, others are applied during the translation algorithm itself, while other key optimizations are applied directly to the resulting Buchi automata independent of how they arose. Among these latter optimizations we give a practical algorithm for a variant of fair simulation reduction based on color refinement. Although there are weaker notions of fair simulation availalbe in the literature, leading to potentially greater reduction, the best algorithms for computing these weaker notions appear at present to be impractical. Our color refinement algorithm, instead of just maintaining equivalence classes of colors, maintains a natural partial ordering of the color classes that is based on their language containment properties during the refinement, coarsening the refinement as a result. We have implemented these optimizations in a translation of an extended temporal logic described in [Ete99], and have tested it on a variety of formulas. It tends to produce reasonably small automata, often close to optimal, and does so within reasonable running time. With the help of Gerard Holzmann the translation is now available via a server on the web through a GUI which depicts the resulting automata at: http://cm.bell-labs.com/cm/cs/what/spin/eqltl.html.