通信有限状態マシン

コンピュータサイエンスにおいて、通信有限状態機械とは、いくつかのアルファベットのチャネルを介して「受信」および「送信」操作でラベル付けされた有限状態機械です。これらは Brand と Zafiropulo によって導入され、 ^[1]ペトリネットのような並行プロセスのモデルとして使用できます。通信有限状態機械は、有界性、デッドロック、未指定の受信などの主要なプロトコル設計エラーを検出できるため、通信プロトコルのモデル化によく使用されます。^[2]

通信有限状態機械の利点は、通信プロトコルの多くの特性を、単にそのような特性を検出するレベルを超えて決定できることです。この利点により、人間の支援や一般性の制限の必要性が排除されます。^[1]

伝播遅延が無視できない状況（複数のメッセージが同時に送信される可能性がある状況）や、プロトコルの当事者と通信媒体を別々のエンティティとして記述することが自然な状況では、通信有限状態マシンは有限状態マシンよりも強力になる可能性があります。^[1]

階層型ステート マシンは、状態自体が他のマシンになる可能性がある有限ステート マシンです。通信する有限ステート マシンは並行性を特徴とするため、通信する階層型ステート マシンの最も注目すべき特徴は、階層と並行性の共存です。これは、マシン内部のより強力な相互作用を意味するため、非常に適切であると考えられてきました。

しかし、階層性と並行性の共存は、本質的に言語の包含性、言語の同等性、そして普遍性のすべてを犠牲にすることが証明されました。^[3]

任意の正の整数に対して、プロセスを持つプロトコル^{[1] :3は}次の4つから成ります。 ${\displaystyle N}$ ${\displaystyle N}$${\displaystyle \{(S_{i})_{i=1}^{N},\ (o_{i})_{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^{N}\}}$

• ${\displaystyle (S_{i})_{i=1}^{N}}$は、互いに素な有限集合のシーケンスです。各集合はプロセスを表すために使用され、 の各要素は、 - 番目のプロセスの可能な状態を表します。${\displaystyle N}$${\displaystyle S_{i}}$${\displaystyle i}$
• ${\displaystyle (o_{i})_{i=1}^{N}}$( ) は各プロセスの初期状態を表すシーケンスです。${\displaystyle o_{i}\in S_{i}}$
• ${\displaystyle (M_{i,j})_{i,j=1}^{N}}$は、各集合がプロセスからプロセスに送信される可能性のあるメッセージを表す、互いに素な有限集合の有限シーケンスです。 の場合、 は空です。${\displaystyle N^{2}}$${\displaystyle M_{i,j}}$${\displaystyle i}$${\displaystyle j}$${\displaystyle i=j}$${\displaystyle M_{i,j}}$
• ${\displaystyle ({\mathtt {succ}})_{i=1}^{N}:S_{i}\times \bigcup _{j=1}^{N}\left(M_{j,i}^{[+]}\cup M_{i,j}^{[-]}\right)\mapsto S_{i}}$は遷移関数のシーケンスです。各関数は、任意のメッセージを送信または受信することによって実行できる遷移をモデル化します。プロセスに関しては、シンボルは受信できるメッセージと送信できるメッセージを示すために使用されます。${\displaystyle i}$${\displaystyle [+]}$${\displaystyle [-]}$

グローバル状態とは、 ${\displaystyle \langle S,C\rangle }$

• ${\displaystyle S=(s_{1},...,s_{N})}$は、それぞれが - 番目のプロセスの状態を表すような順序付けられた状態の集合です。${\displaystyle s_{i}}$${\displaystyle i}$
• ${\displaystyle C}$は、それぞれがの部分列となるような行列です。${\displaystyle N\times N}$${\displaystyle c_{i,j}\in C}$${\displaystyle M_{i,j}}$

初期のグローバル状態は、 ${\displaystyle \langle O,\mathrm {E} \rangle }$

• ${\displaystyle O=(o_{1},...,o_{N})}$
• ${\displaystyle \mathrm {E} }$は、すべての に対して、空語 に等しい行列として定義されます。${\displaystyle N\times N}$${\displaystyle i,j\in \{1,...,N\}}$${\displaystyle E_{i,j}}$${\displaystyle \epsilon }$

ステップには、メッセージを受信するステップとメッセージを送信するステップの 2 種類があります。

プロセスが、のとき、の形式のペアである。同様に、 のとき、 のプロセス から のプロセスにメッセージが送信されるペアは、 のとき、 の形式のペアである。 ${\displaystyle j}$${\displaystyle i}$${\displaystyle \left\langle (s_{1},\dots ,s_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }$${\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}}$${\displaystyle m'_{i,j}\in M_{i,j}}$${\displaystyle i}$${\displaystyle j}$${\displaystyle \left\langle (s_{1},\dots ,s_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle }$${\displaystyle {\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}}$

実行とは、ステップが次のステップに状態を関連付け、最初の状態が初期状態となるようなグローバル状態のシーケンスです。

この状態を通過する実行が存在する場合、 グローバル状態は到達可能であると言われます。${\displaystyle \langle S,C\rangle }$

概念自体の導入により、2 つの有限状態マシンが 1 種類のメッセージのみで通信する場合、有界性、デッドロック、および未指定の受信状態を決定および識別できますが、マシンが 2 種類以上のメッセージで通信する場合はそうではないことが証明されました。その後、1 つの有限状態マシンのみが 1 種類のメッセージで通信し、そのパートナーの通信が制約されていない場合でも、有界性、デッドロック、および未指定の受信状態を決定および識別できることがさらに証明されました。^[2]

さらに、メッセージの優先順位関係が空の場合、有限状態機械間の通信において2種類以上のメッセージが存在する状況でも、有界性、デッドロック、未指定の受信状態を決定できることが証明されている。^[4]

有界性、デッドロック、および不特定の受信状態はすべて多項式時間で決定可能です（つまり、特定の問題は無限時間ではなく扱いやすい時間で解決できます）。なぜなら、それらに関する決定問題は非決定性対数空間完全だからです。^[2]

検討されている拡張機能は次のとおりです。

• 一部の州ではメッセージが受信されない可能性があることを示す注記があること
• メッセージはFILOなどの異なる順序で受信されます。
• 一部のメッセージが失われる場合があります。

チャネルシステムは、本質的には、通信する有限状態マシンのバージョンであり、マシンは個別のプロセスに分割されません。したがって、状態は 1 つであり、どのシステムがどのチャネルで読み取り/書き込みできるかに関する制限はありません。

正式には、プロトコル が与えられた場合、それに関連付けられたチャネル システムは であり、 はおよび の集合です。 ${\displaystyle \langle (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},(M_{i,j})_{i ,j=1}^{n},({\mathtt {成功}})_{i}\rangle }$${\displaystyle \langle \prod (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},\bigcup _{i,j=1 }^{n}(M_{i,j}),\デルタ \rangle }$${\displaystyle \Delta }$${\displaystyle ((s_{1},\dots ,s_{j},\dots ,s_{n}),?m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{j}(s_{j},+m_{i,j}),\dots ,s_{n})}$${\displaystyle ((s_{1},\dots ,s_{i},\dots ,s_{n}),!m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{i}(s_{i},-m_{i,j}),\dots ,s_{n})}$