Process Labeling
問題提議
たとえば,玄関の電気のスイッチ,リビングの電気のスイッチ,...のように,同じモデル:
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} となります.
上の二つの LTS を合成すると以下のようになります.