通信プロセスの代数

通信プロセス代数 (ACP) は、並行システムについての推論に対する代数的アプローチです。これは、プロセス代数またはプロセス計算として知られる並行性の数学的理論のファミリーのメンバーです。ACP は、1982 年にJan BergstraとJan Willem Klopによって最初に開発されました^[1]。これは、保護されていない再帰方程式の解を調査する取り組みの一環として行われました。他の重要なプロセス計算 ( CCSおよびCSP ) よりも、ACP の開発はプロセスの代数に重点を置き、プロセスの抽象的で一般化された公理系を作成することを目指しました^[2] 。実際、プロセス代数という用語は、ACP につながった研究中に造られました。^[要出典]

ACP は、基本的には普遍代数の意味での代数です。この代数は、他のプロセスまたは特定の基本要素の構成を定義する代数プロセス式でシステムを記述する方法です。

ACP は、瞬間的なアトミック アクション( ) をプリミティブとして使用します。デッドロックや停滞を表すアクション や、サイレント アクション(特定の ID を持たない抽象化されたアクション)を表すアクションなど、一部のアクションには特別な意味があります。 ${\displaystyle {\mathit {a,b,c,...}}}$${\displaystyle \delta}$${\displaystyle \tau}$

さまざまな演算子を使用して、アクションを組み合わせてプロセスを形成できます。これらの演算子は、基本的なプロセス代数、並行性、および通信を提供するものとして大まかに分類できます。

• 選択と順序付け– 最も基本的な代数演算子は、アクション間の選択を提供する代替演算子（ ）と、アクションの順序を指定する順序付け演算子（）です。たとえば、プロセス${\displaystyle +}$${\displaystyle \cdot}$

${\displaystyle (a+b)\cdot c}$

まず、またはのいずれかを実行することを選択し、次にアクション を実行します。との選択がどのように行われるかは重要ではなく、未指定のままです。代替構成は交換可能ですが、順次構成は交換不可能であることに注意してください (時間が順方向に流れるため)。${\displaystyle {\mathit {a}}}$${\displaystyle {\mathit {b}}}$${\displaystyle {\mathit {c}}}$${\displaystyle {\mathit {a}}}$${\displaystyle {\mathit {b}}}$

• 並行性– 並行性を記述できるように、ACP はマージ演算子と左マージ演算子を提供します。マージ演算子は、個々のアクションがインターリーブされた 2 つのプロセスの並列合成を表します。左マージ演算子は、マージと同様の意味を持つ補助演算子ですが、常に左側のプロセスから最初のステップを選択することを約束します。例として、プロセス${\displaystyle \vert \vert }$${\displaystyle \vert \lfloor }$

${\displaystyle (a\cdot b)\vert \vert (c\cdot d)}$

いずれのシーケンスでもアクションを実行できます。一方、プロセス${\displaystyle a,b,c,d}$${\displaystyle abcd,acbd,acdb,cabd,cadb,cdab}$

${\displaystyle (a\cdot b)\vert \lfloor (c\cdot d)}$

左マージ演算子によってアクションが最初に実行されることが保証されるため、シーケンスのみを実行できます。${\displaystyle abcd,acbd,acdb}$${\displaystyle {\mathit {a}}}$

• 通信— プロセス間の相互作用（または通信）は、バイナリ通信演算子を使用して表されます。たとえば、アクションとアクションは、それぞれデータ項目の読み取りと書き込みとして解釈できます。この場合、プロセスは${\displaystyle \vert}$${\displaystyle r(d)}$${\displaystyle w(d)}$${\displaystyle d\in D=\{1,2,3,\ldots \}}$

${\displaystyle \left(\sum _{d\in D}r(d)\cdot y\right)\vert (w(1)\cdot z)}$

は、右側のコンポーネント プロセスから左側のコンポーネント プロセスに値を伝達し(つまり、識別子は値 にバインドされ、プロセス内の の空きインスタンスはその値を引き継ぎます)、その後、とのマージとして動作します。${\displaystyle 1}$${\displaystyle {\mathit {d}}}$${\displaystyle 1}$${\displaystyle {\mathit {d}}}$${\displaystyle {\mathit {y}}}$${\displaystyle {\mathit {y}}}$${\displaystyle {\mathit {z}}}$

• 抽象化— 抽象化演算子 は、特定のアクションを「非表示」にして、モデル化されているシステムの内部イベントとして扱う方法です。抽象化されたアクションは、サイレント ステップアクションに変換されます。場合によっては、これらのサイレント ステップを抽象化プロセスの一部としてプロセス式から削除することもできます。たとえば、${\displaystyle \tau_{I}}$${\displaystyle \tau}$

${\displaystyle \tau _{\{c\}}((a+b)\cdot c)=(a+b)\cdot \tau }$

この場合は、

${\displaystyle a+b}$

イベントはもはや観察可能ではなく、観察可能な影響もないため。${\displaystyle {\mathit {c}}}$

