Historical Notes

Büchi automata are finite automata operating on infinite words. A Büchi automaton accepts an infinite word if it induces a run of the automaton that visits some accept state infinitely many times. The formalism was invented by Büchi around 1960 to prove the decidability of the Monadic Second Order Theory of Natural Numbers [1]. Near two decades later, they found practical applications in linear time model checking. In an appendix of his seminal FOCS 1977 paper [2] which introduced temporal logic to computer science, Pnueli suggested two ways to prove the decidability of essentially the linear time model checking problem. (The result was originally stated as "the validity of an arbitrary tense formula over a finite state system is decidable." In the paper, only two tense (temporal) operators F (eventually or sometime) and G (always) were considered.) One proof went via the translation of a temporal formula into a Büchi automaton and then invoked the decidability of language containment between two Büchi automata, one representing the system and the other the temporal formula whose validity over the system is to be checked. This proof was a precursor to the automata-theoretic approach to linear time model checking eloquently advocated by Vardi and Wolper in [3].

1. J. R. Buchi. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pages 1-12. Stanford University Press, 1962.
2. A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46-57, 1977.
3. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verication. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986.