Moritz Lichter

Saarland University Computer Science

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.

Attached Documents


Büchi automata Formalization in Coq

Moritz Lichter, Tue Oct 25 17:04:57 2016