ACP は基本的に、さまざまな演算子の正式な定義に公理的、代数的なアプローチを採用しています。以下に示す公理は、ACP の完全な公理システム(抽象化された ACP) を構成します。 _{${\displaystyle \tau}$}

代替および順次合成演算子を使用して、ACPは公理を満たす基本的なプロセス代数を定義します^[3]

${\displaystyle {\begin{matrix}x+y&=&y+x\\(x+y)+z&=&x+(y+z)\\x+x&=&x\\(x+y)\cdot z&=&(x\cdot z)+(y\cdot z)\\(x\cdot y)\cdot z&=&x\cdot (y\cdot z)\end{matrix}}}$

基本的な代数を超えて、2つの追加の公理が代替演算子と順序付け演算子、およびデッドロックアクションの関係を定義します。${\displaystyle \delta}$

${\displaystyle {\begin{matrix}\delta +x&=&x\\\delta \cdot x&=&\delta \end{matrix}}}$

マージ、左マージ、通信演算子に関連する公理は^{[3]である。}

${\displaystyle {\begin{matrix}x\vert \vert y&=&x\vert \lfloor y+y\vert \lfloor x+x\vert y\\a\cdot x\vert \lfloor y&=&a\cdot (x\vert \vert y)\\a\vert \lfloor y&=&a\cdot y\\(x+y)\vert \lfloor z&=&(x\vert \lfloor z)+(y\vert \lfloor z)\\a\cdot x\vert b&=&(a\vert b)\cdot x\\a\vert b\cdot x&=&(a\vert b)\cdot x\\a\cdot x\vert b\cdot y&=&(a\vert b)\cdot (x\vert \vert y)\\(x+y)\vert z&=&x\vert z+y\vert z\\x\vert (y+z)&=&x\vert y+x\vert z\end{行列}}}$

通信演算子がプロセスではなくアクションのみに適用された場合、それはアクションからアクションへのバイナリ関数として解釈されます。この関数の定義は、プロセス間の可能な相互作用を定義します。相互作用を構成しないアクションのペアはデッドロックアクションにマッピングされ、許可された相互作用のペアは相互作用の発生を表す対応する単一のアクションにマッピングされます。たとえば、通信関数は次のように指定します。 ${\displaystyle \vert :A\times A\rightarrow A}$${\displaystyle \delta}$

${\displaystyle a\vert a\rightarrow c}$

これは、成功した相互作用がアクション に還元されることを示しています。ACP には、に対するカプセル化演算子も含まれており、これは失敗した通信試行 (つまり、通信関数によって還元されていない の要素) をデッドロックアクションに変換するために使用されます。通信関数とカプセル化演算子に関連する公理は^[3]です。${\displaystyle a\vert a}$${\displaystyle c}$${\displaystyle \partial_{H}}$${\displaystyle H\subseteq A}$${\displaystyle H}$

${\displaystyle {\begin{matrix}a\vert b&=&b\vert a\\(a\vert b)\vert c&=&a\vert (b\vert c)\\a\vert \delta &=&\delta \\\partial _{H}(a)&=&a{\mbox{ if }}a\notin H\\\partial _{H}(a)&=&\delta {\mbox{ if }}a\in H\\\partial _{H}(x+y)&=&\partial _{H}(x)+\partial _{H}(y)\\\partial _{H}(x\cdot y)&=&\partial _{H}(x)\cdot \partial _{H}(y)\\\end{matrix}}}$

抽象化演算子に関連する公理は^{[3]である。}

${\displaystyle {\begin{matrix}\tau _{I}(\tau )&=&\tau \\\tau _{I}(a)&=&a{\mbox{ if }}a\notin I\\\tau _{I}(a)&=&\tau {\mbox{ if }}a\in I\\\tau _{I}(x+y)&=&\tau _{I}(x)+\tau _{I}(y)\\\tau _{I}(x\cdot y)&=&\tau _{I}(x)\cdot \tau _{I}(y)\\\partial _{H}(\tau )&=&\tau \\x\cdot \tau &=&x\\\tau \cdot x&=&\tau \cdot x+x\\a\cdot (\tau \cdot x+y)&=&a\cdot (\tau \cdot x+y)+a\cdot x\\\tau \cdot x\vert \lfloor y&=&\tau \cdot (x\vert \vert y)\\\tau \vert \lfloor x&=&\tau \cdot x\\\tau \vert x&=&\delta \\x\vert \tau &=&\delta \\\tau \cdot x\vert y&=&x\vert y\\x\vert \tau \cdot y&=&x\vert y\end{matrix}}}$

上記のリストのアクションaは値 δ を取る可能性があることに注意してください (ただし、もちろん δ は抽象集合Iに属することはできません)。

ACP は、並行システムを記述および分析するために使用できる他のいくつかの形式の基礎またはインスピレーションとして機能しています。

• ペソ
• マイクロCRL
• ｍCRL2
• HyPA — ハイブリッドシステムのためのプロセス代数^[4]