Moritz Lichter

Research Immersion Lab: Büchi Automata in Coq

Author: Moritz Lichter
Advisor: Prof. Dr. Gert Smolka

Abstract

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.

Attached Documents

References

Büchi automata

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.

Formalization in Coq

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.

Legal notice, Privacy policy