Büchi automaton とは

コンピュータサイエンスとオートマトンの理論では、Büchiオートマトンは有限オートマトンを無限インプットに拡張するω-オートマトンの一種です。無限に入力された入力シーケンスを受け入れるのは、(少なくとも)最終状態の1つを無限に訪れるオートマトンの実行が存在する場合です。 Büchiオートマトンは、正規言語の無限語版、オメガ – レギュラー言語を認識します。それは1962年にこの種のオートマトンを発明したスイスの数学者Julius RichardBüchiにちなんで命名されました。
Büchiオートマトンは、しばしば、線形時間論理の式のオートマトン理論バージョンとしてモデルチェックに使用されます。