# Late and Early Bisimulation

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?

• Do these concepts make sense in a generic LTS? I only know (or knew, it's been a while) them in the context of the pi-calculus and family. Wikipedia has definitions but the article fails to convey useful intuitions. All these adjectival bisimulations come into play because actions are complex beasts whose meaning depends on what happened before. – Gilles 'SO- stop being evil' Mar 21 '12 at 16:35
• You're right (again). – Dave Clarke Mar 21 '12 at 17:11

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.