Communicating Sequential Processes

プリミティブ

CSP は、そのプロセス代数における2種類のプリミティブのクラスを提供する。

イベント

イベントとは、通信あるいは相互作用を意味する。不可分で瞬間的なものと見なされる。不可分名（たとえば、${\displaystyle {\mathit {on}}}$、${\displaystyle {\mathit {off}}}$）、複合名（たとえば、${\displaystyle valve.open}$、${\displaystyle valve.close}$）、入出力イベント（たとえば、${\displaystyle mouse?xy}$、${\displaystyle screen!bitmap}$）などがある。

プリミティブプロセス

プリミティブプロセスとは、基本的振る舞いを表したものである。たとえば、${\displaystyle {\mathit {STOP}}}$（まったく通信しないプロセスであり、デッドロックとも言う）や${\displaystyle {\mathit {SKIP}}}$（成功裡に終了することを表す）がある。

代数演算子

CSP には様々な代数演算子がある。主なものを以下に挙げる。

プレフィックス

プレフィックス演算子は、イベントとプロセスを結合して新たなプロセスを生成する。たとえば、

${\displaystyle a\rightarrow P}$

は、${\displaystyle {\mathit {a}}}$ にその環境と通信させようとするプロセスであり、${\displaystyle {\mathit {a}}}$ の後では、プロセス ${\displaystyle {\mathit {P}}}$ として振舞う。

決定的選択

決定的（または外部）選択演算子は、プロセスの将来を2つのコンポーネントプロセス間の選択で定義可能とするもので、プロセス群と初期イベントとのやり取りによって環境が選択を行うことを可能にする。たとえば

${\displaystyle \left(a\rightarrow P\right)\Box \left(b\rightarrow Q\right)}$

は、初期イベント ${\displaystyle {\mathit {a}}}$ および ${\displaystyle {\mathit {b}}}$ とやり取りしようとするプロセスであり、環境がどちらの初期イベントとやり取りすることを選択したかによって、${\displaystyle {\mathit {P}}}$ または ${\displaystyle {\mathit {Q}}}$ として振舞うようになる。${\displaystyle {\mathit {a}}}$ および ${\displaystyle {\mathit {b}}}$ と同時にやり取りする場合、選択は非決定的となる。

非決定的選択

非決定的（または内部）選択演算子は、プロセスの将来を2つのコンポーネントプロセス間の選択で定義可能とするものだが、環境がどちらのコンポーネントプロセスを選択するかを制御できない。たとえば

${\displaystyle \left(a\rightarrow P\right)\sqcap \left(b\rightarrow Q\right)}$

は、${\displaystyle \left(a\rightarrow P\right)}$ または ${\displaystyle \left(b\rightarrow Q\right)}$ のどちらかとして振舞う。${\displaystyle {\mathit {a}}}$ または ${\displaystyle {\mathit {b}}}$ を受容することを拒否でき、環境が ${\displaystyle {\mathit {a}}}$ と ${\displaystyle {\mathit {b}}}$ の両方を提供する場合にそれとやり取りするだけである。決定的選択で選択肢である2つの初期イベントが同一である場合、非決定性が生じる。したがってたとえば、

${\displaystyle \left(a\rightarrow a\rightarrow STOP\right)\Box \left(a\rightarrow b\rightarrow STOP\right)}$

は次と等価である。

${\displaystyle a\rightarrow \left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)}$

インターリーブ

インターリーブ演算子は、完全に独立した並行動作を表す。次のプロセス

${\displaystyle P\;\vert \vert \vert \;Q}$

は、${\displaystyle {\mathit {P}}}$ と ${\displaystyle {\mathit {Q}}}$ が同時並行に動作することを意味する。両方のプロセスが発生するイベントは時系列上でインターリーブされる。

インタフェース並列

インタフェース並列演算子は、コンポーネントプロセス間で同期を必要とする並行動作を表す。インタフェースにおけるイベントは、全コンポーネントプロセスがそのイベントに関わることが可能な場合にのみ発生する。たとえば、次のプロセス

${\displaystyle P\left\vert \left[\left\{a\right\}\right]\right\vert Q}$

は、イベント ${\displaystyle {\mathit {a}}}$ が発生する前に ${\displaystyle {\mathit {P}}}$ と ${\displaystyle {\mathit {Q}}}$ が共にそのイベントを扱える状態になっている必要があることを意味する。したがって例えば、次のプロセス

${\displaystyle \left(a\rightarrow P\right)\left\vert \left[\left\{a\right\}\right]\right\vert \left(a\rightarrow Q\right)}$

