HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Pi Calculus: Restriction necessary for molecular (atomic) action?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
necessarymolecularcalculusrestrictionactionforatomic

Problem

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

Solution

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.

Context

StackExchange Computer Science Q#40761, answer score: 4

Revisions (0)

No revisions yet.