6
$\begingroup$

In "A Calculus of Mobile Processes, Part 1" [1], Milner et al. give an example for transmitting a pair of values $(u,v)$ from the process $P$ to either $R$ or $Q$ (see page 13). All three processes are assumed to run in parallel.

They present following solution:

$$ \begin{align} P &= (w) (\bar{x}(w).P' | \bar{w}u.\bar{w}v.0) \\ Q &= x(w).w(y).w(z).Q' \\ R &= x(w).w(y).w(z).R' \end{align} $$

They claim that "it is vital to this idea that w (...) is indeed a private name". Why is this a necessity?

Wouldn't following solution without restriction work?

$$ \begin{align*} P &= \bar{x}(w).P' | \bar{w}u.\bar{w}v.0 \\ Q &= x(\alpha).\alpha(y).\alpha(z).Q' \\ R &= x(\beta).\beta(y).\beta(z).R' \end{align*} $$

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.159.363&rep=rep1&type=pdf

$\endgroup$

1 Answer 1

4
$\begingroup$

Your solution would work only if you consider $P$, $Q$ and $R$ in parallel as a "closed system", i.e. a system which is not supposed to be composed and interact with an external environment but just to perform internal reactions.

In the context of your quotation, the translation of a polyadic action into a monadic one is supposed to be compositional and to yield a bisimilar labelled semantics. The role of the restriction is to avoid exposing the actions on $w$ to the environment: what happens if the environment performs actions on the public channel in your solution? For instance, consider the process $S$ $$ S = w(y).S' $$ If put in parallel with your version of $P$, $Q$ and $R$ it can "steal" the first/second component of the couple from $Q$ or $R$. This is because you do not need to receive $w$ on $x$ to be able to use it if $w$ is a public name, while that is the only way to acquire it when it is restricted.

$\endgroup$
1
  • $\begingroup$ Oh yes, that would be nasty indeed! :) Thank you for your clear and enlightening answer. $\endgroup$
    – ftl
    Sep 24, 2015 at 23:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.