Barbed bisimulation

Barbed bisimulation refers to an notion of program equivalence which can be defined for any calculus equipped with

• a reduction (i.e. an unlabelled transition)
• a convergence predicate (i.e. some notion of observable behaviour)

As it is a bisimulation at heart, it is often used with process calculi, such as CCS or π-calculus. However, it can also be applied to functional systems too - and in fact has its roots in applicative bisimilarity.

Suppose we have a set \mathcal{T} of terms of a calculus. Suppose further that this set is equipped with

• a reduction relation \rightarrow\ \subseteq \mathcal{T} \times \mathcal{T}, and
• a predicate \Downarrow on terms.

The unary predicate denotes convergence. That is, P\Downarrow means that evaluation of P terminates in a way that is visible to the outside world. There are many meanings to this.

• If we have a \lambda-calculus it could mean that P reduces to a whnf.
• If we have a process calculus, it could mean that P is able to perform a visible action \ell, i.e. that P \xrightarrow{\ell} P' for some other process P'. This \ell is called the barb ("a sharp projection near the end of an arrow, fish hook, or similar object"). In this case it means that P has not gone into livelock, computing forever without interacting with its environment.

Definition. A relation \sim\ \subseteq \mathcal{T} \times \mathcal{T} is called a barbed simulation just if
P \sim Q implies that

1. if P \rightarrow P' then Q \rightarrow Q' for some Q' with P' \sim Q'
2. if P\Downarrow then Q\Downarrow.

Definition. A relation \sim\ \subseteq \mathcal{T} \times \mathcal{T} is called a barbed bisimulation whenever both \sim and \sim^{-1} are barbed simulations.

References

• Barbed bisimulation was first introduced in

@inproceedings{milner_1992,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Barbed bisimulation},
	volume = {623},
	doi = {10.1007/3-540-55719-9_114},
	booktitle = {Automata, {Languages} and {Programming}},
	publisher = {Springer Berlin Heidelberg},
	author = {Milner, Robin and Sangiorgi, Davide},
	editor = {Kuich, W.},
	year = {1992},
	pages = {685--695}
}