Relabelling functions are applied to processes and change the names of action labels. This is usually done to ensure that composed processes synchronise on the correct actions. A relabelling function can be applied to both primitive and composite processes. However, it is generally more used in composition. The general form of the relabelling function is /{newlabel_1/oldlabel_1,…. , newlabel_n/oldlabel_n}. The example shows the composition of two binary semaphore processes to give a semaphore which can be incremented twice (by up). The diagram shows how the down action of the first SEMA process is associated with the up action of the next semaphore by relabelling both to mid.

SEMA = (up -> down -> SEMA).
||SEMA2 = ( SEMA/{mid/down} || SEMA/{mid/up} ).

The alphabet of SEMA2 is {up, down, mid} and its LTS is depicted below:

The following alternative definition of SEMA2 generates exactly the same LTS. In this case, the relabelling function is applied to the composite process rather than its constituent processes.

SEMA = (up -> down -> SEMA).
||SEMA2 = ( first:SEMA|| second:SEMA )
          /{ up/first.up,
	     mid/first.down,
             mid/second.up,
             down/second.down}.

 This may look rather clumsy compared to the first definition, however, it does lead to an elegant definition of a semaphore which can accept N increments.

SEMA = (up->down->SEMA).
||SEMAPHORE(N=4) = (sema[0..N-1]:SEMA(N))
		   /{sema[i:0..N-2].down/sema[i+1].up,
		     up/sema[0].up,
		     down/sema[N-1].down}.

Note that ranges can be used in relabelling functions. In the example, sema[i].down replaces sema[i+1].up.