Büchi Store: An open repository of ω-automata
Journal
International Journal on Software Tools for Technology Transfer
Journal Volume
15
Journal Issue
2
Pages
109-123
Date Issued
2013
Author(s)
Abstract
We introduce Büchi Store, an open repository of Büchi automata and other types of ω-automata for model-checking practice, research, and education. The repository contains Büchi automata and their complements for common specification patterns and numerous temporal formulae. These automata are made as small as possible by various construction techniques in view of the fact that smaller automata are easier to understand and often help in speeding up the model-checking process. The repository is open, allowing the user to add automata that define new languages or are smaller than existing equivalent ones. Such a collection of Büchi automata is also useful as a benchmark for evaluating translation or complementation algorithms and as examples for studying Büchi automata and temporal logic. These apply analogously for other types of ωf-automata, including deterministic Büchi and deterministic parity automata, which are also collected in the repository. In particular, the use of smaller deterministic parity automata as an intermediary helps reduce the complexity of automatic synthesis of reactive systems from temporal specifications. © 2013 Springer-Verlag Berlin Heidelberg.
Type
journal article