Input/output automaton とは

入出力オートマトンは、ほとんどのタイプの非同期並行システムを記述するのに適用可能な正式なモデルを提供する。 I / Oオートマトンモデルには、それ自体がさまざまなタイプの分散システムをモデル化できる非常に基本的な構造が含まれています。特定のタイプの非同期システムを記述するために、この基本モデルに追加の構造を追加する必要があります。このモデルは、相互作用し、任意の相対速度で動作するプロセスやメッセージチャネルなどのシステムコンポーネントを記述して推論する明示的な方法を提示します。 I / Oオートマトンは、Nancy A. LynchとMark R. Tuttleによって「分散アルゴリズムの階層的正当性証明」1987年に最初に導入されました。
「I / Oオートマトンは、他のシステムコンポーネントとやりとりすることができる分散システムコンポーネントをモデル化します。これは、遷移が名前付きアクションに関連付けられた単純なタイプのステートマシンです。アクションには、入力、出力、内部アクションの3種類があります。オートマトンは入力と出力のアクションを使用して環境と通信しますが、内部アクションはオートマトンだけが見ることができます。オートマトンによって選択されて実行される内部アクションや出力アクションとは異なり、入力アクション(環境から単純に到着する)はオートマトンの制御下にありません。