Communicating Sequential Processes
隠蔽演算子は、何らかのイベントを観測不可能とすることでプロセスの抽象化手段を提供する。隠蔽の例として次の
( a → P ) ∖ { a } {\displaystyle \left(a\rightarrow P\right)\setminus \left\{a\right\}}
は、イベント a {\displaystyle {\mathit {a}}} が P {\displaystyle {\mathit {P}}} の中で出現しないものとすると、以下のように省略可能である。
P {\displaystyle {\mathit {P}}}
この合成プロセスを "coin" と "card" というイベントを隠蔽することで抽象化すると、次のようになる。
( ( c o i n → c h o c → S T O P ) ◻ ( c a r d → S T O P ) ) ∖ { c o i n , c a r d } {\displaystyle \left(\left(coin\rightarrow choc\rightarrow STOP\right)\Box \left(card\rightarrow STOP\right)\right)\setminus \left\{coin,card\right\}}
以上から、次の非決定性プロセスが得られる。
( c h o c → S T O P ) ⊓ S T O P {\displaystyle \left(choc\rightarrow STOP\right)\sqcap STOP}
これは、"choc" イベント後に停止するか、単に停止するプロセスである。言い換えれば、システムを外部から見たものとして上記抽象化を扱えば(すなわち、人間が行った決定を無視すれば)、非決定性が生じる。