\documentclass[letterpaper,11pt]{article}% Fontsize 11 point
\usepackage{hyperref}
\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}
\renewcommand{\thefootnote}{}
\footnotetext{\hspace*{-16pt}Written August 2000 for the
 forgotten {\sl Encyclopedia of Distributed Computing}
 (J.E.~Urban \& P.~Dasgupta, eds.).
  ``Further reading'' added November 2010.
 To appear in the {\sl Encyclopedia of Parallel Computing}
 (D.~Padua, ed.), Springer, 2011.}
\begin{center}
{\Large \bf Bisimulation}
\\ \ \\
R.J. van Glabbeek\\[1ex]
\footnotesize
NICTA, Sydney, Australia.
\\[1ex]
School of Computer Science and Engineering,
The University of New South Wales, Sydney, Australia.
\\[1ex]
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}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
    \special{pn 8}%
    \special{ar 571 217 20 20 0 6.28319}%
    \special{ar 177 610 20 20 0 6.28319}%
    \special{ar 177 1004 20 20 0 6.28319}%
    \special{ar 177 1004 39 39 0 6.28319}%
    \special{ar 965 610 20 20 0 6.28319}%
    \special{ar 965 1004 20 20 0 6.28319}%
    \special{ar 965 1004 39 39 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.354in
    \rlap{\kern 0.315in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.354in
    \rlap{\kern 0.827in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.768in
    \rlap{\kern 0.098in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.768in
    \rlap{\kern 1.043in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{pa 571 0}%
    \special{pa 571 197}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 596 97}%
    \special{pa 571 197}%
    \special{pa 546 97}%
    \special{pa 596 97}%
    \special{fp}%
    \special{pa 557 230}%
    \special{pa 191 596}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 279 543}%
    \special{pa 191 596}%
    \special{pa 244 508}%
    \special{pa 279 543}%
    \special{fp}%
    \special{pa 177 630}%
    \special{pa 177 984}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 202 884}%
    \special{pa 177 984}%
    \special{pa 152 884}%
    \special{pa 202 884}%
    \special{fp}%
    \special{pa 585 230}%
    \special{pa 951 596}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 898 508}%
    \special{pa 951 596}%
    \special{pa 862 543}%
    \special{pa 898 508}%
    \special{fp}%
    \special{pa 965 630}%
    \special{pa 965 984}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 990 884}%
    \special{pa 965 984}%
    \special{pa 940 884}%
    \special{pa 990 884}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.610in
    \rlap{\kern 1.555in\lower\graphtemp\hbox to 0pt{\hss $\nobis$\hss}}%
    \special{ar 2539 217 20 20 0 6.28319}%
    \special{ar 2539 610 20 20 0 6.28319}%
    \special{ar 2146 1004 20 20 0 6.28319}%
    \special{ar 2146 1004 39 39 0 6.28319}%
    \special{ar 2933 1004 20 20 0 6.28319}%
    \special{ar 2933 1004 39 39 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.374in
    \rlap{\kern 2.618in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.748in
    \rlap{\kern 2.283in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.748in
    \rlap{\kern 2.795in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{pa 2539 0}%
    \special{pa 2539 197}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2564 97}%
    \special{pa 2539 197}%
    \special{pa 2514 97}%
    \special{pa 2564 97}%
    \special{fp}%
    \special{pa 2539 236}%
    \special{pa 2539 591}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2564 491}%
    \special{pa 2539 591}%
    \special{pa 2514 491}%
    \special{pa 2564 491}%
    \special{fp}%
    \special{pa 2525 624}%
    \special{pa 2160 990}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2248 937}%
    \special{pa 2160 990}%
    \special{pa 2213 902}%
    \special{pa 2248 937}%
    \special{fp}%
    \special{pa 2553 624}%
    \special{pa 2919 990}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2866 902}%
    \special{pa 2919 990}%
    \special{pa 2831 937}%
    \special{pa 2866 902}%
    \special{fp}%
    \hbox{\vrule depth1.181in width0pt height 0pt}%
    \kern 3.110in
  }%
}%
\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-behavior 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}
These definition stem from concurrency theory. On Kripke structures,
when studying modal or temporal logics, normally a stronger version of
the first two conditions is imposed:
\begin{itemize}
\item[$\wedge$] if $sRt$ and $p \in P$, then
 $s \models p \Leftrightarrow t \models p$.
\end{itemize}
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}

\subsection*{Further reading}

Gentle introductions to bisimulation semantics, with many examples of
applications, can be found in the textbooks:

\begin{list}{\settowidth\labelwidth{[1]}
             \leftmargin\labelwidth
             \advance\leftmargin\labelsep}{}
\item[$-$]
{\sc J.C.M. Baeten \& W.P. Weijland} (1990):
{\em Process Algebra}, Cambridge University Press.

\item[$-$]
{\sc R. Milner} (1989):
{\em Communication and Concurrency}, Prentice Hall.
\end{list}
An historical perspective on bisimulation appears in
\begin{list}{\settowidth\labelwidth{[1]}
             \leftmargin\labelwidth
             \advance\leftmargin\labelsep}{}
\item[$-$]
{\sc D. Sangiorgi} (2009):
{\em On the origins of bisimulation and coinduction},
{\sl ACM Transactions on Programming Languages and Systems} 31(4).
\end{list}

\end{document}
