Congruence Relations for B\"uchi Automata

TL;DR

This paper introduces improved and optimal congruence relations for B"uchi automata, enabling more efficient automata-based verification and a direct, optimal translation to deterministic finite automata for complement acceptance.

Contribution

It presents exponentially coarser and asymptotically optimal congruence relations, and a novel direct, optimal translation from B"uchi automata to FDFWs.

Findings

Improved congruence relations are exponentially coarser than classical ones.

Achieved asymptotically optimal congruence relations of size 2^{O(n log n)}.

First direct and optimal translation from B"uchi automata to FDFWs.

Abstract

We revisit here congruence relations for B\"uchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{\mathcal{O}(n^2)}$, where $n$ is the number of states of a given B\"uchi automaton $\mathcal{A}$. Here 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 B\"uchi automata to a family of deterministic finite automata (FDFW) that accepts the complementary language. To the best of our knowledge, our construction is the first direct and optimal translation from B\"uchi automata to FDFWs.