Brzozowski’s Algorithm for Automata Minimization Verified in Coq

Deterministic finite automata are abstract machines that play a vital role in computer science and control engineering, aiding in the development of compilers, search algorithms, modeling of discrete event systems and more. With the aim of optimizing computational resources, minimization algorithms have been developed to eliminate unreachable and indistinguishable states in these automata. Brzozowski’s algorithm is one such method which involves reversing and determinizing the automaton twice. Despite its apparent simplicity, proving the correctness of this minimization method requires various inductive strategies. For this purpose, the Coq proof assistant was employed to streamline the proof and provide a means of verification for the algorithm. In addition to the related demonstrations, this paper contributes with a straightforward representation of automata in functional programming languages. This approach uses only lists and types with decidable equality, so that common data structures can be utilized to represent finite automata. It also offers an accessible explanation for the reasoning process.