Abstract
We introduce the Büchi Store, an open repository of Büchi 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 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 new automata or smaller ones that are equivalent to some existing automaton. Such a collection of Büchi automata is also useful as a benchmark for evaluating complementation or translation algorithms and as examples for studying Büchi automata and temporal logic.
This work was supported in part by National Science Council, Taiwan, under the grant NSC97-2221-E-002-074-MY3.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Int’l Congress on Logic, Methodology and Philosophy of Science, pp. 1–11 (1962)
CodeIgniter, http://codeigniter.com/
Couvreur, J.M.: On-the-fly verification of linear temporal logic. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)
Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Kähler, D., Wilke, T.: Complementation, disambiguation, and determinization of Büchi automata unified. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 724–735. Springer, Heidelberg (2008)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377–408. ACM, New York (1990)
Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS, pp. 255–264. IEEE, Los Alamitos (2006)
Safra, S.: On the complexity of ω-automta. In: FOCS, pp. 319–327. IEEE, Los Alamitos (1988)
Schewe, S.: Büchi complementation made tight. In: STACS, pp. 661–672 (2009)
Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard (1983)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. TCS 49, 217–237 (1987)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
The Spec Patterns repository, http://patterns.projects.cis.ksu.edu/
Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: GOAL extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 346–350. Springer, Heidelberg (2008)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332–344. IEEE, Los Alamitos (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tsay, YK., Tsai, MH., Chang, JS., Chang, YW. (2011). Büchi Store: An Open Repository of Büchi Automata. In: Abdulla, P.A., Leino, K.R.M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2011. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19835-9_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-19835-9_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19834-2
Online ISBN: 978-3-642-19835-9
eBook Packages: Computer ScienceComputer Science (R0)