Communicating Sequential Processes
ここで、 Σ ∗ {\displaystyle \Sigma ^{\ast }} は考えられる全てのイベントの有限な並びの集合である。
安定失敗モデルはトレースモデルを拒絶集合(refusal set)で拡張したものである。拒絶集合とは、プロセスが実行を拒絶できるイベントの集合 X ⊆ Σ {\displaystyle X\subseteq \Sigma } である。失敗(failure)は ( s , X ) {\displaystyle \left(s,X\right)} という対で表される。ここで s {\displaystyle s} はトレース、 X {\displaystyle X} は拒絶集合であり、トレース s {\displaystyle s} が実行されたときそのプロセスが拒絶するイベント群を表す。安定失敗モデルにおけるプロセスの観測された振る舞いは、 ( t r a c e s ( P ) , f a i l u r e s ( P ) ) {\displaystyle \left(traces\left(P\right),failures\left(P\right)\right)} という対で表される。例えば、