2000 | OriginalPaper | Buchkapitel
Optimizing Büchi Automata
verfasst von : Kousha Etessami, Gerard J. Holzmann
Erschienen in: CONCUR 2000 — Concurrency Theory
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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