Communicating Sequential Processes
決定的(または外部)選択演算子は、プロセスの将来を2つのコンポーネントプロセス間の選択で定義可能とするもので、プロセス群と初期イベントとのやり取りによって環境が選択を行うことを可能にする。たとえば
( a → P ) ◻ ( b → Q ) {\displaystyle \left(a\rightarrow P\right)\Box \left(b\rightarrow Q\right)}
は、初期イベント a {\displaystyle {\mathit {a}}} および b {\displaystyle {\mathit {b}}} とやり取りしようとするプロセスであり、環境がどちらの初期イベントとやり取りすることを選択したかによって、 P {\displaystyle {\mathit {P}}} または Q {\displaystyle {\mathit {Q}}} として振舞うようになる。 a {\displaystyle {\mathit {a}}} および b {\displaystyle {\mathit {b}}} と同時にやり取りする場合、選択は非決定的となる。
V e n d i n g M a c h i n e | [ { c o i n , c a r d } ] | P e r s o n ≡ c o i n → c h o c → S T O P {\displaystyle VendingMachine\left\vert \left[\left\{coin,card\right\}\right]\right\vert Person\equiv coin\rightarrow choc\rightarrow STOP}
ここで、同期が "coin" についてのみ必要とされる場合、以下が得られる。
V e n d i n g M a c h i n e | [ { c o i n } ] | P e r s o n ≡ ( c o i n → c h o c → S T O P ) ◻ ( c a r d → S T O P ) {\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)}
名前が示すとおり、CSPは独立したプロセス群がメッセージパッシングによって通信することで相互にやり取りしているものとしてシステムを記述する。しかし、CSPの名称に含まれる "Sequential"(逐次的)という部分は誤解を生じる可能性がある。というのも最近のCSPでは、プロセスは単なる逐次的プロセスだけでなく、より基本的なプロセス群の並列合成で生成されるプロセスも含まれるからである。プロセス間の関係やプロセスが周囲と通信する方法は、各種プロセス代数演算子を使って表される。このような代数的手法を使うことで、少数のプリミティブ要素から容易に極めて複雑なプロセスを構築できる。
その後、ホーアは Stephen Brookes や Bill Roscoe らと共に理論面の改良に取り組み、CSPをプロセス代数的にしていった。この方向性は、同時期にロビン・ミルナーが行っていた Calculus of Communicating Systems(CCS)の研究と相互に影響しあっている。CSPの理論面は1984年に発表され、1985年に出版されたホーアの著書 Communicating Sequential Processes で一般に知られるようになった。2006年9月現在でも、Citeseer によればこの本は計算機科学分野での引用回数第3位とされている(ただし、サンプリング方式であるため信頼性は高くない)。このホーアの著書以降、CSPの理論は若干変更されただけである。変更のほとんどは、CSPプロセス解析と検証のための自動化ツールの出現に対応するものである。Roscoe の The Theory and Practice of Concurrency ではこの新たなCSPが解説されている。
インタフェース並列演算子は、コンポーネントプロセス間で同期を必要とする並行動作を表す。インタフェースにおけるイベントは、全コンポーネントプロセスがそのイベントに関わることが可能な場合にのみ発生する。たとえば、次のプロセス
P | [ { a } ] | Q {\displaystyle P\left\vert \left[\left\{a\right\}\right]\right\vert Q}
は、イベント a {\displaystyle {\mathit {a}}} が発生する前に P {\displaystyle {\mathit {P}}} と Q {\displaystyle {\mathit {Q}}} が共にそのイベントを扱える状態になっている必要があることを意味する。したがって例えば、次のプロセス
文法的に正しいCSPの表現の意味を定義する形式意味論はいくつかある。CSPの理論には、相互に一貫した表示的意味論、代数的意味論、操作的意味論がある。