Research Immersion Lab: Büchi Automata in Coq
Author: Moritz Lichter
Advisor: Prof. Dr. Gert Smolka
Büchi automata are a well-known automata model for infinitely long words. We give a formalization of Büchi automata in the constructive type theory in Coq. While the word problem becomes undecidable for Büchi automata, we can decide language emptiness. Büchi automata are known to be closed under boolean operations in classical mathematics. In contrast to NFAs on finite words, Büchi automata cannot be made deterministic and thus the complement construction gets more difficult. In order to prove the closure properties we need assumptions for combinatorial reasoning on infinite words. These assumptions are weaker then excluded middle. We follow the complementation proof idea originally given by Büchi and analyze which assumptions are sufficient to prove its correctness.
Formalization in Coq
- Bakhadyr Khoussainov and Anil Nerode. Automata Theory and its Applications. Birkhäuser, Boston, 2011.
- Dominique Perrin and Jean-Éric Pin. Infinite Words - Automata, Semigroups, Logic and Games. Elsevier, 2004.
- J. R. Büchi. "On a Decision Method in Restricted Second-Order Arithmetic." In: International Congress on Logic, Methodology, and Philosophy of Science. Stanford University Press, 1962, pages 1-11.
- Martin Hofmann and Martin Lange. Automatentheorie und Logik. Springer-Verlag Berlin Heidelberg, 2011.
- Ming-Hsien Tsai et al. "State of Büchi Complementation." In: Logical Methods in Computer Science, 10(4), 2014.
- Moshe Y. Vardi. "The Büchi Complementation Saga". In: STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings. 2007, pages 12-22.
- Christian Doczkal and Gert Smolka. "Two-way Automata in Coq". In: Interactive theorem proving (itp 2016), Ed. by Jasmin Blanchette and Stephan Merz. Vol. 9807. LNCS. 2016, pp. 151–166.
- Jan Christian Menz. A Coq Library for Finite Types. Bachelor Thesis, Saarland University, 22/7/2016.
- Gert Smolka and Kathrin Stark. "Hereditarily Finite Sets in Constructive Type Theory". In: Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-27, 2016. Ed. by Jasmin Christian Blanchette and Stephan Merz. Vol. 9807.
LNCS. Springer, 2016, pp. 374–390.