2016-12-16 Buchi Automataあれこれ 未整理 記事の体をなさぬメモ 用語 Buchi Automatonあれこれ 思いつき次第追記していきます Emptiness checking Buchi Automatonが受理する言語が空でない 初期状態から到達可能かつサイクル上にある終状態が存在する. 効率的なアルゴリズム オートマトンを有向グラフとみなし強連結成分に分ける 初期状態から各成分に到達可能かを調べる 初期状態から到達可能かつ自明でない強連結成分が終状態を含むかを調べる このアルゴリズムは線形時間で終わる 参考 Büchi automaton - Wikipedia