The process a: P has an alphabet in which every action label in the alphabet of P is prefixed with label a. Processes may also be labelled with a set of labels. The process {a,b}::P has the effect of taking every action prefix of P l and replacing it with the prefix {a.l,b.l}. The example below illustrates the use of sets:
LOCK = (get -> rel -> LOCK). P = (mutex.get -> critical_section -> mutex.rel -> non_critical -> P)@{mutex}. ||SYS = (p1:P || p2:P || {p1,p2}::mutex:LOCK).
The label set {p1,p2} ensures that the processes p1 and p2 do not synchronise on get and rel. The LTS for process {p1,p2}::mutex:LOCK is depicted below: