Congruence Relations for Büchi Automata
Journal
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Journal Volume
13047 LNCS
Pages
465-482
Date Issued
2021
Author(s)
Abstract
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 3O(n2), 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 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.
Subjects
Formal verification
Asymptotically optimal
Buchi automata
Deterministic finite automata
Number of state
Finite automata
Type
conference paper