Formal Verification of Automata Theory in Isabelle/HOL

This project aims to formalize the mathematical theory of finite automata and Büchi automata using the interactive theorem prover Isabelle/HOL. The objective is to develop a comprehensive, machine-checked framework that provides precise definitions, verified constructions, and formally proven fundamental results of automata theory.

Automata theory forms an essential foundation of theoretical computer science, with applications in formal language theory, program verification, and model checking. Finite automata describe computational processes over finite words, while Büchi automata extend this concept to infinite words, enabling the specification and verification of properties of systems exhibiting infinite behaviour. Isabelle/HOL provides a formal environment in which mathematical definitions and theorems can be expressed and their correctness verified through machine-checked proofs.

The project covers fundamental constructions and equivalence results for finite automata, including determinization, minimization, and equivalences with regular expressions and regular grammars. Building on these results, the framework is extended to Büchi automata, addressing infinite words, infinite runs, acceptance conditions, and properties of ω-regular languages. The overarching goal is to establish a rigorous and reusable formalization of automata theory that can serve as a foundation for further research and formal verification.