は、イベント ${\displaystyle {\mathit {a}}}$ を扱うことができ、次のように表せる。

${\displaystyle P\left\vert \left[\left\{a\right\}\right]\right\vert Q}$

一方

${\displaystyle \left(a\rightarrow P\right)\left\vert \left[\left\{a,b\right\}\right]\right\vert \left(b\rightarrow Q\right)}$

は、単純なデッドロックを意味する。

隠蔽

隠蔽演算子は、何らかのイベントを観測不可能とすることでプロセスの抽象化手段を提供する。隠蔽の例として次の

${\displaystyle \left(a\rightarrow P\right)\setminus \left\{a\right\}}$

は、イベント ${\displaystyle {\mathit {a}}}$ が ${\displaystyle {\mathit {P}}}$ の中で出現しないものとすると、以下のように省略可能である。

${\displaystyle {\mathit {P}}}$

例

簡単なCSPの例として、チョコレートの自動販売機の抽象表現とチョコレートを購入しようとしている人との相互作用を考える。この自動販売機は2つのイベント "coin" と "choc" を扱う。"coin" は代金の投入を表し、"choc" はチョコレートの引渡しを表す。チョコレートを渡す前に代金の支払いを要求する機械は次のように記述される。

${\displaystyle VendingMachine=coin\rightarrow choc\rightarrow STOP}$

支払いに硬貨またはカードを使う人は、以下のようにモデル化される。

${\displaystyle Person=(coin\rightarrow STOP)\Box (card\rightarrow STOP)}$

これら2つのプロセスを並列に置くことで、互いにやり取りできるようにする。合成プロセスの振る舞いは、2つのプロセスが同期しなければならないイベント依存する。すなわち、

${\displaystyle VendingMachine\left\vert \left[\left\{coin,card\right\}\right]\right\vert Person\equiv coin\rightarrow choc\rightarrow STOP}$

ここで、同期が "coin" についてのみ必要とされる場合、以下が得られる。

${\displaystyle VendingMachine\left\vert \left[\left\{coin\right\}\right]\right\vert Person\equiv \left(coin\rightarrow choc\rightarrow STOP\right)\Box \left(card\rightarrow STOP\right)}$

この合成プロセスを "coin" と "card" というイベントを隠蔽することで抽象化すると、次のようになる。

${\displaystyle \left(\left(coin\rightarrow choc\rightarrow STOP\right)\Box \left(card\rightarrow STOP\right)\right)\setminus \left\{coin,card\right\}}$

以上から、次の非決定性プロセスが得られる。

${\displaystyle \left(choc\rightarrow STOP\right)\sqcap STOP}$

これは、"choc" イベント後に停止するか、単に停止するプロセスである。言い換えれば、システムを外部から見たものとして上記抽象化を扱えば（すなわち、人間が行った決定を無視すれば）、非決定性が生じる。

構文

CSPの構文は、プロセスとイベントの結合の「正当な」方法を定義する。${\displaystyle {\mathit {e}}}$ をイベント、${\displaystyle {\mathit {X}}}$ をイベントの集合とする。するとCSPの基本構文は以下のように定義される。

${\displaystyle {\begin{array}{lcll}{Proc}&::=&\mathrm {STOP} &\;\\&|&\mathrm {SKIP} &\;\\&|&e\rightarrow {Proc}&({\text{prefixing}})\\&|&{Proc}\;\Box \;{Proc}&({\text{external}}\;{\text{choice}})\\&|&{Proc}\;\sqcap \;{Proc}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{Proc}\;\vert \vert \vert \;{Proc}&({\text{interleaving}})\\&|&{Proc}\;|[\{X\}]|\;{Proc}&({\text{interface}}\;{\text{parallel}})\\&|&{Proc}\setminus X&({\text{hiding}})\\&|&{Proc}\;;{Proc}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{Proc}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{Proc}\;\triangleright \;{Proc}&({\text{timeout}})\\&|&{Proc}\;\triangle \;{Proc}&({\text{interrupt}})\end{array}}}$

註：上記の構文では簡潔にするため、発散 (計算機科学)（英語版）を表す${\displaystyle \mathbf {div} }$プロセスや、アルファベット付き並列、パイピング、インデックス付き選択などの様々な演算子を省略している。

形式意味論

この節の加筆が望まれています。

文法的に正しいCSPの表現の意味を定義する形式意味論はいくつかある。CSPの理論には、相互に一貫した表示的意味論、代数的意味論、操作的意味論がある。