\documentclass[runningheads]{llncs}
\bibliographystyle{alpha}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                            References                                %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Prop.~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Cor.~\ref{cor-#1}}
\newcommand{\df}[1]{Def.~\ref{df-#1}}
\newcommand{\fig}[1]{Fig.~\ref{fig-#1}}
\newcommand{\sect}[1]{Sect.~\ref{sec-#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			        New Commands				  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}}	% disjoint union
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox	% openface character
	[0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\IG}{\dc{G}}				% graphs
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\goto}[2]{\stackrel{#1}{\longrightarrow}_{#2}}% transition
\newcommand{\gonotto}[2]{\hspace{4pt}\not\hspace{-4pt}	% no transition
	\stackrel{#1\ }{\longrightarrow}_{#2}}
\newcommand{\dto}[2]{\,{\stackrel{#1}{\raisebox{0pt}	% abstract
	[3pt][0pt]{$\scriptstyle=\!\Longrightarrow$}}_{#2}}\,}%	transition
\newcommand{\opt}[1]{\mbox{\tiny(}#1\mbox{\tiny)}}      % optional action
\newcommand{\bis}[1]{\mbox{}\;				% bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\bisc}[1]{\mbox{}\;				% bisimulation congr.
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}^c\,}
\newcommand{\bisfc}[1]{\mbox{}\;		% FAP bisimulation congr.
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}^{\it fc}\,}
\newcommand{\nobis}[1]{\;\mbox{$\,\not\hspace{-2.5pt}	% no bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,$}\,}
\newcommand{\nd}{\mbox{\sc nodes}}
\newcommand{\ed}{\mbox{\sc edges}}
\newcommand{\rt}{\mbox{\sc root}}
\newcommand{\leftmerge}{\|\hspace{-1.06ex}\raisebox{-1.17ex}{$-$}}% left merge

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{A Characterisation of\\ Weak Bisimulation Congruence}
\author{Rob van Glabbeek}
\authorrunning{R.J. van Glabbeek}
\institute{National ICT Australia\\
and School of Computer Science and Engineering\\
The University of New South Wales\\
\email{rvg@cs.stanford.edu}}
\begin{document}
\maketitle

\begin{abstract}
This paper shows that weak bisimulation congruence can be
characterised as rooted weak bisimulation equivalence, even without
making assumptions on the cardinality of the sets of states or actions
of the processes under consideration.
\end{abstract}

\section*{Introduction}

Weak bisimulation equivalence, also known as observation equivalence
\cite{Mi90b}, is a fundamental semantic equivalence used in system
verification, and one of the first proposed in the literature.
It upgrades strong bisimulation equivalence by featuring abstraction
from internal actions.

In order to allow compositional system verification, semantic
equivalence relations need to be \emph{congruences} for the operators
under consideration, meaning that the equivalence class of an $n$-ary
operator $f$ applied to arguments $p_1,\ldots,p_n$ is completely
determined by the equivalence classes of these arguments.  Although
strong bisimulation equivalence is a congruence for the operators of
CCS, ACP$_\tau$ and many other languages found in the literature, weak
bisimulation equivalence fails to be a congruence for the
\emph{choice} or \emph{alternative composition} operator $+$ of CCS,
as well as for the left-merge \plat{\leftmerge} of ACP$_\tau$.  To
bypass this problem, one uses the coarsest congruence relation for $+$
that is finer than weak bisimulation equivalence, called \emph{weak
bisimulation congruence}, and characterised as \emph{rooted weak
bisimulation equivalence} in \cite{BK85}. This equivalence turns out
to be a minor variant of weak bisimulation equivalence, and a
congruence for all of CCS, ACP$_\tau$ and many other languages.

Classical proof sketches arguing that rooted weak bisimulation
equivalence is indeed weak bisimulation congruence typically make
some cardinally assumptions, such as that there is an infinite
alphabet of actions of which each process uses only a finite subset.
The current contribution establishes the validity of this
characterisation without making such assumptions.
It also argues that the \emph{root condition} that turns weak
bisimulation into rooted weak bisimulation embodies two properties,
one of which is needed to obtain a congruence for the +, and
one to obtain a congruence for the left-merge.

\section{Process Graphs}\label{sec-process graphs}

\begin{definition}[\cite{BK86a}]\rm\label{df-process graph} A
\emph{process graph} over an alphabet of actions $Act$ is a rooted,
directed graph whose edges are labelled by elements of $Act$.
Formally, a process graph $g$ is a triple $(\nd(g), \rt(g), \ed(g))$,
where
\begin{itemize}
\item
$\nd (g)$ is a set, of which the elements are called the \emph{nodes}
or \emph{states} of $g$,
\item
$\rt (g) \in \nd (g)$ is a special node: the \emph{root} or \emph{initial
state} of $g$,
\item
and $\ed (g) \subseteq \nd (g) \times Act \times \nd (g)$ is a set of triples
$(s,a,t)$ with $s,t \in \nd (g)$ and $a \in Act$: the \emph{edges} or
\emph{transitions} of $g$.
\end{itemize}
\end{definition}
Normally, one is not interested in the names of the nodes in a process
graph. For this reason, process graphs are considered {up to isomorphism}.

\begin{definition}\rm\label{df-isomorphism}
Let $g$ and $h$ be process graphs. A \emph{graph isomorphism} between
$g$ and $h$ is a bijective function $f: \nd (g) \rightarrow \nd (h)$
satisfying
\begin{itemize}
\item
$f( \rt (g))= \rt (h)$ and
\item
$(s,a,t) \in \ed (g) ~ \Leftrightarrow ~ (f(s),a,f(t)) \in \ed (h)$.
\end{itemize}
Graphs $g$ and $h$ are \emph{isomorphic}, notation $g \cong h$, if there
exists a graph isomorphism between them.
\end{definition}
If $g\cong h$ then $g$ and $h$ differ only in the identity of their
nodes.  Graph isomorphism is an equivalence relation on the class of
process graphs.

Further on, process graphs are pictured by using open dots ($\circ$)
to denote nodes, and labelled arrows to denote edges.  The root is
represented by an incoming arrow, not originating from another node.
These drawings present process graphs only up to isomorphism.

Let $\IG(Act)$ be the class of process graphs over the alphabet of
actions $Act$ \emph{up to isomorphism}. This means that I am satisfied
with a level of precision in describing elements of $\IG(Act)$ that
fails to distinguish isomorphic process graphs.  In the digression
below I will indicate how to raise the precision of my definitions to
a fully formal level; the digression should also make clear that it is
not really worthwhile to maintain this level throughout the paper.

Next I define the most basic process algebraic operations on
$\IG(Act)$: a constant 0 for \emph{inaction}, a binary infix written
operator + for \emph{alternative composition} or \emph{choice}, and
unary operators $a.$ for \emph{action prefixing} for each $a\in Act$.
For the sake of convenience, in the definition below I will only
consider \emph{root-acyclic} process graphs. In \sect{unwinding} I
will extend the definition to arbitrary process graphs.

\begin{definition}[\cite{BK86a}]\rm\label{df-operators}
A process graph is \emph{root-acyclic} if it has no incoming edges at
the root.  Let $\IG^\rho(Act)$ be the class of root-acyclic process
graphs over $Act$ up to isomorphism.  The constant 0 and the operators
$a.$ and $+_\rho$ are defined on $\IG^\rho(Act)$ as follows. (The
subscript $\rho$ serves to distinguish this alternative composition
from the more general one that will be defined in \sect{unwinding}.)
\begin{itemize}
\item 0 is interpreted as the trivial graph, having one node (the
      root) and no edges;
\item $a.g$ is obtained from $g$ by adding a new node, which will be
the root of $a.g$, and a new $a$-labelled edge from the root of $a.g$
to the root of $g$;
\item $g+_\rho h$ is obtained by identifying the root nodes of disjoint
copies of $g$ and $h$.
\end{itemize}
\end{definition}

\subsection*{Digression: Distinguishing Isomorphic Process Graphs}
In \df{operators} I have not bothered to tell which node exactly will
be the only node of the process graph 0 and which new node will be
added in the construction of $a.g$. Moreover, in taking the disjoint
union of $g$ and $h$, no explicit solution is offered for what to do
when $g$ and $h$ have nodes in common. Here I provide two possible
answers. As it doesn't matter at all which one is chosen, the reader
may pick himself, or make up a third.

\paragraph{Making arbitrary choices to resolve ambiguity.}~\\[5pt]
The definitions of $0$ and $a.g$ could for instance be given as
follows:
\begin{itemize}
\item $\nd(0)=\{*\}$,
\item $\rt(0)=*$,
\item $\ed(0)=\emptyset$.
\end{itemize}
\begin{itemize}
\item $\nd(a.g)=\{*\}\cup\{s'\mid s\in\nd(g)\}$,
\item $\rt(a.g)=*$,
\item $\ed(a.g)=\{(*,a,\rt(g)')\}\cup \{(s',a,t')\mid(s,a,t)\in\ed(g)\}$.
\end{itemize}
Here the nodes of $g$ are renamed from $s$ into $s'$, so as to make
sure that none of them happens to be the symbol $*$ that is used to
name the new root node.

\paragraph{Working modulo isomorphism.}~\\[5pt]
In this approach $\IG(Act)$ is the class of process graph
\emph{modulo isomorphism}, meaning that the elements of $\IG(Act)$
are isomorphism classes of process graphs.

Now $0\in\IG^\rho(Act)$ is defined as the isomorphism class of all
trivial process graphs, after observing that all trivial graphs are
isomorphic. To obtain the isomorphism class $a.G$, for $G$ an
isomorphism class of process graphs, I first pick a representative
$g\!\in\!G$ and a fresh object $r \not\in\nd(g)$. Then $a.g$ is
defined by
\begin{itemize}
\item $\nd(a.g)=\nd(g)\cup\{r\}$,
\item $\rt(a.g)=r$ and
\item $\ed(a.g)=\ed(g)\cup\{(r,a,\rt(g))\}$.
\end{itemize}
Finally, $a.G$ is defined to be the isomorphism class containing
$a.g$, and the exercise is concluded by showing that the result is
independent of the choice of $g\!\in\!G$.  Likewise, $G+_\rho H$, for
$G,H\in \IG^\rho(Act)$, is obtained as the isomorphism class of $g+_\rho h$, where
$g\in G$ and $h\in H$ are chosen in such a way that $\nd(g)\cap \nd(h)
=\rt(g)=\rt(h)$, and $g+_\rho h$ is defined by
\begin{itemize}
\item $\nd(g+_\rho h)=\nd(g)\cup\nd(h)$,
\item $\rt(g+_\rho h)=\rt(g)=\rt(h)$ and
\item $\ed(g+_\rho h)=\ed(g)\cup\ed(h)$.
\end{itemize}
Again, it must be shown that the result is independent of the
choice of $g$ and $h$.

\section{Bisimulation Semantics}\label{sec-bisimulation}

To make process graphs into a useful semantic model of calculi that
enable system verification, a semantic equivalence coarser than
isomorphism needs to be defined. The most popular choices are strong
and weak bisimulation equivalence, and some of their variants.
Such an equivalence can be used fruitfully when it is a
\emph{congruence} for the process algebraic operators that are
considered in a particular application. These almost always include
the operators 0, $a.$ and +. A semantic equivalence $\sim$ is a
congruence for these operators if $g\sim h$ implies 
$a.g \sim a.h$ and $g_1\sim h_1 \wedge g_2\sim h_2$ implies
$g_1+g_2 \sim h_1+h_2$.

\subsection{Strong Bisimulation}

\begin{definition}\rm\label{df-bisimulation}
Let $g,h \in \IG(Act)$.  The graphs $g$ and $h$ are \emph{(strong)
bisimulation equivalent}, notation $g\bis{}h$, if there exists a
binary relation $R \subseteq \nd (g) \times \nd (h)$, called a
\emph{bisimulation} between $g$ and $h$, satisfying, for all
$a\!\in\!Act$:
\begin{itemize}
\item
$\rt (g) ~R~ \rt (h)$.
\item
If $sRt$ and $(s,a,s') \in \ed (g)$, then $\exists(t,a,t') \in \ed (h)$ such that $s'Rt'$.
\item
If $sRt$ and $(t,a,t') \in \ed (h)$, then $\exists(s,a,s') \in \ed (g)$ such that $s'Rt'$.
\end{itemize}
\end{definition}
It is well-known and easy to check that $\bis{}$ is an equivalence
relation indeed.
I will now show that it is a congruence relation for $a.$ and $+_\rho $.
Because these operators have so-far not been defined outside $\IG^\rho(Act)$,
for now this result will pertain to root-acyclic process graphs only.

\begin{definition}\rm\label{df-rooted}
A relation between the nodes of two root-acyclic process graphs is
called \emph{rooted} if it relates root nodes with root nodes only.
\end{definition}

\begin{lemma}\label{lem-rooted}
Let $g,h \in \IG^\rho(Act)$. If $g\bis{}h$ then there exist a rooted
bisimulation between $g$ and $h$.
\end{lemma}

\begin{proof}
Let $R$ be a bisimulation between $g$ and $h$. A rooted bisimulation
is obtained from $R$ by omitting all liaisons between root nodes and
non-root nodes.
\end{proof}

\begin{proposition}\label{pr-strong congruence}
On $\IG^\rho(Act)$, bisimulation equivalence is a congruence for $a.$ and $+_\rho $.
\end{proposition}

\begin{proof}
Suppose $R$ is a bisimulation between $g$ and $h$.  Then $$R \cup
\{(\rt(a.g),\rt(a.h))\}$$ is a bisimulation between $a.g$ and $a.h$.
Moreover, invoking \lem{rooted}, let $R_i$ be a rooted bisimulation
between $g_i$ and $h_i$ for $g_i,h_i\in\IG^\rho(Act)$ and $i=1,2$ then
$R_1\cup R_2$ is a bisimulation between $g_1+_\rho g_2$ and $h_1+_\rho h_2$.\qed
\end{proof}

\subsection{Weak Bisimulation}

Let $\tau\in Act$ be the \emph{invisible action} or \emph{silent
step}. Henceforth, write $s\goto{a}{g} s'$ for $(s,a,s') \in \ed (g)$
and $s\dto{}{g} s'$ when there are $s_0,\ldots,s_n$ in $\nd(g)$ such
that \plat{s=s_0 \goto{\tau}{g} s_1 \goto{\tau}{g} \cdots\goto{\tau}{g}s_n=s'}.
Moreover, $s\dto{a}{g} s'$ denotes that there are nodes $s_1$ and
$s_2$ in $g$ such that \plat{s \dto{}{g} s_1 \goto{a}{g} s_2 \dto{}{g} s'}
and \plat{s\dto{\opt{a}}{g} s'} is a shorthand for $s\dto{}{g} s'$ when
$a=\tau$, and $s\dto{a}{g}s'$ when $a\neq\tau$.
Thus, $s\dto{\opt{\tau}}{g} s'$ says that in $g$ one can travel from
$s$ to $s'$ by performing a sequence of zero or more $\tau$-steps,
whereas $s\dto{\tau}{g} s'$ requires at least one $\tau$-step.
For $a\neq\tau$ there is no difference between \plat{\dto{\opt{a}}{g}} and
$\dto{a}{g}$.

\begin{definition}\rm\label{df-weak bisimulation}
Let $g,h \in \IG(Act)$.
The graphs $g$ and $h$ are \emph{weak bisimulation equivalent}, notation
$g\bis{w}h$, if there exists a binary relation $R \subseteq \nd (g)
\times \nd (h)$, called a \emph{weak bisimulation} between $g$ and $h$,
satisfying, for all $a\!\in\!Act$:
\begin{itemize}
\item
$\rt (g) ~R~ \rt (h)$.
\item
If $sRt$ and \plat{s\goto{a}{g} s'}, then there is a $t'$ such that
\plat{t\dto{\opt{a}}{h}t'} and $s'Rt'$.
\item
If $sRt$ and \plat{t\goto{a}{g} t'}, then there is an $s'$ such that
\plat{s\dto{\opt{a}}{h}s'} and $s'Rt'$.
\end{itemize}
\end{definition}
It is well-known and easy to check that $\bis{w}$ is an equivalence
relation indeed. However, $\bis{w}$ fails to be a congruence for the $+$.
Namely, $\tau.a.0\bis{w}a.0$ but $\tau.a.0+_\rho b.0 \nobis{w} a.0+_\rho b.0$.
The proof of \pr{strong congruence} does not generalise to $\bis{w}$
because \lem{rooted} does not hold for $\bis{w}$: there is no rooted
weak bisimulation between $\tau.a.0$ and $a.0$.

\subsection{Rooted Weak Bisimulation}

Although weak bisimulation equivalence captures the invisible nature
of the silent step rather well, in order to obtain a congruence, a
finer equivalence relation is needed. Such an equivalence was proposed
by Bergstra \& Klop in \cite{BK85}. In fact it is the obvious ``fix''
in the definition of weak bisimulation equivalence needed to inherit
the proof of \pr{strong congruence}.

\begin{definition}[\cite{BK85}]\rm\label{df-rwb}
Two graphs $g,h \in \IG^\rho(Act)$ are \emph{rooted weak bisimulation
  equivalent}, notation $g\bis{rw}h$, if there exists a rooted weak
bisimulation between them (recall \df{rooted}).
\end{definition}
Again, it is easy to check that $\bis{rw}$ is an equivalence
relation. By definition it is finer than $\bis{w}$.  It is strictly
finer because $\tau.0 \bis{w} 0$ but $\tau.0 \nobis{rw} 0$ (and
likewise $\tau.a.0 \bis{w} a.0$ but $\tau.a.0 \nobis{rw} a.0$).
Moreover, \lem{rooted} implies that $\bis{rw}$ is coarser than
$\bis{}$.  It is strictly coarser because $\tau.\tau.0 \bis{rw}
\tau.0$ but $\tau.\tau.0 \nobis{} \tau.0$.

\begin{proposition}\label{pr-rwb}
On $\IG^\rho(Act)$, rooted weak bisimulation equivalence is a congruence
for $a.$ and $+_\rho $.
\end{proposition}

\begin{proof}
Suppose $R$ is a rooted weak bisimulation between $g$ and $h$.  Then
$$R \cup \{(\rt(a.g),\rt(a.h))\}$$ is a rooted weak bisimulation
between $a.g$ and $a.h$.  Moreover, let $R_i$ be a rooted weak
bisimulation between $g_i$ and $h_i$ for $g_i,h_i\in\IG^\rho(Act)$ and
$i=1,2$ then $R_1\cup R_2$ is a rooted weak bisimulation between
$g_1+_\rho g_2$ and $h_1+_\rho h_2$.\qed
\end{proof}

\section{Root Unwinding}\label{sec-unwinding}

In this section I will generalise the definitions and results of
Sections~\ref{sec-process graphs} and~\ref{sec-bisimulation} from
root-acyclic to general process graphs.

\subsection{The Definition of Alternative Composition}

The definition of 0 and $a.$ on $\IG(Act)$ is exactly as on
$\IG^\rho(Act)$ (see \df{operators}). However, defining the + on
$\IG(Act)$ as in \df{operators} would yield counterintuitive results.
Namely we would have $g+h=m$, as in the top row of \fig{plus}.
However, $m$ is able to first do a number of $a$-actions from $g$ and
then a $b$ from $h$; this is inconsistent with the idea that $g+h$
should from the initial state onwards behave either as $g$ or as $h$.
In fact, strong bisimulation equivalence would fail to be a congruence
for this definition of $+$, for $g \bis{} g^\rho$, yet $m \nobis{} k$.

\begin{figure}[htp]
\mbox{}\vspace{-1em}

%\input{plus}
\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 375 197 20 20 0 6.28319}%
    \special{pa 296 220}%
    \special{pa 355 197}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 253 211}%
    \special{pa 355 197}%
    \special{pa 272 257}%
    \special{pa 253 211}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.669in
    \rlap{\kern 0.375in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 375 394 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 375 197 20 20 0 6.28319}%
    \special{pa 375 0}%
    \special{pa 375 177}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 400 77}%
    \special{pa 375 177}%
    \special{pa 350 77}%
    \special{pa 400 77}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.197in
    \rlap{\kern 0.060in\lower\graphtemp\hbox to 0pt{\hss $g$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.394in
    \rlap{\kern 1.162in\lower\graphtemp\hbox to 0pt{\hss +\hss}}%
    \special{ar 1753 394 20 20 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.197in
    \rlap{\kern 1.595in\lower\graphtemp\hbox to 0pt{\hss $h$\hss}}%
    \special{pa 1753 197}%
    \special{pa 1753 374}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1778 274}%
    \special{pa 1753 374}%
    \special{pa 1728 274}%
    \special{pa 1778 274}%
    \special{fp}%
    \special{ar 2147 394 20 20 0 6.28319}%
    \special{pa 1773 394}%
    \special{pa 2127 394}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2027 369}%
    \special{pa 2127 394}%
    \special{pa 2027 419}%
    \special{pa 2027 369}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.394in
    \rlap{\kern 1.950in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.394in
    \rlap{\kern 2.737in\lower\graphtemp\hbox to 0pt{\hss $\neq$\hss}}%
    \special{ar 3525 197 20 20 0 6.28319}%
    \special{pa 3446 220}%
    \special{pa 3505 197}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3403 211}%
    \special{pa 3505 197}%
    \special{pa 3421 257}%
    \special{pa 3403 211}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.669in
    \rlap{\kern 3.525in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 3525 394 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 3525 197 20 20 0 6.28319}%
    \special{pa 3525 0}%
    \special{pa 3525 177}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3550 77}%
    \special{pa 3525 177}%
    \special{pa 3500 77}%
    \special{pa 3550 77}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.197in
    \rlap{\kern 3.210in\lower\graphtemp\hbox to 0pt{\hss $m$\hss}}%
    \special{ar 3918 197 20 20 0 6.28319}%
    \special{pa 3544 197}%
    \special{pa 3899 197}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3799 172}%
    \special{pa 3899 197}%
    \special{pa 3799 222}%
    \special{pa 3799 172}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.197in
    \rlap{\kern 3.721in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{ar 375 1575 20 20 0 6.28319}%
    \special{pa 296 1598}%
    \special{pa 355 1575}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 253 1589}%
    \special{pa 355 1575}%
    \special{pa 272 1635}%
    \special{pa 253 1589}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.047in
    \rlap{\kern 0.375in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 375 1772 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 375 1575 20 20 0 6.28319}%
    \special{ar 375 1181 20 20 0 6.28319}%
    \special{pa 375 1201}%
    \special{pa 375 1555}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 400 1455}%
    \special{pa 375 1555}%
    \special{pa 350 1455}%
    \special{pa 400 1455}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.378in
    \rlap{\kern 0.375in\lower\graphtemp\hbox to 0pt{\hss $a$~~~\hss}}%
    \special{pa 375 984}%
    \special{pa 375 1161}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 400 1061}%
    \special{pa 375 1161}%
    \special{pa 350 1061}%
    \special{pa 400 1061}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.181in
    \rlap{\kern 0.060in\lower\graphtemp\hbox to 0pt{\hss $g^\rho$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.378in
    \rlap{\kern 1.162in\lower\graphtemp\hbox to 0pt{\hss +\hss}}%
    \special{ar 1753 1378 20 20 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.181in
    \rlap{\kern 1.595in\lower\graphtemp\hbox to 0pt{\hss $h$\hss}}%
    \special{pa 1753 1181}%
    \special{pa 1753 1358}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1778 1258}%
    \special{pa 1753 1358}%
    \special{pa 1728 1258}%
    \special{pa 1778 1258}%
    \special{fp}%
    \special{ar 2147 1378 20 20 0 6.28319}%
    \special{pa 1773 1378}%
    \special{pa 2127 1378}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2027 1353}%
    \special{pa 2127 1378}%
    \special{pa 2027 1403}%
    \special{pa 2027 1353}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.378in
    \rlap{\kern 1.950in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.378in
    \rlap{\kern 2.737in\lower\graphtemp\hbox to 0pt{\hss =\hss}}%
    \special{ar 3525 1575 20 20 0 6.28319}%
    \special{pa 3446 1598}%
    \special{pa 3505 1575}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3403 1589}%
    \special{pa 3505 1575}%
    \special{pa 3421 1635}%
    \special{pa 3403 1589}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 2.047in
    \rlap{\kern 3.525in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 3525 1772 197 197 0 6.28319}%
    \special{sh 0.000}%
    \special{ar 3525 1575 20 20 0 6.28319}%
    \special{ar 3525 1181 20 20 0 6.28319}%
    \special{pa 3525 1201}%
    \special{pa 3525 1555}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3550 1455}%
    \special{pa 3525 1555}%
    \special{pa 3500 1455}%
    \special{pa 3550 1455}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.378in
    \rlap{\kern 3.525in\lower\graphtemp\hbox to 0pt{\hss $a$~~~\hss}}%
    \special{pa 3525 984}%
    \special{pa 3525 1161}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3550 1061}%
    \special{pa 3525 1161}%
    \special{pa 3500 1061}%
    \special{pa 3550 1061}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.181in
    \rlap{\kern 3.210in\lower\graphtemp\hbox to 0pt{\hss $k$\hss}}%
    \special{ar 3918 1181 20 20 0 6.28319}%
    \special{pa 3544 1181}%
    \special{pa 3899 1181}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3799 1156}%
    \special{pa 3899 1181}%
    \special{pa 3799 1206}%
    \special{pa 3799 1156}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.181in
    \rlap{\kern 3.721in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \hbox{\vrule depth2.297in width0pt height 0pt}%
    \kern 3.938in
  }%
}%
\centerline{\raise 1em\box\graph}
\vspace{-1em}
\caption{Alternative composition of process graphs}
\label{fig-plus}
\end{figure}

\noindent
For most applications we are interested in process graphs only up to
strong bisimulation equivalence. Up to strong bisimilarity, the
definition of the + on $\IG(Act)$ is completely determined by its
definition on $\IG^\rho(Act)$, because every process graph is strongly
bisimilar with a root-acyclic process graph. The following
construction is used to establish this.

\begin{definition}[\cite{BK86a}]\rm\label{df-unwinding}
\emph{Root unwinding} is the operator $\rho$ on $\IG(Act)$ given by
\begin{itemize}
\item $\nd(\rho(g))=\nd(g)\dcup\{*\}$,
\item $\rt(\rho(g))=\{*\}$ and
\item $\ed(\rho(g))=\ed(g)\cup\{(*,a,s)\mid(\rt(g),a,s)\in\ed(g)\}$.
\end{itemize}
\end{definition}
Note that $\rho(g)\in\IG^\rho(Act)$ for all $g\in\IG(Act)$.

\begin{proposition}[\cite{BK86a}]\label{pr-unwinding}
$g \bis{} \rho(g)$ for every process graph $g\in\IG(Act)$.
\end{proposition}
\begin{proof}
The relation $\{(s,s)\mid s\in\nd(g)\} \cup \{(\rt(g),*)\}$ is a
  bisimulation between $g$ and $\rho(g)$.\qed
\pagebreak[2]
\end{proof}

\begin{definition}[\cite{BK86a}]\rm\label{df-plus}
The definition of the + is extended from $\IG^\rho(Act)$ to
$\IG(Act)$ by $g+h := \rho(g)+_\rho \rho(h)$, where $+_\rho$ is given by
\df{operators}.
\end{definition}
This construction automatically entails that $\bis{}$ is a congruence
for the +.

\begin{proposition}
On $\IG(Act)$, $\bis{}$ is a congruence for $a.$ and $+$.
\end{proposition}

\begin{proof}
The case of $a.$ goes exactly as in \pr{strong congruence}.
Let $g \bis{} g'$ and $h \bis{} h'$.\\
Then $\rho(g) \bis{} g \bis{} g' \bis{} \rho(g')$ and likewise
$\rho(h) \bis{} \rho(h')$.\\ Hence $g+h = \rho(g)+_\rho\rho(h) \bis{}
\rho(g')+_\rho\rho(h') = g'+h'$ by \pr{strong congruence}.\qed
\end{proof}
On $\IG^\rho(Act)$ it is in general not the case that $g+h \cong
g+_\rho h$. However, up to strong bisimilarity, both versions of the + agree.

\begin{proposition}
Let $g,h\in\IG^\rho(Act)$. Then $g+h \bis{} g+_\rho h$.
\end{proposition}

\begin{proof}
$g+h = \rho(g)+_\rho\rho(h) \bis{} g+_\rho h$, using
  Propositions~\ref{pr-unwinding} and~\ref{pr-strong congruence}.\qed
\end{proof}
It is also possible to merge the definitions of $+$, $+_\rho$ and root
unwinding:

\begin{definition}\rm
Let $g,h\in\IG^\rho(Act)$. Then $g+h$ can alternatively be defined by
\begin{itemize}
\item $\nd(g+h)=\nd(g)\dcup\nd(h)\dcup\{*\}$,
\item $\rt(g+h)=\{*\}$ and
\item $\ed(g+h)=\ed(g)\cup\ed(h)\cup\\\{(*,a,s)\mid(\rt(g),a,s)\in\nd(g)
      \vee (\rt(h),a,s)\in\nd(h)\}$.
\end{itemize}
\end{definition}
It is trivial to check that up to isomorphism this definition yields
the same alternative composition operator as \df{plus}.

\subsection{Rooted Weak Bisimulation}

Postulating that rooted weak bisimulation has to be a coarser
equivalence than strong bisimulation, \pr{unwinding} implies that
there is a unique extension of $\bis{rw}$ from $\IG^\rho(Act)$ to $\IG(Act)$.

\begin{definition}\rm\label{df-rwbG}
Let $g,h\in\IG(Act)$. Then $g\bis{rw}h$ iff
$\rho(g)\bis{rw}\rho(h)$ as per \df{rwb}.
\end{definition}

\begin{proposition}\label{pr-rw congruence}
On $\IG(Act)$, $\bis{rw}$ is a congruence for $a.$ and $+$.
\end{proposition}

\begin{proof}
The case of $a.$ goes exactly as in \pr{rwb}.
Let $g \bis{rw} g'$ and $h \bis{rw} h'$.\\
Then $\rho(g) \bis{} g \bis{rw} g' \bis{} \rho(g')$, so $\rho(g)
\bis{rw} \rho(g')$, and likewise $\rho(h) \bis{rw} \rho(h')$.\\
Hence $g+h = \rho(g)+_\rho\rho(h) \bis{rw}
\rho(g')+_\rho\rho(h') = g'+h'$ by \pr{rwb}.\qed
\end{proof}
The following characterisation of rooted weak bisimulation equivalence
was taken as definition in \cite{Mi90b}. Let, for $g\in\IG(Act)$ and
$s\in\nd(g)$, $g_s$ denote the process graph obtained from $g$ by
appointing $s$ as its root.
\pagebreak[2]

\begin{proposition}\label{pr-Milner}
Let $g,h\in\IG(Act)$. Then $g\bis{rw}h$ iff
\begin{itemize}
\item if $\rt(g) \goto{a}{g} s$ then there is a $t$ such that
  $\rt(h)\dto{a}{h}t$ and $g_s\bis{w}h_t$;
\item if $\rt(h) \goto{a}{h} t$ then there is an $s$ such that
  $\rt(g)\dto{a}{g}s$ and $g_s\bis{w}h_t$.
\end{itemize}
\end{proposition}

\begin{proof}
``If'': Let $B=\{(s,t) \in \nd(g)\times\nd(h) \mid g_s \bis{w} h_t\}$
and $$B^\rho=B\dcup\{(\rt(\rho(g)),\rt(\rho(h)))\}
\subseteq\nd(\rho(g))\times\nd(\rho(h)),$$ recalling that
$\nd(\rho(g))=\nd(g)\dcup\{\rt(\rho(g))\}$, and likewise for $\rho(h)$.
Assume that both clause above hold.  It suffices to show that $B^\rho$
is a rooted weak bisimulation between $\rho(g)$ and $\rho(h)$, for by
\df{rwbG} this implies $g\bis{rw}h$. The relation $B^\rho$ is rooted
by construction. So I need to show it is a weak bisimulation.

Let $sB^\rho t$ and $s\goto{a}{\rho(g)}s'$. It suffices to show that
there is a $t'$ such that \plat{t\dto{\opt{a}}{\rho(h)}t'} and
$s'B^\rho t'$.  The other requirement then follows by symmetry.

First assume $sBt$.  In that case, $s\goto{a}{g}s'$ and $g_s \bis{w}
h_t$, so there is a weak bisimulation $R$ between $g_s$ and
$h_s$. Thus $sRt$, and there must be a $t'$ such that
$t\dto{\opt{a}}{h}t'$ and $s'Rt'$. Hence $g_{s'} \bis{w} h_{t'}$,
$s'Bt'$ and $s'B^\rho t'$.
\df{unwinding} yields \plat{t\dto{\opt{a}}{\rho(h)}t'}.

Now assume $s=\rt(\rho(g))$ and $t=\rt(\rho(h))$, so
$\rt(\rho(g))\goto{a}{\rho(g)}s'$. Then, by \df{unwinding},
\plat{\rt(g)\goto{a}{g}s'}, so by the first clause of \pr{Milner} there is
a $t'$ such that $\rt(h)\dto{a}{h}t'$ and $g_{s'}\bis{w}h_{t'}$.
Hence $s'Bt'$ and $s'B^\rho t'$.
\df{unwinding} yields \plat{\rt(\rho(h))\dto{a}{\rho(h)}t'},
hence \plat{t=\rt(\rho(h))\dto{\opt{a}}{\rho(h)}t'}.

``Only if'': Let $R$ be a rooted weak bisimulation between $\rho(g)$
and $\rho(h)$.  Suppose \plat{\rt(g)\goto{a}{g}s}.  \df{unwinding}
yields \plat{\rt(\rho(g))\goto{a}{\rho(g)}s}, so there must be a $t$
such that $\rt(\rho(h))\dto{\opt{a}}{\rho(h)}t$ and $sRt$. As $R$ is
rooted, the case that $a=\tau$ and $t\!=\!\rt(\rho(h))$ cannot apply,
so $\rt(\rho(h))\dto{a}{\rho(h)}t$, hence $\rt(h)\dto{a}{h}t$ by
\df{unwinding}. Furthermore, $sRt$ implies $g_s\bis{w}h_t$.
The other clause follows by symmetry.
\end{proof}

\section{Weak Bisimulation Congruence}

A different modification of weak bisimulation equivalence into a
congruence for the + was proposed in \cite{HM85}.

\begin{proposition}\label{pr-coarsest}
For every equivalence relation $\sim$ on $\IG(Act)$ and every set $L$
of operators on $\IG$ there is a coarsest congruence relation $\sim^c$
that is finer than $\sim$.
\end{proposition}

\begin{proof}
Let a \emph{semantic context} $C[\cdot]$ be an expression build
from process graphs $g\in\IG(Act)$ and the \emph{hole} $[\cdot]$
through application of operators from $L$, and in which the hole
occurs exactly once.  If $C[\cdot]$ is a semantic context and
$g\in\IG(Act)$, then $C[g]$ denotes the process graph obtained by
evaluating the expression $C[\cdot]$ in which $g$ is substituted for
the hole $[\cdot]$.

Alternatively, a semantic context can be regarded as a unary
operator on process graphs: a \emph{primitive context} is obtained
from an operator in $L$ by instantiating all but one of its arguments
by process graphs; and a general semantic context is the
composition of any number (possibly 0) of primitive contexts.

An equivalence relation $\approx$ on $\IG(Act)$ is a congruence for
$L$ iff for every $n$-ary operator $f$ in $L$ one has $g_1 \approx
h_1 \wedge \cdots \wedge g_n \approx h_n
\Rightarrow f(g_1,\ldots,g_n)\approx f(h_1,\ldots,h_n)$. This is the
case iff for every semantic context $C[\cdot]$ one has
$g \approx h \Rightarrow C[g]\approx C[h]$.

Given an equivalence relation $\sim$ on $\IG(Act)$, define $\sim^c$ by
\begin{center}
$g \sim^c h$ iff $C[g] \sim C[h]$ for every semantic context
$C[\cdot]$.
\end{center}

By construction, $\sim^c$ is a congruence on $\IG(Act)$.  For if
$g\sim^c h$ and $D[\cdot]$ is a semantic context, then for
every semantic context $C[\cdot]$ also $C[D[\cdot]]$ is a
semantic context, so $\forall C[\cdot](C[D[g]] \sim C[D[h]])$ and
hence $D[g]\sim^c D[h]$.

The trivial context guarantees that $g \sim^c h \Rightarrow g\sim h$,
so $\sim^c$ is finer than $\sim$.

Finally, $\sim^c$ is the coarsest congruence finer than $\sim$,
because if $\approx$ is any congruence finer than $\sim$, then\\[1ex]
\mbox{}\hfill $g\approx h ~\Rightarrow~ \forall C[\cdot](C[g]\approx C[h])
~\Rightarrow~ \forall C[\cdot](C[g] \sim C[h]) ~\Rightarrow~
g \sim^c h.$~~~\hfill\qed
\end{proof}

\begin{definition}\rm
The coarsest congruence w.r.t.\ the $+$ that is finer than weak
bisimulation equivalence is called \emph{weak bisimulation
  congruence}, notation $\bisc{w}$.
\end{definition}
Here I address the question whether both approaches coincide, i.e.\
whether $\bis{rw} = \bisc{w}$. \pr{rw congruence} immediately yields
$\bis{rw} \subseteq \bisc{w}$. The following proof sketch, due to Jan
Willem Klop [personal communication], is a first attempt to establish
the reverse.

\begin{trivlist} \item[\hspace{\labelsep}\it Proof Sketch.]
It suffices to restrict attention to the graphs in $\IG^\rho(Act)$,
for when $g \bisc{w} h \Rightarrow g\bis{rw} h$ for
$g,h\in\IG^\rho(Act)$, then by \pr{unwinding} the same holds for
$g,h\in\IG(Act)$. [Namely $g\bisc{w}h \Rightarrow \rho(g) \bis{} g
  \bisc{w} h \bis{} \rho(h) \Rightarrow \rho(g) \bisc{w} \rho(h)
  \Rightarrow \rho(g)\bis{rw} \rho(h) \Rightarrow g\bis{}
  \rho(g) \bis{rw} \rho(h) \bis{} h \Rightarrow g\bis{rw} h$.]

So let $g,h\in\IG^\rho(Act)$ and assume
$g\bisc{w}h$. Let $a\neq\tau$ be an action that does not occur
in either $g$ or $h$. Then $g+a.0 \bis{w} h+a.0$ by the definition of
$\bisc{w}$. Let $R$ be a weak bisimulation between $g+a.0$ and $h+a.0$.\\[1ex]
\emph{Claim.} $R$ must be rooted.\\[1ex]
\emph{Proof of Claim.} $\rt(g+a.0) \goto{a}{g+a.0} \rt(0)$, so if
$\rt(g+a.0) \,R\, t$ then $t\dto{a}{h+a.0}t'$ for some
$t'\in\nd(h+a.0)$ with $\rt(0) \,R\, t'$.
This is only possible if $t=\rt(h+a.0)$. By symmetry, $s\,R\,\rt(h+a.0)$
is only possible if $s=\rt(g+a.0)$.\\[1ex]
\emph{Application of Claim.} The restriction of $R$ to the nodes of
$g$ and $h$ is a rooted weak bisimulation between $g$ and $h$, showing
that $g \bis{rw} h$.\qed
\end{trivlist}
The only weak point in this proof sketch is in the choice of an action
$a\neq\tau$ that does not occur in $g$ or $h$. What if such an action
does not exists? Below I present two solutions to this problem.

\subsection{The Fresh Atom Principle}

The \emph{Fresh Atom Principle} (FAP) allows us to use fresh actions in
proofs. It was invented and named by Jan Willem Klop [personal
communication].  In order to justify the use of FAP, one needs to\pagebreak[2]
realise that for any choice of a set of actions $Act$ containing
$\tau$ there exists a class $\IG(Act)$ of process graphs over
$Act$. Likewise a \emph{parametrised} semantic equivalence $\sim$ has
an incarnation in each of these classes, and I write $\sim^{Act}$ to
denote the equivalence $\sim$ as it exists in $\IG(Act)$.  Obviously,
$\IG(A) \subseteq \IG(B)$ for sets of actions $A \subseteq B$.  Now
say that a parametrised equivalence $\sim$ \emph{satisfies} FAP, if, whenever
$A\subseteq B$, $\sim^A$ is the restriction of $\sim^B$ to $\IG(A)$,
i.e.\ if for $g,h\in\IG(A)\subseteq\IG(B)$ one has $g\sim^A h
\Leftrightarrow g \sim^B h$. It is immediate from their definitions that
$\bis{}$, $\bis{w}$, $\bis{rw}$ and most other semantic equivalences
defined in the literature satisfy FAP. In fact, satisfying FAP looks
like a good sanity check for any meaningful equivalence.

In this spirit, one may want to use, instead of $\bisc{w}$, the
coarsest congruence finer than $\bis{w}$ that satisfies FAP, notation
$\bisfc{w}$. This congruence is obtained by allowing, in the proof of
\pr{coarsest}, contexts $C$ that may involve fresh actions.

\begin{theorem}
$\bisfc{w}$ coincides with $\bis{rw}$.
\end{theorem}

\begin{proof} The proof sketch above applies here.
After assuming $g \bisfc{w} h$ in $\IG(Act)$, apply FAP to obtain $g
\bisfc{w} h$ in $\IG(Act\dcup\{a\})$. As in the proof sketch, conclude
that $g \bis{rw} h$ in $\IG(Act\dcup\{a\})$. Since $\bis{rw}$
satisfies FAP this implies that $g \bis{rw} h$ in $\IG(Act)$.\qed
\end{proof}

\subsection{Arbitrary Many Non-bisimilar Processes}

Even though we now know that $\bis{rw}$ coincides with $\bisfc{w}$ and
thus is the coarsest sane equivalence contained in $\bis{w}$ that is a
congruence for the +, the question still remains if also $\bisc{w}$
coincides with $\bis{rw}$. In case $Act=\{\tau\}$, this is not the case.
For in that case $\bis{w}$, and hence also $\bisc{w}$, is the universal
relation, but $\tau.0 \nobis{rw} 0$. However, as I will show in the
following, in all other cases we have in fact that $\bisc{w} = \bis{rw}$.

\begin{proposition}[Jan Willem Klop]\label{pr-ordinal processes}
Provided that there is at least one action $a\in Act-\{\tau\}$, for
each infinite cardinal $\kappa$ there are at least $\kappa$
bisimulation equivalence classes of $\tau$-free process graphs in
$\IG(Act)$ with less than $\kappa$ nodes.
\end{proposition}

\begin{proof}
For each ordinal $\lambda$ define $g_\lambda\in\IG(Act)$ as
follows.
\begin{itemize}
\item $g_0:=0$,
\item $g_{\lambda+1} := g_\lambda + a.g_\lambda$ and
\item for $\lambda$ a limit ordinal,
 $g_\lambda:=\sum_{\mu<\lambda}g_\mu$, meaning that
 $g_\lambda$ is constructed from all graphs
 $g_\mu$ for $\mu<\lambda$ by identifying their root.
\end{itemize}
\emph{Claim 1.}
$\rt(g_\lambda)\goto{a}{g_\lambda}s ~~\Leftrightarrow~~ s=\rt(g_\mu)$ for some
$\mu<\lambda$.\\[1ex]
\emph{Proof of Claim 1.}
A straightforward transfinite induction on $\lambda$.\\[1ex]
\emph{Claim 2.}
If $\mu<\lambda$ then $g_\lambda \nobis{} g_\mu$.\\[1ex]
\emph{Proof of Claim 2,} by transfinite induction on $\lambda$:
Let $\mu < \lambda$. By Claim 1 we have
\plat{\rt(g_\lambda) \goto{a}{g_\lambda} \rt(g_\mu)}.
However, when \plat{\rt(g_\mu)\goto{a}{g_\mu} s} we have
$s=\rt(g_\rho)$ for some $\rho<\mu$, and by induction $g_\mu \nobis{}
g_\rho$. Thus $g_\lambda \nobis{} g_\mu$.\\[1ex]
\emph{Claim 3.} For infinite $\lambda$, $|\nd(g_\lambda)|=|\lambda|$.\\[1ex]
\emph{Proof of Claim 3.}
A straightforward transfinite induction on $\lambda$, using that the
cardinality of a disjoint union of $|\lambda|$ sets of cardinality
$0<\kappa\leq |\lambda|$ is $|\lambda|$.\\[1ex]
\emph{Application of the claims.} For each infinite cardinal $\kappa$
there are $\kappa$ ordinals $\lambda$ smaller than $\kappa$.
Now the proposition follows from Claims 2 and 3.\qed
\end{proof}

\begin{theorem}\label{thm-coincide}
Provided that there is an $a\in Act-\{\tau\}$, on $\IG(Act)$ weak
bisimulation congruence coincides with rooted weak bisimulation equivalence.
\end{theorem}

\begin{proof}
Following the idea from the earlier proof sketch, let $g\bisc{w}h$
with $g,h\in\IG^\rho(Act)$. Let $\kappa$ be the smallest infinite
cardinal, such that $g$ and $h$ have less than $\kappa$ nodes. So
there are less than $\kappa$ process graphs $g_s$ with $s\in\nd(g)$
and $h_t$ with $t\in\nd(h)$.
Hence by \pr{ordinal processes} there is a $\tau$-free process graph
$k$ with $|\nd(k)|<\kappa$, such that $k \nobis{} g_s$ and $k \nobis{}
h_t$ for any such $g_s$ and $h_t$. Now $g+a.k \bis{w} h+a.k$ by the
definition of $\bisc{w}$. Let $R$ be a weak bisimulation between
$g+a.k$ and $h+a.k$.\\[1ex]
\emph{Claim 1.} The restriction of $R$ to $\nd(g)\times\nd(h)$ must be
rooted.\\[1ex]
\emph{Proof of Claim 1.} \plat{\rt(g+a.k)\goto{a}{g+a.k}\rt(k)}, so if
$\rt(g+a.k) \,R\, t$ for some $t\in\nd(h)-\{\rt(h)\}$, then
$t\dto{a}{h+a.k}t'$ for some $t'\in\nd(h)$ with $\rt(k)\,R\,t'$ and
hence $k\bis{w}h_{t'}$. By the
definition of $k$ this is impossible. Likewise, it is impossible that
$s\,R\,\rt(h+a.k)$ for $s\in\nd(g)-\{\rt(g)\}$.\\[1ex]
\emph{Claim 2.} The restriction of $R$ to $\nd(g)\times\nd(h)$ is a weak
bisimulation.\\[1ex]
\emph{Proof of Claim 2.} Let \plat{\rt(g)\goto{b}{g}s}. Then
\plat{\rt(g+a.k)\goto{b}{g+a.k}s}, so there must be a $t\in\nd(h+a.k)$
such that \plat{\rt(h+a.k)\dto{\opt{b}}{h+a.k}t} and $s\,R\,t$. The
possibility that $b=a$ and $t=\rt(k)$ can not occur, for this would
imply $g_s \bis{w} k$. The possibility that $b=\tau$ and
$t=\rt(h+a.k)$ can not occur by Claim 1. Therefore
$t\in\nd(h)-\{\rt(h)\}$ and \plat{\rt(h)\dto{b}{h}t}.
Likewise, \plat{\rt(h)\goto{b}{h}t} implies that there is an
$s\in\nd(g)-\{\rt(g)\}$ with \plat{\rt(g)\dto{b}{g}s} and $s\,R\,t$.
It follows that the restriction of $R$ to $\nd(g)\times\nd(h)$ is a
rooted weak bisimulation between $g$ and $h$. Hence $g\bis{rw}h$.\qed
\end{proof}
Rather than working with arbitrary process graphs, some people prefer
to set a bound on the number of nodes. This happens for instance when
one insists that $\IG(Act)$ should be set rather than a proper
class. That can be achieved by first fixing a set $\cal N$ of
potential nodes, and then allowing only process graphs $g$ with
$\nd(g)\subseteq\cal N$.  For any infinite cardinal $\kappa$ let
$\IG_\kappa(Act)$ be the class of process graphs over $Act$ with less
than $\kappa$ nodes. In particular $\IG_{\aleph_0}(Act)$ is the class of
regular, or finite-state, process graphs. \thm{coincide} transfers
smoothly from $\IG(Act)$ to $\IG_\kappa(Act)$.

\begin{theorem}
Provided that there is an $a\in Act-\{\tau\}$, on $\IG_\kappa(Act)$ weak
bisimulation congruence coincides with rooted weak bisimulation equivalence.
\end{theorem}

\begin{proof}
The proof above goes through because the process $k$ fits in
$\IG_\kappa(Act)$.\qed
\end{proof}
Another cardinality restriction that is sometimes imposed, is the
requirement that each node should have less than $\kappa$ outgoing
edges. In case $\kappa>\aleph_0$, this class of
\emph{$\kappa$-branching} process graphs is not essentially different
from $\IG_\kappa(Act)$, and the same proof applies. More interesting
is the case $\kappa=\aleph_0$. Up to strong bisimulation equivalence,
the \emph{finitely branching} process graphs form a proper superclass
of $\IG_{\aleph_0}(Act)$, the finite-state process graphs, and a
proper subclass of $\IG_{\aleph_1}(Act)$, the countable state process
graphs. However, as shown in \cite{BBK87a}, any countable state
process graph is weakly bisimilar to a finitely branching process
graph. Using this, the proof of \thm{coincide} can be adapted to
apply to the class of finitely branching process graphs as well.

\section{The Left-merge and Rooted Weak Simulations}

In \cite{BK85} is has been shown that $\bis{rw}$ is a congruence for
all operators of ACP$_\tau$. Just as for the $+$, the root condition
comes to the rescue in the congruence proof for the left-merge
\plat{\leftmerge}.  One has \plat{\tau.a.0\leftmerge b.0 \nobis{w}
a.0\leftmerge b.0}, because only the former process can do a $b$ before
an $a$, so $\bis{w}$ fails to be a congruence for this operator.  The
reason that the root condition (\df{rooted}) helps here, is that in
\plat{g\leftmerge h} steps from $h$ can happen in any state of $g$
except the initial one; thus only a weak bisimulation between $g_1$
and $g_2$ that does not relate roots with non-roots can be modified
into a weak bisimulation between \plat{g_1\leftmerge h} and
\plat{g_2\leftmerge h}.

There is a directional difference in the way the root condition solves
the congruence problems for $+$ and \plat{\leftmerge}. This can be seen by
applying it to weak simulation.

\begin{definition}\rm\label{df-weak simulation}
Let $g,h \in \IG^\rho(Act)$.
The graph $g$ is \emph{weakly simulated} by the graph $h$
if there exists a binary relation $R \subseteq \nd (g)
\times \nd (h)$, called a \emph{weak simulation} from $g$ to $h$,
satisfying, for all $a\!\in\!Act$:
\begin{itemize}
\item
$\rt (g) ~R~ \rt (h)$.
\item
If $sRt$ and \plat{s\goto{a}{g} s'}, then there is a $t'$ such that
\plat{t\dto{\opt{a}}{h}t'} and $s'Rt'$.
\end{itemize}
A weak simulation from $g$ to $h$ is \emph{source rooted} if $s \,R\,
\rt(h) ~\Rightarrow~ s=\rt(g)$. It is \emph{target rooted} if $\rt(g) \,R\,
t ~\Rightarrow~ t=\rt(h)$.
\end{definition}
The relation of ``being weakly simulation by'' is a \emph{preorder}
(transitive and reflexive), called the \emph{weak simulation preorder}.
Likewise one obtains the \emph{source rooted weak simulation preorder}
and the \emph{target rooted weak simulation preorder}.

\begin{proposition}
The target rooted weak simulation preorder is a precongruence for the $+$.
This means that if there are target rooted weak simulations from $g_1$ to
$h_1$ and from $g_2$ to $h_2$, then there is a target rooted weak
simulation from $g_1+g_2$ to $h_1 +h_2$.
\end{proposition}

\begin{proof}
Suppose that $R_i$ is a target rooted weak simulation from $g_i$ to
$h_i$ for $g_i,h_i\in\IG^\rho(Act)$ and $i=1,2$ then $R_1\cup R_2$ is
a target rooted weak simulation from $g_1+_\rho g_2$ to $h_1+_\rho h_2$.\qed
\end{proof}

\begin{lemma}
If there is a weak simulation from $g$ to $h$ then there is a target
rooted weak simulation from $g$ to $h$.
\end{lemma}
\begin{proof}
Omit all liaisons of the form $\rt(g)\,R\,t$ with $t\neq\rt(h)$.\qed
\end{proof}

\begin{corollary}
The weak simulation preorder is a precongruence for the $+$, as well as
for action prefixing, even without upgrading it with root conditions.
\end{corollary}
A complete axiomatisation of this preorder is given by the usual
axioms for strong bisimulation, together with the axioms
$x \sqsubseteq x+y$ and $\tau.x = x$, where the latter is a shorthand
for $\tau.x \sqsubseteq x \wedge x \sqsubseteq \tau.x$.

\begin{proposition}
The source rooted simulation preorder is a precongruence for the $\leftmerge$.
\end{proposition}

\begin{trivlist} \item[\hspace{\labelsep}\it Proof Idea.]
Suppose that $R$ is a weak simulation from $g$ to $h$ for
$g,h\in\IG^\rho(Act)$. When adapting $R$ to a weak simulation from
\plat{g\leftmerge k} to \plat{h\leftmerge k}, one needs to make sure
that when \plat{g\leftmerge k} can do a step from $k$, then so can
\plat{h\leftmerge k}.  The only way this can fail is when a non-root
state from $g$ is related to the root of $h$. In that case
\plat{g\leftmerge k} can do a step from $k$, but \plat{h\leftmerge k}
cannot.\qed
\end{trivlist}
The weak simulation preorder fails to be a precongruence for the
\plat{\leftmerge}, for $\tau.a.0$ is weakly simulated by $a.0$, but
\plat{\tau.a.0\leftmerge b.0} is not weakly simulated by \plat{a.0
  \leftmerge b.0}.
This is because the weak simulation from $\tau.a.0$ to $a.0$ is not
source rooted. It follows that the source rooted weak simulation
preorder is strictly finer than the (target rooted) weak simulation
preorder.

It is possible to upgrade the notion of weak simulation by various
conditions, such as the following \emph{stability} requirement \cite{vG93}.
\begin{definition}\rm
A weak simulation $R$ from $g$ to $h$ is \emph{stability respecting} if
\begin{itemize}
\item if $sRt$ and $s \gonotto{\tau}{g}$ then there is a $t'$ such that
  $t\dto{}{h} t'\gonotto{\tau}{h}$ and $sRt'$.
\end{itemize}
\end{definition}
Again, target rootedness is needed to make the induced preorder into
a precongruence for the $+$, and source rootedness to make it into a
precongruence for the \plat{\leftmerge}. This time the two rooted
variants are incomparable, because there is a target rooted, but not
source rooted, stability respecting weak simulation from $\tau.a.0$ to
$a.0$, and a source rooted, but not target rooted, stability
respecting weak simulation from $a.0$ to $\tau.a.0$.

\section{Concluding Remark}

The method to turn simulation or bisimulation based equivalences into
congruences by insisting on root conditions generalises smoothly to
other notions of (bi-)simulation.
In the case of branching, delay and $\eta$-bisimulation, this is
elaborated in \cite{GW96}. Interestingly, the alternative
characterisation of rooted weak bisimulation presented in \pr{Milner}
takes a rather different shape when applied to rooted branching
bisimulation. However, the characterisation with the root
condition of \df{rooted} remains the same.

\subsubsection{Acknowledgement.}
Many crucial ideas incorporated in this paper originate from Jan
Willem Klop, and stem from the mid eighties. Originally, Jan Willem
and I planned to write a joint pamphlet on this matter, but as this
plan never materialised, I finally collected the material in this
paper, dedicated to Jan Willem at the occasion of his sixtieth birthday.

\begin{thebibliography}{BBKB7}

\bibitem[BBK87]{BBK87a}
{\sc J.C.M. Baeten, J.A. Bergstra \& J.W. Klop} (1987):
\newblock {\em On the consistency of {Koomen's} fair abstraction rule.}
\newblock {\sl Theoretical Computer Science} 51(1/2), pp. 129--176.

\bibitem[BK85]{BK85}
{\sc J.A. Bergstra \& J.W. Klop} (1985):
\newblock {\em Algebra of communicating processes with abstraction.}
\newblock {\sl Theoretical Computer Science} 37(1), pp. 77--121.

\bibitem[BK86]{BK86a}
{\sc J.A. Bergstra \& J.W. Klop} (1986):
\newblock {\em Algebra of communicating processes.}
\newblock In J.W.~de Bakker, M.~Hazewinkel \& J.K. Lenstra, editors: {\sl Mathematics and Computer Science}, CWI Monograph 1, North-Holland, pp. 89--138.

\bibitem[Gla93]{vG93}
{\sc R.J.~van Glabbeek} (1993):
\newblock {\em The linear time -- branching time spectrum {II}; the semantics of sequential systems with silent moves (extended abstract).}
\newblock In E.~Best, editor: {\sl {\rm Proceedings} CONCUR'93, {\rm 4$^{\it th}$ International Conference on {\sl Concurrency Theory}, Hildesheim, Germany}}, {\sl \rm LNCS} 715, Springer, pp. 66--81.

\bibitem[GW96]{GW96}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1996):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock {\sl Journal of the ACM} 43(3), pp. 555--600.

\bibitem[HM85]{HM85}
{\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.

\bibitem[Mil90]{Mi90b}
{\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{thebibliography}
\end{document}
