無限オブジェクト上のオートマトン

無限オブジェクト上のオートマトンは、無限の単語や無限の木など、決して終わることのない入力を読み取り、どの状態や遷移が無限に頻繁に訪れるかに応じて受理します。これは、継続的で非終端的なシステムについて推論するための数学的メカニズムを提供します。

Definition

オメガオートマトンは、その実行が無限であり、無限に頻繁に訪れる状態の集合に関する条件によって受理が定義される有限状態機械です。このようなオートマトンは、オメガ正則言語と呼ばれる無限の単語または木の集合を認識します。

Scope

このトピックでは、無限の単語上のBüchi、Muller、Rabin、およびパリティオートマトン、それらを区別する受理条件、決定化と補元化の結果、無限の木上のオートマトン、そしてこれらのオートマトン、単項二階論理、および合成と検証で使用される無限ゲームとの間の深い関連性について扱います。

Core questions

• 有限機械は、終わりがない入力をどのようにして受理または拒否できるのでしょうか？
• 非決定性Büchiオートマトンと決定性Büchiオートマトンは、表現力においてなぜ異なるのでしょうか？
• 無限オブジェクト上のオートマトンは、システム動作を記述するための論理とどのように関連しているのでしょうか？
• これらのオートマトンの補元化を困難にしている要因は何であり、なぜそれが重要なのでしょうか？

Key theories

Büchi受理とオメガ正則言語

Büchiオートマトンは、ある受理状態が無限に頻繁に訪れるときに無限の単語を受理します。このように認識される言語、すなわちオメガ正則言語は、自然数上の単項二階論理で定義可能な言語と一致します。

決定化とパリティ条件

非決定性Büchiオートマトンは、受理条件を変更せずに一般的に決定化することはできませんが、Safraの構成法はそれらを決定性Rabinオートマトンまたはパリティオートマトンに変換します。これは補元化やゲームの解決に不可欠です。

Clinical relevance

オメガオートマトンはモデル検査のアルゴリズム的基盤です。反応システムと時相論理プロパティはそれぞれ無限の単語上のオートマトンに変換され、プロパティの検査は空性テストに帰着されます。これにより、ハードウェア、プロトコル、および並行ソフトウェアの自動検証が可能になります。

History

Büchiは1960年頃、自然数の単項二階理論を決定するために無限の単語上のオートマトンを導入しました。McNaughtonは、より強力な受理条件を用いてそれらを決定化する方法を示し、Rabinは理論を無限の木に拡張しました。これらの結果は、1970年代後半に時相論理がコンピュータサイエンスに導入されて以来、検証の中心となりました。

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

機械は無限の入力をどのように受理できるのでしょうか？

受理は、終わりがないため、終端状態に到達することによって定義されるのではなく、どの状態が繰り返し現れるかによって定義されます。例えば、Büchiオートマトンは、その無限の実行中に指定された受理状態を無限に頻繁に通過するときに受理します。

これらのオートマトンは検証にとってなぜ重要なのでしょうか？

オペレーティングシステムやネットワークプロトコルなどの非終端システムは、無限の振る舞いによって自然にモデル化されます。「システムがデッドロックしない」や「すべての要求が最終的に処理される」といったプロパティはオメガ正則言語となり、それらの検査はモデルチェッカーが自動的に実行できるオートマトン操作に帰着されます。