Back

Example of contextual equivalent processes

We describe two contextual equivalent processes which must be distinguished.Example 2

Let $P$ and $Q$ be the processes as follows:

$\begin{array}[t]{ll}P\stackrel{\mbox{\scriptsize\it def}}{=}a[P_1]+a[P_2].\\......]+b[].\\Q_2\stackrel{\mbox{\scriptsize\it def}}{=}a[Q_2]+c[].\\\end{array}$

According to Definition .1 for ``+'', $P$ and $Q$ have the following structure:

$$\hspace{-.5em}\begin{array}[t]{ll}P\equiv (\nu \mbox{\it ......rash}[\mbox{\it out $a$}]\vert Q_2)] ).\end{array}\end{array}$$

The behavior of $P$ and $Q$ are illustrated by Fig. 1.

Fig 1: Process $P$ and process $Q$

The problem of these processes were originally shown by Brinksma for CCS processes. When the traveling ambient $n[!\mbox{\it in $a$}\vert\mbox{\it in $c$}]$ is running parallel to the process $P$, the traveling ambient will be able to enter into the ambient $b[]$ in $P$ though this may be impossible when the traveling ambient is running parallel to $Q$. Contextual equivalence, however, identifies $P$ and $Q$. Intuitively, $P$ and $Q$ are the processes as follows:
 

$$\begin{array}[t]{lll}P&\doteq&a[a[a[a[\cdots] +b[]]+c[]]+b[......]]+b[]]\\& &+a[a[a[a[\cdots] +c[]]+c[]]+c[]].\\\end{array}$$

If ``+'' is a primitive operator, any times of opening of ambient $a$, that is, $\mbox{\it open $a$}.,\ldots,.\mbox{\it open $a$}$ for $P$ exhibits the pair of ambients$a[]$ and $b[]$ or $a[]$ and $c[]$. The same opening operation for $Q$ can exhibits the same pair of ambient. $\Box$

Our ``+'' operator defined in Definition .1 can be used like a primitive operator and when it works as primitive one, the above explanation holds. While, our ``+'' is a macro defined by using parallel operator, there exists a case in which ambients $a[]$,$b[]$ and $c[]$ are exhibited at the same time for $P$. The next example shows this situation:Example 3   Let $P$ and $Q$ be the processes defined in Example 2 and ${\cal C}$ be a context as follows:

$${\cal C}=n[!\mbox{\it in $a$}] \vert !\mbox{\it open $a$} \vert -.$$

We can observe ambients $a[],b[]$ and $c[]$ at the same time in the following computation for $\mbox{${\cal C}(P)$}$:
 

$$\hspace{-2em}\begin{array}[t]{ll}\mbox{${\cal C}(P)$}\mbox......h}[\mbox{\it out $a$}]\\\vert P_1 \vert P_2 ).\end{array}$$

Thus, ambients $a[],b[]$ and $c[]$ in $P_1$ and $P_2$ are exhibited. But, the same context ${\cal C}$ will exhibit $a[],b[]$ and $c[]$ for$Q$ in the same sequence, thus, the procedure for proving contextual equivalence can not distinguish $P$ from $Q$. $\Box$

 Back