\documentclass[11pt]{article}		% Fontsize 11 point
\textwidth    		6.5 in		% paper = 8.5x11in
\textheight   		8.58in          %  + foot 30pt = 9.00in
\oddsidemargin		0   pt          % 1 inch margin comes for free
\evensidemargin 	0   pt          % 1 inch margin comes for free
\topmargin      	0   pt          % 4 margins of 1in each
\headheight     	0   pt          % default 12pt = 0.42cm       
\headsep        	0   pt          % default 25pt = 0.88cm       

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			Theorem-like environments			  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}

\newenvironment{definition}{\begin{defi} \rm }{\end{defi}}
\newenvironment{theorem}{\begin{theo} \rm }{\end{theo}}

\renewenvironment{itemize}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\rec}[1]{\plat{			 	% modal diamond
	\stackrel{\mbox{\tiny $/$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
	\!\!#1\!\!
	\stackrel{\mbox{\tiny $\backslash$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\nobis}{\mbox{$\,\not\hspace{-2.5pt}	% no bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,\,$}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\bibliographystyle{plain}

\vspace*{5pt}
\begin{center}
{\Large \bf Bisimulation}
\\ \ \\
R.J. van Glabbeek\\
\footnotesize
Computer Science Department, Stanford University, CA 94305-9045, USA\\
{\tt http://theory.stanford.edu/\~{}rvg ~~~~~~ rvg@cs.stanford.edu}
\end{center}
\vspace{5pt}

\noindent
Bisimulation equivalence is a semantic equivalence relation on
labelled transition systems, which are used to represent distributed
systems. It identifies systems with the same branching structure.

\subsection*{Labelled Transition Systems}

A labelled transition system consists of a collection of states and
a collection of transitions between them. The transitions are labelled
by actions from a given set $A$ that happen when the transition is
taken, and the states may be labelled by predicates from a given set
$P$ that hold in that state.

\begin{definition}
Let $A$ and $P$ be sets (of {\em actions} and {\em predicates},
respectively).\\  A {\em labelled transition system} (LTS)
over $A$ and $P$ is a triple $(S,\rightarrow, \models)$ with
\begin{itemize}
\item $S$ a class (of {\em states}),
\item $\rightarrow$ a collection of binary relations
$\stackrel{a}{\longrightarrow} \; \subseteq S \times S$---one for every $a \in A$---(the
{\em transitions}),\\ such that for all $s \in S$ the class
$\{t \in S \mid s \stackrel{a}{\longrightarrow} t\}$ is a set,
\item and $\models\; \subseteq S \times P$. $s \models p$ says that
predicate $p \in P$ {\em holds} in state $s \in S$.
\end{itemize}
\end{definition}
LTSs with $A$ a singleton (i.e.\ with $\rightarrow$ a single binary
relation on $S$) are known as {\em Kripke structures}, the models of
modal logic. General LTSs (with $A$ arbitrary) are the Kripke models
for polymodal logic.  The name ``labelled transition system'' is
employed in concurrency theory. There, the elements of $S$ represent
the systems one is interested in, and $s \stackrel{a}{\longrightarrow} t$ means that system
$s$ can evolve into system $t$ while performing the action $a$. This
approach identifies states and systems: the states of a system $s$ are
the systems reachable from $s$ by following the transitions.  In this
realm $P$ is often taken to be empty, or it contains a single
predicate $\surd$ indicating successful termination.

\begin{definition}
A {\em process graph} over $A$ and $P$ is a tuple
$g=(S,I,\rightarrow,\models)$ with $(S,\rightarrow,\models)$ an LTS
over $A$ and $P$ in which $S$ is a  set, and $I \in S$. 
\end{definition}
Process graphs are used in concurrency theory to disambiguate between
states and systems. A process graph $(S,I,\rightarrow,\models)$
represents a single system, with $S$ the set of its states and $I$ its
initial state.  In the context of an LTS $(S,\rightarrow,\models)$ two
concurrent systems are modelled by two members of $S$; in the context
of process graphs, they are two different graphs. The {\em nondeterministic
finite automata} used in {\em automata theory} are process graphs with a
finite set of states over a finite alphabet $A$ and a set $P$
consisting of a single predicate denoting {\em acceptance}.

\subsection*{Bisimulation equivalence}

Bisimulation equivalence is defined on the states of a given LTS, or
between different process graphs.

\begin{definition}
Let $(S,\rightarrow,\models)$ be an LTS over $A$ and $P$.  
A {\em bisimulation} is a binary relation $R \subseteq S \times S$,
satisfying:
\begin{itemize}
\item[$\wedge$] if $sRt$ then $s \models p \Leftrightarrow t \models p$
for all $p \in P$,
\item[$\wedge$] if $sRt$ and $s \stackrel{a}{\longrightarrow} s'$ with $a \in A$, then
there exists a $t'$ with $t \stackrel{a}{\longrightarrow} t'$ and $s'Rt'$,
\item[$\wedge$] if $sRt$ and $t \stackrel{a}{\longrightarrow} t'$ with $a \in A$, then
there exists an $s'$ with $s \stackrel{a}{\longrightarrow} s'$ and $s'Rt'$.
\end{itemize}
Two states $s,t \in S$ are {\em bisimilar}, denoted $s \;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{}\, t$,
if there exists a bisimulation $R$ with $sRt$.
\end{definition}
Bisimilarity turns out to be an equivalence relation on $S$, and is
also called {\em bisimulation equivalence}.

\begin{definition}
Let $g=(S,I,\rightarrow,\models)$ and
$h=(S',I',\rightarrow',\models')$ be
process graphs over $A$ and $P$.  
A {\em bisimulation} between $g$ and $h$ is a binary relation $R
\subseteq S \times S'$, satisfying $I R I'$ and the same three clauses
as above. $g$ and $h$ are {\em bisimilar}, denoted $g \;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{}\, h$,
if there exists a bisimulation between them.
\end{definition}
.PS
scale = 2.54
boxwid = 0.5; boxht = 0.5
circlerad = 0.05
arrowhead = 7

LC1: circle at (-2.5,2)
LC2: circle at last circle +(-1,-1)
LC3: circle at last circle +(0,-1); circle at last circle rad .1
LC4: circle at LC1 +(1,-1)
LC5: circle at last circle +(0,-1); circle at last circle rad .1

LB1: box invis "$a$" at LC1 +(-.65,-.35)
LB2: box invis "$a$" at LC1 +(.65,-.35)
LB3: box invis "$b$" at LC1 +(-1.2,-1.4)
LB5: box invis "$c$" at LC1 +(1.2,-1.4)

arrow from LC1+(0,.6) to LC1 chop circlerad chop circlerad
arrow from LC1 to LC2 chop circlerad chop circlerad
arrow from LC2 to LC3 chop circlerad chop circlerad
arrow from LC1 to LC4 chop circlerad chop circlerad
arrow from LC4 to LC5 chop circlerad chop circlerad

box invis "$\nobis$" at (0,1)

RC1: circle at (2.5,2)
RC2: circle at RC1 +(0,-1)
RC3: circle at RC2 +(-1,-1); circle at last circle rad .1
RC4: circle at RC2 +(1,-1); circle at last circle rad .1

RB1: box invis "$a$" at RC1 +(.2,-.4)
RB2: box invis "$b$" at RC2 +(-.65,-.35)
RB3: box invis "$c$" at RC2 +(.65,-.35)
RB4: box invis at RC2 +(1.2,-1.2)

arrow from RC1+(0,.6) to RC1 chop circlerad chop circlerad
arrow from RC1 to RC2 chop circlerad chop circlerad
arrow from RC2 to RC3 chop circlerad chop circlerad
arrow from RC2 to RC4 chop circlerad chop circlerad
.PE
\centerline{\raise 1em\box\graph}

\noindent
{\bf Example}\,
The two process graphs above (over $A=\{a,b,c\}$ and $P=\{\surd\}$),
in which the initial states are indicated by short incoming arrows
and the final states (the ones labelled with $\surd$) by
double circles, are not bisimulation equivalent, even though in
automata theory they accept the same language. The choice between $b$
and $c$ is made at a different moment (namely before vs.\ after the
$a$-action); i.e.\ the two systems have a different {\em branching
structure}. Bisimulation semantics distinguishes systems that differ
in this manner.

\subsection*{Modal Logic}

(Poly)modal logic is an extension of propositional logic with formulas
$\rec{a}\varphi$, saying that it is possible to follow an
$a$-transition after which the formula $\varphi$ holds. Modal formulas
are interpreted on the states of labelled transition systems.  Two
systems are bisimilar iff they satisfy the same infinitary modal
formulas.

\begin{definition} The language ${\cal L}$ of {\em polymodal logic}
over $A$ and $P$ is given by: 
\begin{itemize}
\item $\top \in {\cal L}$,
\item $p \in {\cal L}$ for all $p \in P$,
\item if $\varphi,\psi \in {\cal L}$ for then $\varphi \wedge \psi \in {\cal L}$,
\item if $\varphi \in {\cal L}$ then $\neg \varphi \in {\cal L}$,
\item if $\varphi \in {\cal L}$ and $a \in A$ then $\rec{a}\varphi \in {\cal L}$.
\end{itemize}
Basic (as opposed to {\em poly-}) modal logic is the special case
where $|A|=1$; there $\rec{a}\varphi$ is simply denoted
$\diamond\varphi$.  The {\em Hennessy-Milner logic} is polymodal logic
with $P=\emptyset$.  The language ${\cal L}^\infty$ of {\em infinitary
polymodal logic} over $A$ and $P$ is obtained from ${\cal L}$ by
additionally allowing $\bigwedge_{i \in I} \varphi_i$ to be in
${\cal L}^\infty$ for arbitrary index sets $I$ and $\varphi_i \in
{\cal L}^\infty$ for $i \in I$. The connectives $\top$ and $\wedge$ are
then the special cases $I=\emptyset$ and $|I|=2$.
\end{definition}

\begin{definition}
Let $(S,\rightarrow,\models)$ be an LTS over $A$ and $P$.
The relation $\models \; \subseteq S \times P$ can
be extended to the {\em satisfaction relation} $\models \; \subseteq S
\times {\cal L}^\infty$, by defining
\begin{itemize}
\item $s \models \bigwedge_{i\in I}\varphi_i$ if $s \models \varphi_i$
      for all $i \in I$---in particular,
      $s \models \top$ for any state $s \in S$,
\item $s \models \neg \varphi$ if $s \not\models \varphi$,
\item $s \models \rec{a}\varphi$ if there is a state $t$ with $s
      \stackrel{a}{\longrightarrow} t$ and $t \models \varphi$.
\end{itemize}
Write ${\cal L}(s)$ for $\{\varphi \in {\cal L} \mid s \models \varphi\}$.
\end{definition}

\begin{theorem}\hspace{-1pt}[5]\hspace{1pt}
Let $(S,\rightarrow,\models)$ be an LTS and $s,t \in S$.
Then  $s \;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{}\, t \Leftrightarrow {\cal L}^\infty(s) = {\cal L}^\infty(t)$.
\end{theorem}
In case the systems $s$ and $t$ are image finite, it suffices to
consider finitary polymodal formulas only [3].
In fact, for this purpose it is enough to
require that one of $s$ and $t$ is image finite.

\begin{definition}
Let $(S,\rightarrow,\models)$ be an LTS\@. A state $t \in S$ is {\em
reachable} from $s \in S$ if there are $s_i \in S$ and $a_i \in A$ for
$i=0,...,n$ with $s=s_0$, $s_{i-1} \stackrel{a_i}{\longrightarrow} s_i$ for $i=1,...,n$,
and $s_n = t$. A state $s\in S$ is {\em image finite} if for every
state $t \in S$ reachable from $s$ and for every $a \in A$, the
set $\{u \in S \mid t \stackrel{a}{\longrightarrow} u\}$ is finite.
\end{definition}

\begin{theorem}\hspace{-2pt}[4]\hspace{1pt}
Let $(S,\rightarrow,\models)$ be an LTS and $s,t \!\in\! S$ with $s$
image finite. Then  $s \;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{}\, t \Leftrightarrow {\cal L}(s) = {\cal L}(t)$.
\end{theorem}

\subsection*{Non-well-founded sets}
Another characterization of bisimulation semantics can be given by
means of {\sc Aczel}'s universe ${\cal V}$ of non-well-founded sets
[1].  This universe is an extension of the Von Neumann
universe of well-founded sets, where the axiom of foundation (every
chain $x_0 \ni x_1 \ni \cdots$ terminates) is replaced by an
{\em anti-foundation axiom}. 

\begin{definition} 
Let $(S,\rightarrow,\models)$ be an LTS, and let ${\cal B}$ denote the
unique function ${\cal M} : S \rightarrow {\cal V}$ satisfying, for
all $s \in S$,
$${\cal M} (s)=\{\rec{a, {\cal M} (t)} \mid s \stackrel{a}{\longrightarrow} t\}.$$
\end{definition}
It follows from Aczel's anti-foundation axiom that such a function
exists.  In fact, the axiom amounts to saying that systems of
equations like the one above have unique solutions.
${\cal B}(s)$ could be taken to be the {\em branching structure} of $s$.
The following theorem then says that two systems are bisimilar iff
they have the same branching structure.

\begin{theorem}\hspace{-1pt}[2]\hspace{1pt}
Let $(S,\rightarrow,\models)$ be an LTS and $s,t \in S$.
Then $s \;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{}\, t ~ \Leftrightarrow ~ {\cal B}(s)={\cal B}(t)$.
\end{theorem}

\subsection*{Abstraction}

In concurrency theory it is often useful to distinguish between {\em
internal actions}, that do not admit interactions with the outside
world, and {\em external} ones. As normally there is no need to
distinguish the internal actions from each other, they all have the
same name, namely $\tau$. If $A$ is the set of external actions a
certain class of systems may perform, then $A_\tau := A
\stackrel{\mbox{\huge .}}{\cup} \{\tau\}$.  Systems in that class are
then represented by labelled transition systems over $A_\tau$ and a
set of predicates $P$. The variant of bisimulation equivalence that
treats $\tau$ just like any action of $A$ is called {\em strong
bisimulation equivalence}. Often, however, one wants to abstract from
internal actions to various degrees. A system doing two $\tau$ actions
in succession is then considered equivalent to a system doing just
one. However, a system that can do either $a$ or $b$ is considered
different from a system that can do either $a$ or first $\tau$ and
then $b$, because if the former system is placed in an environment
where $b$ cannot happen, it can still do $a$ instead, whereas the
latter system may reach a state (by executing the $\tau$ action) in
which $a$ is no longer possible.

Several versions of bisimulation equivalence that formalize these
desiderata occur in the literature. {\em Branching bisimulation
equivalence} [2], like strong bisimulation, faithfully
preserves the branching structure of related systems. The notions of
{\em weak} and {\em delay} bisimulation equivalence, which
were both introduced by Milner under the name {\em observational
equivalence}, make more identifications, motivated by observable
machine-behaviour according to certain testing scenarios.

Write $s \Longrightarrow t$ for $\exists n\!\geq\! 0\!: \exists s_0,...,s_n\!: s\!=\!s_0
\stackrel{\tau}{\longrightarrow} s_1 \stackrel{\tau}{\longrightarrow} \cdots \stackrel{\tau}{\longrightarrow} s_n\! =\! t$, i.e.\ a
(possibly empty) path of $\tau$-steps from $s$ to $t$. Furthermore,
for $a \in A_\tau$, write $\plat{s \stackrel{(a)}{\longrightarrow} t}$ for $s
\stackrel{a}{\longrightarrow} t \vee (a=\tau \wedge s=t)$. Thus $\plat{\stackrel{(a)}{\longrightarrow}}$
is the same as $\stackrel{a}{\longrightarrow}$ for $a \in A$, and $\plat{\stackrel{(\tau)}{\longrightarrow}}$
denotes zero or one $\tau$-steps.

\begin{definition}
Let $(S,\rightarrow,\models)$ be an LTS over $A_\tau$ and $P$.  
Two states $s,t \in S$ are {\em branching bisimulation equivalent},
denoted $s \;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{b}\, t$, if they are related by a binary relation $R
\subseteq S \times S$ (a {\em branching bisimulation}), satisfying:
\begin{itemize}
\item[$\wedge$] if $sRt$ and $s \models p$ with $p \in P$, then
there is a $t_1$ with $t \Longrightarrow t_1 \models p$ and $sRt_1$,
\item[$\wedge$] if $sRt$ and $t \models p$ with $p \in P$, then
there is a $s_1$ with $s \Longrightarrow s_1 \models p$ and $s_1Rt$,
\item[$\wedge$] if $sRt$ and $s \stackrel{a}{\longrightarrow} s'$ with $a \!\in\! A_\tau$, then
there are $t_1,t_2,t'$ with $\plat{t \Longrightarrow t_1 \stackrel{(a)}{\longrightarrow} t_2 = t'}$,
$sRt_1$ and $s'Rt'$,
\item[$\wedge$] if $sRt$ and $t \stackrel{a}{\longrightarrow} t'$ with $a \!\in\! A_\tau$, then
there are $s_1,s_2,s'$ with $\plat{s \!\Longrightarrow\! s_1 \!\stackrel{(a)}{\longrightarrow}\! s_2 = s'}$,
$s_1Rt$ and $s'Rt'$.
\end{itemize}
{\em Delay bisimulation equivalence}, $\;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{d}\,$, is obtained by
dropping the requirements $sRt_1$ and $s_1Rt$.
{\em  Weak bisimulation equivalence} [5], $\;\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{w}\,
$, is
obtained by furthermore relaxing the requirements $t_2 = t'$ and $s_2
= s'$ to $t_2 \Longrightarrow t'$ and $s_2 \Longrightarrow s'$.
\end{definition}
For systems without $\tau$'s all these notions coincide with strong
bisimulation equivalence.

\subsection*{Concurrency}

When applied to {\em parallel systems}, capable of performing
different actions at the same time, the versions of bisimulation
discussed here employ {\em interleaving semantics}: no distinction is
made between true parallelism and its nondeterministic sequential
simulation. Versions of bisimulation that do make such a distinction
have been developed as well, most notably the {\em ST-bisimulation}
[2], that takes temporal overlap of actions into account,
and the {\em history preserving bisimulation} [2] that even
keeps track of causal relations between actions.  For this purpose,
system representations such as {\em Petri nets} or {\em event
structures} are often used instead of labelled transition systems.

\subsection*{References}

\begin{list}{\settowidth\labelwidth{[1]}
             \leftmargin\labelwidth
             \advance\leftmargin\labelsep}{}

\item[{[1]}]
{\sc P.~Aczel} (1988):
\newblock {\em Non-well-founded Sets}, {\sl CSLI Lecture Notes} 14.
\newblock Stanford University.

\item[{[2]}]
{\sc R.J.~van Glabbeek} (1990):
\newblock {\em Comparative Concurrency Semantics and Refinement of Actions}.
\newblock PhD thesis, Free University, Amsterdam.
\newblock Second edition available as CWI tract 109, CWI, Amsterdam 1996.

\item[{[3]}]
{\sc M.~Hennessy \& R.~Milner} (1985):
\newblock {\em Algebraic laws for nondeterminism and concurrency.}
\newblock {\sl Journal of the ACM} 32(1), pp. 137--161.

\item[{[4]}]
{\sc M.J. Hollenberg} (1995):
\newblock {\em {Hennessy-Milner} classes and process algebra.}
\newblock In A.~Ponse, M.~de~Rij\-ke \& Y.~Venema, editors: {\sl Modal Logic and Process Algebra: a Bisimulation Perspective}, {\sl CSLI Lecture Notes} 53, CSLI Publications, Stanford, California, pp. 187--216.

\item[{[5]}]
{\sc R.~Milner} (1990):
\newblock {\em Operational and algebraic semantics of concurrent processes.}
\newblock In J.~van Leeuwen, editor: {\sl Handbook of Theoretical Computer Science}, chapter~19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201--1242.

\end{list}
\end{document}
