Büchi自动机的同余关系
Congruence Relations for Büchi Automata
摘要：
在这里，我们重新审视Büchi自动机的同余关系，它在基于自动机的验证中起着核心作用。经典同余关系的大小是$3^{\mathcal{O}(n^2)}$，其中$n$是给定的Büchi自动机$\mathcal{A}$的状态数。在这里，我们提出了改进的同余关系，可以比经典的指数粗糙。进一步给出了尺寸为$2^{\mathcal{O}(n \log n)}$的渐近最优同余关系.基于这些最佳的同余关系，我们得到了一个最佳的翻译从Büchi自动机的一个家庭的确定性有限自动机（FDFW），接受互补语言。据我们所知，我们的建设是第一个直接和最佳的翻译从Büchi自动机FDFW。
英文摘要：
We revisit here congruence relations for Büchi 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üchi 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üchi 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üchi automata to FDFWs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
