問題提議

たとえば，玄関の電気のスイッチ，リビングの電気のスイッチ，．．．のように，同じモデル:

SWITCH = (on -> off > SWITCH).

を複数個必要とする場合があります．しかし，これを以下のように並列合成してしまうと，問題がおこります．

||TWO_SWITCH = (SWITCH||SWITCH).

これでは，各プロセスの action が shared action として同時に起こってしまうので，単一のスイッチと区別がつかなくなってしまいます．

解決策

そこで，接頭辞をつけて同一名のプロセスを区別します．a:P は，P の alphabet 内の各 action label に a という接頭辞を付けることを表します．

上記のスイッチの場合は，以下のようになります．

||TWO_SWITCH = (a:SWITCH||b:SWITCH).

このときの各プロセスの alphabet は，{a.ou, a.out}, {b.on, b.off} となります．

上の二つの ＬＴＳ を合成すると以下のようになります．