Optimizing Büchi Automata

Kousha Etessami, Gerard J. Holzmann

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We describe a family of optimizations implemented in a translation from a linear temporal logic to Büchi automata. Such optimized automata can enhance the efficiency of model checking, as practiced in tools such as Spin. Some of our optimizations are applied during preprocessing of temporal formulas, while other key optimizations are applied directly to the resulting Büchi automata independent of how they arose. Among these latter optimizations we apply a variant of fair simulation reduction based on color refinement. We have implemented our optimizations in a translation of an extension to LTL described in [Ete99]. Inspired by this work, a subset of the optimizations outlined here has been added to a recent version of Spin. Both implementations begin with an underlying algorithm of [GPVW95]. We describe the results of tests we have conducted, both to see how the optimizations improve the sizes of resulting automata, as well as to see how the smaller sizes for the automata affect the running time of Spin’s explicit state model checking algorithm. Our translation is available via a web-server which includes a GUI that depicts the resulting automata: http://cm.bell-labs.com/cm/cs/what/spin/eqltl.html
Original languageEnglish
Title of host publicationCONCUR 2000 - Concurrency Theory
Subtitle of host publication 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings
PublisherSpringer Berlin Heidelberg
Pages153-167
Number of pages15
Volume1877
ISBN (Electronic)978-3-540-44618-7
ISBN (Print)978-3-540-67897-7
DOIs
Publication statusPublished - 2000

Fingerprint

Dive into the research topics of 'Optimizing Büchi Automata'. Together they form a unique fingerprint.

Cite this