Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Can someone help me understand why $ L( P ) = a^n b^n c^n $ in the following pi - calculus process

$$ P = ( \nu k_1, k_2, k_3, u_{b} , u_c)( \overline{k_1} \mid \overline{k_2} \mid Q_a \mid Q_b \mid Q_c) $$

$$Q_a = {!}k_1.a.( \overline{k_1} \mid \overline{k_3} \mid \overline{u_b} \mid \overline{u_c})$$

$$Q_{b} = k_1.!k_3.k_2.u_b.b.\overline{k_2}$$

$$Q_{c} = k_2.(! u_c.c \mid u_b.\mathrm{DIV} )$$

where $DIV = !τ$

share|improve this question
    
Can somebody create a tag for process-algebra as this ques lies there .... –  user8250 Nov 3 '11 at 20:58
1  
What is your definition of $L(P)$? It seems to me that the process can emit $ac$ and then diverge. Shouldn't that make $ac\in L(P)$? But $ac\not\in a^nb^nc^n$. –  Henning Makholm Nov 3 '11 at 21:27
    
$L(P)$ has been defined as the language that is weakly terminating that is all sequences that can be generated without the divergence... –  user8250 Nov 4 '11 at 19:57
add comment

1 Answer

At the beginning, there is a waiting $\overline{k_1}$. It can be consumed by reducing $Q_a$, which immediately puts one back, or it can be consumed by reducing $Q_b$, which gets rid of $\overline{k_1}$ forever (thus preventing $Q_a$ from reducing ever again). Thus, once a $b$ has been emitted, no $a$ can be emitted any longer. By the same reasoning on $\overline{k_2}$, once a $c$ has been emitted, no $b$ can be emitted any longer. Hence all traces of $P$ match $a^* b^* c^*$.

Let $a^n b^p c^q$ be a trace of $P$: Emitting a $b$ requires an input on $u_b$. There are exactly as many inputs on $u_b$ as there are reductions of the replication in $Q_a$, which is as many as $a$'s are emitted. Hence $p \leq n$. By the same reasoning on $u_c$, each emission on $c$ requires one prior emission on $a$, hence $q \leq n$.

If $p < n$ and the system isn't just about to emit a $b$ in $Q_b$, then there is at least one spare $\overline{u_b}$. We saw previously that there is at most one $\overline{k_2}$; let us refine the analysis:

  • If there is a $\overline{k_2}$, then $Q_c$ must be intact. $Q_b$ may have become $!k_3.k_2.u_b.b.\overline{k_2}$, which can progress because there is a spare $\overline{k_3}$ produced together with the spare $\overline{u_b}$; or it may have become $(!k_3.k_2.u_b.b.\overline{k_2}) \mid k_2.u_b.b.\overline{k_2}$, which can progress since there is an outstanding output on $k_2$.
  • If the last $\overline{k_2}$ was consumed within $Q_b$, then the leftover from the replication must be either $u_b.b.\overline{k_2}$, which can progress by emitting that spare $\overline{u_b}$, or $b.\overline{k_2}$ or $\overline{k_2}$ which can progress to put back an $\overline{k_2}$.
  • Otherwise the last $\overline{k_2}$ must have been consuming by reducing $Q_c$. Then that spare $\overline{u_b}$ must lead to a divergence.

In any case, a complete, non-diverging trace cannot have a spare $\overline{u_b}$ and thus has $p = n$.

Now suppose $q < p = n$: As before, if the system isn't about to emit a $c$ in $Q_c$, then there is a spare $\overline{u_c}$. If $Q_b$ hasn't started reducing yet, then either there is a $\overline{k_1}$ and $Q_a$ can reduce, or $Q_a$ is in the process of reducing; either way the system can progress. Since $p = n$, there cannot be a spare $\overline{k_3}$ for the replication in $Q_b$ to progress. So either there is a spare $\overline{k_2}$ and $Q_c$ can start reducing, or there is none and $Q_c$ has already been reduced. There is no spare $\overline{u_b}$ because that would require $p < n$. But as long as there is a spare $\overline{u_c}$, the replication in $Q_c$ can progress and emit a $c$.

We've shown that any complete, terminating trace of $P$ is of the form $a^n b^n c^n$. Showing that $P$ can emit all such traces is left as an easy exercise for the reader.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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