プロセス代数CSP

Communicating Sequential Processes（CSP）とは並行システムを相互作用するプロセスの群として捉え記述し、その正しさを数学的に証明するための仕様記述言語である。
ここで、相互作用とは特にイベントと呼ばれシステムに応じて定義する。プロセスはイベントとCSPの代数演算子により以下のように定義される。

PROC = SKIP                     (正常終了)
       STOP                     (停止)
       event   ->     PROC      (接頭辞 prefix)
       PROC     \     {c}       (隠蔽 hiding)
       PROC [[e1<-e2]]          (変更 renaming)
       PROC     ;     PROC      (逐次 sequential)
       PROC    /\     PROC      (割り込み interrupt)
       PROC    [>     PROC      (untimed timeout)
       PROC    []     PROC      (外部選択 external choice)
       PROC    |~|    PROC      (内部選択 internal choice)
       PROC    |||    PROC      (interleaving)
       PROC   [|c|]   PROC      (sharing)
       PROC [c1||c2]  PROC      (alphabetized parallel)
       PROC [e1<->e2] PROC      (linked parallel)
       if b then PROC else PROC (条件選択 boolean)

PROC  :プロセス
e1,e2 :イベント
c1,c2 :イベントの集合
b     :boolean式

例えば、a,bをイベントとすると prefixにより、 a -> SKIP や b -> STOP はプロセスとなる。さらにこれらプロセスの外部選択 (a -> SKIP) [] (b -> STOP) もプロセスとなる。さらに・・・

このようにして複雑な振る舞いをするプロセス（システム）を記述していく。各演算子について次章以降で例を交え説明していく。