Parallel
Composition ||

If P and Q are processes then (P||Q) represents the concurrent execution of P and Q.

Replicator
forall

forall [i:1..N] P(i) is the parallel composition (P(1) || … || P(N))

Process
Labeling :

a:P prefixes each label in the alphabet of P with a.

Process
Sharing ::

{a1,..,ax}::P replaces every label n in the alphabet of P with the labels a1.n,…,ax.n. Further, every transition (n->Q) in the definition of P is replaced with the transitions ({a1.n,…,ax.n}->Q).

Priority High <<

||C =(P||Q)<<{a1,…,an} specifies a composition in which the actions a1,…,an have higher priority than any other action in the alphabet of P||Q including the silent action tau. In any choice in this system which has one or more of the actions a1,…,an labeling a transition, the transitions labeled with lower priority actions are discarded.

Priority Low >>

||C=(P||Q)>>{a1,…,an} specifies a composition in which the actions a1,…,an have lower priority than any other action in the alphabet of P||Q including the silent action tau. In any choice in this system which has one or more transitions not labeled by a1,…,an, the transitions labeled by a1,…,an are discarded.