Buchi Automataあれこれ

Buchi Automatonあれこれ

思いつき次第追記していきます

Emptiness checking

Buchi Automatonが受理する言語が空でない

初期状態から到達可能かつサイクル上にある終状態が存在する.

効率的なアルゴリズム

1. オートマトンを有向グラフとみなし強連結成分に分ける
2. 初期状態から各成分に到達可能かを調べる
3. 初期状態から到達可能かつ自明でない強連結成分が終状態を含むかを調べる

このアルゴリズムは線形時間で終わる

参考

Büchi automaton - Wikipedia