On the Virtue of Patience: Minimizing Büchi Automata
Rüdiger Ehlers and Bernd Finkbeiner
Explicit-state model checkers like SPIN, which verify systems against properties stated in linear-time temporal logic (LTL), rely on efficient LTL-to-Büchi translators. A difficult design decision in such constructions is to trade time spent on minimizing the Büchi automaton versus time spent on model checking against an unnecessarily large automaton. Standard reduction methods like simulation quotienting are fast but often miss optimization opportunities. We propose a new technique that achieves significant further reductions when more time can be invested in the minimization of the automaton. The additional effort is often justified, for example, when the properties are known in advance, or when the same property is used in multiple model checking runs. We use a modified SAT solver to perform bounded language inclusion checks on partial solutions. SAT solving allows us to prune large parts of the search space for smaller automata already in the early solving stages. The bound allows us to fine-tune the algorithm to run in limited time. Our experimental results show that, on standard LTL-to-Büchi benchmarks, our prototype implementation achieves a significant further size reduction on automata obtained by the best currently available LTL-to-Büchi translators.
17th International SPIN Workshop on Model Checking of Software (SPIN 2010).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.