Late and Early Bisimulation

Question

This is a follow up to my earlier questions on coinduction and bisimulation.

A relation $R \subseteq S \times S$ on the states of an LTS is a bisimulation iff $\forall (p,q)\in R,$ $$ \begin{array}{l} \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R \text{ and } \\ \text{ if } q \stackrel\alpha\rightarrow q' \text{ then } \exists p', \; p \stackrel\alpha\rightarrow p' \text{ and } (p',q')\in R. \end{array} $$

This is a very powerful and very natural notion, after you come to appreciate it. But it's not the only notion of bisimulation. In special circumstances, such as in the context of the $\pi$-calculus, other notions such as open, branching, weak, barbed, late and early bisimulation exist, though I do not fully appreciate the differences. But for this question, I want to limit focus just two notions.

What are late and early bisimulation and why would I use one of these notions instead of standard bisimulation?

Answer 1

Late and early only make sense when building the LTS. The notion of bisimulation stays the same.

However there are several notion of bisimilarities in the π-calculus for example. These are related to how new names are handled. It happens in the π-calculus because it is a name-passing process calculus. There is no such thing in CCS where names cannot be sent.

Usually, the notion of barbed equivalence or congruence is more unanimous. Then you have to prove the equivalence with the late/early/open bisimilarity to give it some credit.

To be quick about it, early transitions are that way: $$ a(x).P \stackrel{a(b)}{\longrightarrow} P[b/x] \qquad \begin{array}{c} P \stackrel{a(b)}{\longrightarrow} P' \quad Q \stackrel{\overline ab}{\longrightarrow} Q' \\ \hline P\mid Q → P' \mid Q' \end{array} $$

and late are like this: $$ a(x).P \stackrel{a(x)}{\longrightarrow} P \qquad \begin{array}{c} P \stackrel{a(x)}{\longrightarrow} P' \quad Q \stackrel{\overline ab}{\longrightarrow} Q' \\ \hline P\mid Q → P'[b/x] \mid Q' \end{array} $$

You see the difference is subtle and is just about where the substitution is done. My preference go to the late one because when I reason about processes, I just remember that the $x$ in the transition $a(x)$ is bound. Also the late bisimilarity is the strongest one (beside the open one which is really not the same) and the processes that are early but not late bisimilar are kind of weird, so you don't lose much.