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: