Congruence Relations for Büchi Automata

We revisit congruence relations for Büchi automata, which play a central role in automata-based formal verification. The size of the classical congruence relation is in \(3^{\mathcal {O}(n^{2})}\), where n is the number of states of the given Büchi automaton. We present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptotically optimal congruence relations of size \(2^{\mathcal {O}(n \log n)}\). Based on these optimal congruence relations, we obtain an optimal translation from a Büchi automaton to a family of deterministic finite automata (FDFA), which can be made to accept either the original language or its complement. To the best of our knowledge, our construction is the first direct and optimal translation from Büchi automata to FDFAs.