Coinductive Algorithms for Büchi Automata
Coinductive Algorithms for Büchi Automata
复制标题
Büchi 自动机的共归纳算法
DOI：
10.1007/978-3-030-24886-4_15
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
D. Pous
中科院分区：
文献类型：
--
作者：
Denis Kuperberg;L. Pinault;D. Pous
我们提出了一种新算法来检查非确定性 Büchi 自动机的语言等价性。我们从 Calbrix、Nivat 和 Podelski 提出的构造开始，该构造可以将问题简化为检查自动机在有限词上的等价性。尽管这种构造生成了大型且高度不确定的自动机，但我们展示了如何利用其特定结构并应用基于共归纳的最先进技术来减少必须探索的状态空间。这样做，我们获得了不需要完全确定或补充的算法。
We propose a new algorithm for checking language equivalence of non-deterministic Büchi automata. We start from a construction proposed by Calbrix, Nivat and Podelski, which makes it possible to reduce the problem to that of checking equivalence of automata on finite words. Although this construction generates large and highly non-deterministic automata, we show how to exploit their specific structure and apply state-of-the art techniques based on coinduction to reduce the state-space that has to be explored. Doing so, we obtain algorithms which do not require full determinisation or complementation.