2
$\begingroup$

In a process like $$ R \stackrel{def}=((a.\bar{b}.0)\setminus\{b\})[a\to b]\mid(\bar{b}.b.0)+\bar{b}.c.0 $$

$b$ is restricted to perform on the inner process of RHS $(a.\bar{b}.0)\setminus\{b\}$, thereafter the $a$ is relabeled to $b$. What I am confused is in drawing the LTS of it, the $a$ action occur at first process (we can have a transition with label $a$ in the LTS) and it is the next process that renaming takes place? can the following LTS be valid as first actions transitions? (the bar is replaced by underline) enter image description here

$\endgroup$
2
$\begingroup$

I am not completely sure about what is causing your confusion, but perhaps this can help:

$a.\bar{b}.0$ can only perform $a$.

$(a.\bar{b}.0)\setminus\{b\}$ can only perform $a$.

$((a.\bar{b}.0)\setminus\{b\})[a\to b]$ can only perform $b$ (i.e. $a$ after substitution).

The full process $((a.\bar{b}.0)\setminus\{b\})[a\to b]\mid(\bar{b}.b.0)+\bar{b}.c.0$ can perform $b$, $\bar b$ (two distinct ways), and $\tau$ (two distinct ways).

Also note that the unrelated process $((a.\bar{b}.0)[a\to b])\setminus\{b\}$ would instead be stuck.

$\endgroup$
  • $\begingroup$ Thanks, I have edited the question and added LTS. so as you have mentioned there are two distinct Tau actions. my confusion is in that. where do they happen? $\endgroup$ – Amir-Mousavi May 7 '18 at 20:57
  • $\begingroup$ @Amir-Mousavi There should be no $a$ there on the left arrow, only $b$ because of the renaming. The $\tau$s are caused by synchronization, where one side of the parallel does $b$ and the other does $\bar b$. $\endgroup$ – chi May 7 '18 at 21:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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