Hiding and Renaming

We meet some new operators. Hiding (P\X) allows you to conceal the internal actions of a process from the outside world. Renaming (P〚R〛) gives a flexible way of changing the labels on the events that a process communicates into different labels seen by the outside world. We see how hiding can create more natural models of parallel systems but can create a few theoretical difficulties, and how renaming combined with parallelism can create seemingly magical effects such as allowing Adam and Eve to achieve a variable renaming so each can have their own choice of apple. We introduce link parallel: a combination of parallel, hiding and renaming that makes constructing practical networks comparatively simple, and see how it can be used in building some natural dynamic networks such as one for implementing mergesort. We find that renaming can help FDR solve Sudoku puzzles faster.

1. 1.

   Some other process algebras, notably CCS, combine parallel and hiding into a single operator: they do not factor the ‘natural’ operator into two parts like CSP.

2. 2.

   This is exactly how FDR and ProBE represent nondeterministic choice, as previously described in Sect. 1.6.

3. 3.

   TPC identifies the process \(P\rhd Q\) with \( \left( {P\,\sqcap \,STOP} \right)\,\square \,Q \). This identification is correct, if a little hard to understand, in the theories of CSP that TPC considers. Since we will consider a number of theories in later chapters where it is not correct to identify these two terms, we prefer to think of \(\rhd\) as a primitive operator rather than one derived from others.

4. 4.

   See p. 203 for further discussion of this point.

5. 5.

   It is possible to achieve the effect of variable renaming by combining one-to-many renaming with parallel combination with a process that chooses the appropriate image of an event for the current trace. See Exercise 5.10 below.

6. 6.

   Chaining (≫) is sometimes called piping.

7. 7.

   A similar implementation of Hoare’s Quicksort can be found in TPC.

Authors and Affiliations

1. Oxford University Computing Laboratory, Wolfson Bldg., Parks Road, Oxford, OX1 3QD, UK

   Prof. A. W. Roscoe

Corresponding author

Correspondence to A. W. Roscoe .

Reprints and permissions

© 2010 Springer-Verlag London Limited

Policies and ethics