Communicating Sequential Processes
より形式的に表せば、プロセス P {\displaystyle P} のトレースモデルでの意味は t r a c e s ( P ) ⊆ Σ ∗ {\displaystyle traces\left(P\right)\subseteq \Sigma ^{\ast }} として定義される。すなわち、
⟨ ⟩ ∈ t r a c e s ( P ) {\displaystyle \langle \rangle \in traces\left(P\right)} ( t r a c e s ( P ) {\displaystyle traces\left(P\right)} は空のシーケンスを含む)
s 1 ⌢ s 2 ∈ t r a c e s ( P ) ⟹ s 1 ∈ t r a c e s ( P ) {\displaystyle s_{1}\smallfrown s_{2}\in traces\left(P\right)\implies s_{1}\in traces\left(P\right)} ( t r a c e s ( P ) {\displaystyle traces\left(P\right)} はプレフィックスで閉じている)
CSP には様々な代数演算子がある。主なものを以下に挙げる。
失敗/発散モデルは、失敗モデルを発散(divergence)を扱えるよう拡張したものである。失敗/発散モデルにおけるプロセスは ( f a i l u r e s ⊥ ( P ) , d i v e r g e n c e s ( P ) ) {\displaystyle \left(failures_{\perp }\left(P\right),divergences\left(P\right)\right)} という対で表され、 d i v e r g e n c e s ( P ) {\displaystyle divergences\left(P\right)} は発散を生じさせる全トレースの集合である。また、 f a i l u r e s ⊥ ( P ) = f a i l u r e s ( P ) ∪ { ( s , X ) | s ∈ d i v e r g e n c e s ( P ) } {\displaystyle failures_{\perp }\left(P\right)=failures\left(P\right)\cup \left\{\left(s,X\right)\vert s\in divergences\left(P\right)\right\}} が成り立つ。