\documentstyle[11pt]{article}		% Fontsize 11 point
\textwidth    		6.5 in		% paper = 8.5x11in
\textheight   		8.98in          %  + foot 30pt = 9.40in
\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       
\parindent		14  pt		% default 17pt

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			Theorem-like environments			  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}

\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{th-#1} }{\end{theo}}
\newenvironment{proposition}[1]{\begin{prop} \rm \label{pr-#1} }{\end{prop}}
\newenvironment{lemma}[1]{\begin{lemm} \rm \label{lem-#1} }{\end{lemm}}
\newenvironment{corollary}[1]{\begin{coro} \rm \label{cor-#1} }{\end{coro}}
\newenvironment{example}[1]{\begin{exam} \rm \label{ex-#1} }{\end{exam}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}

\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\thm}[1]{Theorem~\ref{th-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Corollary~\ref{cor-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\title}[1]{ \vspace*{5pt}
			\renewcommand{\thefootnote}{\fnsymbol{footnote}}
			\setcounter{footnote}{1}
			\begin{center}
			{\LARGE \bf #1\makebox[0pt][l]{\footnotemark}\\ \ \\}
			\setcounter{footnote}{0}
			R.J. van Glabbeek\makebox[0pt][l]{\footnotemark}\\
			\footnotesize
			Computer Science Department, Stanford University\\
			Stanford, CA 94305, USA.\\
			{\tt rvg@cs.stanford.edu}
			\end{center}
			\footnotetext{This work was supported by ONR under
			grant number N00014-92-J-1974.}
			\setcounter{footnote}{2}
\footnotetext{I don't intend to publish this paper separately,
as it will be integrated with {\sc Fokkink} \cite{Fok95b} and
{\sc Aceto \& Ing\'olfsd\'ottir} \cite{AI95} into {\sc Aceto,
Fokkink, Van Glabbeek \& Ing\'olfsd\'ottir} \cite{AFGI95}.}
			\vspace{5pt}			}
\renewcommand{\abstract}[1]{\begin{list}{}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item #1\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}}	% transition
\newcommand{\dto}[1]{\stackrel{#1}{\Longrightarrow}}	% abstract transition
\newcommand{\bis}[1]{ \;				% bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\pf}{{\bf Proof:\ }}			% beginning of proof
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\bibliographystyle{plain}

\title{Branching Bisimulation as a Tool in the Analysis of Weak Bisimulation}
\abstract{It is shown that the analysis of weak congruence can
sometimes be simplified by means of a similar analysis of branching
congruence as an intermediate step. This point is made through a
completeness proof for an equational axiomatization of basic CCS with
prefix iteration.}

\section{Introduction}

A fundamental semantic equivalence in the study of concurrent systems
is {\em bisimulation equivalence} \cite{Mi80}. The concept of
bisimulation equivalence on labelled transition systems without a
notion of invisible action is completely canonical. When invisible
actions, or $\tau$-steps, are introduced however, a certain degree of
freedom in the definition of bisimulation equivalence emerges, even
without considering {\em divergence}. The most prominent version of
bisimulation is {\sc Milner}'s notion of {\em weak (bisimulation)
congruence} or {\em observation congruence} \cite{Mi80}.  An
alternative is the notion of {\em branching (bisimulation) congruence} of
{\sc Van Glabbeek \& Weijland} \cite{GW89ea}.

Since the inception of the branching bisimulation eleven advantages of the
use of branching congruence over other equivalences in general and
weak congruence in particular have been found:
\begin{enumerate}
\vspace{-3pt} \item
Verifications in branching bisimulation semantics are sound
independent of ones notion of observable behaviour \cite{GW89ea,vG93c}.
\vspace{-3pt} \item
No coarser semantics (like weak bisimulation) has this property \cite{GW96}.
\vspace{-3pt} \item
In abstract interleaving semantics no finer notion of bisimulation is
suitable \cite{vG93a}.
\vspace{-3pt} \item
There is a reasonable operator for which branching bisimulation is a
congruence and weak bisimulation or coarser notions are not. On the
other hand no examples testifying for the opposite are known \cite{GW96}.
\vspace{-3pt} \item
Branching bisimulation equivalence is the only known equivalence in
the linear time -- branching time spectrum that supports an
`eventually' operator as part of a temporal logic on transition
systems \cite{GW90}. It even supports all the operators of CTL$^*$ and
corresponds with stuttering equivalence of Kripke structures \cite{DV95}.
\vspace{-3pt} \item
There are practical applications in which weak bisimulation poses a
problem that can be solved by moving to branching bisimulation \cite{GW90}.
No applications have been found in which the reverse holds \cite{GW96}.
\vspace{-3pt} \item
Branching congruence has a lower complexity than any
other abstract semantic equivalence used in concurrency theory \cite{GrV90}.
\vspace{-3pt} \item
For sequential processes, branching congruence is preserved under
action refinement, whereas weak congruence is not \cite{GW89a}.
\vspace{-3pt} \item
Branching congruence has a very appealing complete axiomatization
\cite{vG93a}
\vspace{-3pt} \item
and better term rewriting properties than other (abstract)
bisimulations \cite{GW90,AkBa90,DIN90}.
\vspace{-3pt} \item
Finally, it has a nice characterization as back-and-forth bisimulation \cite{DMV90}.
\vspace{-3pt} \end{enumerate}
On the other hand there is one advantage of weak over branching
congruence, namely that only the former one can be understood as
strong bisimulation congruence on an alternative transition system,
obtainable in a simple way from the original one (namely as a kind of
reflexive and transitive closure) \cite{GW96}.

The purpose of this paper is to add a twelfth advantage of branching
bisimulation to the list above. I claim that even when branching
bisimulation would not be found interesting in its own right, it
may serve as a better tool to prove certain properties about weak
bisimulation than weak bisimulation itself.

This claim is substantiated by means of a comparison between two
proofs of the completeness of an axiomatization for weak bisimulation
congruence over basic CCS with prefix iteration.

In {\sc Aceto \& Ing\'olfsd\'ottir} \cite{AI95}, where the
axiomatization is proposed, a completeness proof in terms of weak
bisimulation is given, counting 12 pages---written out in great
detail---and containing several levels of nested case-distinctions.
I have examined the proof carefully and found no way to significantly
shorten it, otherwise than by removal of details or using branching
bisimulation.

{\sc Fokkink} \cite{Fok95a} also reports on an unsuccessful attempt to
shorten this proof, which however yielded a completeness proof of an
axiomatization for branching bisimulation, counting less than two
pages. For the sake of fairness is should be taken into account that
that proof uses a completeness result for strong bisimulation, proven
in {\sc Fokkink} \cite{Fok94} in four pages---also written out in detail.
However, {\sc Fokkink} \cite{Fok95b} has recently shown how that result
can be obtained in only half a page.

In this paper I show within two pages how the completeness of the
axiomatization of \cite{AI95} for weak congruence follows from the
completeness of the axiomatization of \cite{Fok95a} for branching
congruence. Altogether the route via branching bisimulation is much
simpler than the `direct' way.

I also provide a complete axiomatization for the notion of
{\em delay congruence}, a version of observational equivalence proposed
in {\sc Milner} \cite{Mi81}. This is even more an easy corollary of
the result for branching bisimulation.

\section{Basic CCS with prefix iteration}\label{BCCS}

Assume a set $V$ of {\em variables} and $A$ of {\em actions}.
Let $\tau \not\in A$ denote a special {\em invisible action} and write
$A_\tau := A \cup \{\tau\}$. Let $x,y,...$ range over $V$, $a,b,...$
over $A$ and $\alpha, \beta, ...$ over $A_\tau$.
The language BCCS$^*$ (called MPA$_{\delta}^*(A_\tau)$ in
\cite{Fok94,AI95}) is given by the BNF grammar
$$P:= x \mid 0 \mid \alpha.P \mid P+P \mid \alpha^*P$$ 
One may leave out redundant brackets, assuming that + binds weaker than
$\alpha.$ and $\alpha^*$.

The {\em action relations} $\goto{\alpha}$ between terms over BCCS$^*$
are generated by the following {\em action rules}:
\begin{center}
$\displaystyle\hfill \alpha.x \goto{\alpha} x \hfill
\frac{x \goto{\alpha} x'}{x+y \goto{\alpha} x'} \hfill
\frac{y \goto{\alpha} y'}{x+y \goto{\alpha} y'} \hfill
\alpha^*x \goto{\alpha} \alpha^*x \hfill
\frac{x \goto{\alpha} x'}{\alpha^*x \goto{\alpha} x'} \hfill$
\end{center}
Let $p,q,r,s,t$ (possibly primed or subscripted) range over $T({\rm
BCCS}^*)$, the set of {\em closed} BCCS$^*$ expressions (not
containing variables).
More on prefix iteration can be found in \cite{Fok94,Fok95a,AI95}.

\section{Bisimulations}

This section recalls the definitions and congruence theorems for
several kinds of bisimulation equivalences. For motivation and further
information see \cite{Mi80,Mi81,GW96}.

\begin{definition}{strong}
Two processes $p,q \in T({\rm BCCS}^*)$ are {\em strong
(bisimulation) equivalent} if there
exists a symmetric binary relation ${\cal R}$ on $T({\rm BCCS}^*)$
with $p{\cal R}q$, such that 
$$s{\cal R}t \wedge s\goto{\alpha} t' \mbox{ implies } \exists
t': t \goto{{\alpha}} t' \wedge s'{\cal R}t'.$$
\end{definition}
As observed in \cite{Fok94}, strong equivalence is a congruence for BCCS$^*$.

Write $p \dto{} q$ for $\exists n\geq 0: \exists p_0,...,p_n: p=p_0
\goto{\tau} p_1 \goto{\tau} ... \goto{\tau} p_n = q$, i.e.\ a
(possibly empty) path of $\tau$-steps from $p$ to $q$. Furthermore,
for $\alpha \in A_\tau$, write ${p \goto{(\alpha)} q}$ for $p
\goto{\alpha} q \vee (\alpha=\tau \wedge p=q)$. Thus ${\goto{(a)}}$
is the same as $\goto{a}$ for $a \in A$, and ${\goto{(\tau)}}$
denotes zero or one $\tau$-steps.

\begin{definition}{bb}
Two processes $p,q \in T({\rm BCCS}^*)$ are {\em branching
(bisimulation) equivalent}---notation $p \bis{b} q$---if there
exists a symmetric binary relation ${\cal R}$ on $T({\rm BCCS}^*)$
with $p{\cal R}q$, such that 
\begin{equation}\label{bisimulation}
s{\cal R}t \wedge s\goto{\alpha} s' \mbox{ implies } \exists
t_1,t_2,t': t\dto{} t_1 \goto{(\alpha)} t_2 \dto{} t' \wedge s{\cal
R}t_1 \wedge s'{\cal R}t_2 \wedge s'{\cal R}t'.
\end{equation}
They are {\em branching congruent}---$p \bis{rb} q$---if
$\begin{array}{l}p\goto{\alpha} p' \mbox{ implies } \exists
q': q \goto{\alpha} q' \wedge p'\bis{b}q' \mbox{ and}\\
q\goto{\alpha} q' \mbox{ implies } \exists
p': p \goto{\alpha} p' \wedge p'\bis{b}q'.\end{array}$
\end{definition}
This definition is equivalent to the one in \cite{GW89a,GW90,GW96}, as
follows immediately from the proof of Lemma 1.1 in \cite{GW90,GW96}.
There a relation satisfying (\ref{bisimulation}) is called a {\em semi
branching bisimulation}.

\begin{definition}{weak}
{\em Weak (bisimulation) equivalence} \cite{Mi80}---notation $\bis{w}$---is
defined as $\bis{b}$, but without the requirements $s{\cal R}t_1$ and
$s'{\cal R}t_2$.
Two processes $p$ and $q$ are {\em weak congruent}---notation $p
\bis{rw} q$---if 
$$\begin{array}{l}p\goto{\alpha} p' \mbox{ implies } \exists q_1,q_2,q':
q \dto{}q_1\goto{\alpha}q_2\dto{} q' \wedge p'\bis{w}q' \mbox{ and}\\
q\goto{\alpha} q' \mbox{ implies } \exists p_1,p_2,p':
p \dto{}p_1\goto{\alpha}p_2\dto{} p' \wedge p'\bis{w}q'.\end{array}$$
{\em Delay bisimulation equivalence} \cite{Mi81}---$\bis{d}$---is
defined as $\bis{b}$, but without the requirement $s{\cal R}t_1$.\\[5pt]
$p$ and $q$ are {\em delay congruent}---$p \bis{rd} q$---if
$\begin{array}{l}p\goto{\alpha} p' \mbox{ implies } \exists
q_1,q': q \dto{} q_1 \goto{\alpha} q' \wedge p'\bis{w}q' \mbox{ and}\\
q\goto{\alpha} q' \mbox{ implies } \exists
p_1,p': p \dto{} p_1 \goto{\alpha} p' \wedge p'\bis{w}q'.\end{array}$
\end{definition}
A remarked in \cite{GW90}, the existence requirement of a process $t$
with $t_2 \dto{} t'$ and $s' {\cal R} t'$ is redundant in the
definitions of $\bis{b}$ and $\bis{d}$.

\begin{proposition}{congruence} ({\bf Congruence})
For $x\in\{b,w,d\}$, $\bis{rx}$ is an equivalence relation such that
$$\mbox{if } p\bis{rx}q \mbox{ then }
~\alpha.p\bis{rx}\alpha.q,~~p+r\bis{rx}q+r,~~r+p\bis{rx}r+q~ \mbox{
and }~\alpha^* p\bis{rx}\alpha^* q.$$
Moreover $\bis{rx}$ is the coarsest relation with these properties
contained in $\bis{x}$.
\end{proposition}
\begin{proof} Equivalence is straightforward; see \cite{Bas95} or
\cite{GW96}. However, as observed in {\sc Basten} \cite{Bas95}, the
transitivity proof for $\bis{rb}$ in \cite{GW90} is wrong. He also
shows that stating \df{bb} in terms of semi branching bisimulations
prevents the error.

That $\bis{rx}$ is a congruence for BCCS$^*$ follows
easily from the definitions, using that the relation
$$\{(\alpha^*P,\alpha^*Q) \mid \alpha \in A_\tau, P \bis{rx} Q\}
\cup \bis{x}$$
satisfies (\ref{bisimulation}) (depending on $x$ possibly modified as
in \df{weak}).

That $\bis{rx}$ is the coarsest congruence contained in $\bis{x}$ is shown in
\cite{GW90,GW96}.
\end{proof}
Obviously, $\bis{rb}$ is a finer congruence than $\bis{rw}$ and
$\bis{rd}$ sits in between.

\section{Complete axiomatizations}

{\sc Aceto \& Ing\'olfsd\'ottir} \cite{AI95} proposed the following
axiomatization for weak congruence on BCCS$^*$ expressions.

\begin{figure}[htb]
$$\begin{array}{lr@{~~=~~}l@{~~~~~~~~}lr@{~~=~~}l}
{\rm A1}  & x+y		& y+x	  \\
{\rm A2}  & (x+y)+z	& x+(y+z) &{\rm T1}  & \alpha.\tau.x & \alpha.x      \\
{\rm A3}  & x+x		& x	  &{\rm T3}  & a.(x+\tau.y) &a.(x+\tau.y)+a.y\\
{\rm A0}  & x+0		& x	  &{\rm MT1} &a^*(x+\tau.y)&a^*(x+\tau.y+a.y)\\
{\rm MI1} & \alpha.\alpha^*x+x&\alpha^*x&{\rm MT2} & a^*\tau.a^*x & \tau.a^*x\\
{\rm MI2} & a^*a^*x	& a^*x	  &{\rm FIR} & \tau^*x     & \tau.x          \\
\end{array}$$
\caption{A complete axiomatization for weak bisimulation\label{weak}}
\end{figure}

\noindent
They also derived the following equations from these axioms:
$$\begin{array}{lr@{~~=~~}l@{~~~~~~~~}lr@{~~=~~}l}
{\rm T2}  & \tau.x  	& \tau.x+x	&
{\rm DT2} & \tau.(x+y) + x  & \tau.(x+y)\\
{\rm DMI1}& a^*x	& a^*x+x	&
{\rm MT3} &a^*(x+\tau.y)&a^*(x+\tau.y)+a.y\\
\end{array}$$
It is well known that A0--3 form a complete axiomatization for the
sublanguage without $^*$ and $\tau$, and A0--3 together with T1--3
form a complete axiomatization for weak congruence on the sublanguage
without $^*$ \cite{Mi80}. In {\sc Fokkink} \cite{Fok94} the axioms
A0--3 and MI1--2 are shown to be complete for the sublanguage without
$\tau$ (on which all bisimulation equivalences of the previous section
coincide).  

In \cite{AI95} the entire axiomatization of Figure~\ref{weak} is
proven sound and complete for weak congruence on BCCS$^*$. The new
axioms MT1--2 and FIR were also shown to be independent. All
completeness results mentioned here refer in the first place
to closed terms. In \cite{AI95}, the axioms of Figure
\ref{weak} were in addition shown to be {\em $\omega$-complete},
which together with completeness for closed terms yields completeness
for open terms.

{\sc Fokkink} \cite{Fok95a} established that the axioms A0--3 and
MI1--2 together with
$$\begin{array}{lr@{~~=~~}l}
{\rm B}&	\alpha.(\tau.(x+y)+x)&\alpha.(x+y)\\
{\rm MI6}&	\tau^* x & \tau.x + x \\
{\rm MI7}&	a.a^*(\tau.a^*(x+y)+x) & a.a^*(x+y)
\end{array}$$
form a complete axiomatization of branching congruence on BCCS$^*$. As remarked
before, this result is much easier to obtain than the completeness
result for weak congruence of \cite{AI95}. Therefore I will now
significantly shorten the proof of the latter result by deriving it
from the former.

\begin{proposition}{derivable}
The axioms B and MI6--7 are derivable from the axioms of Figure~\ref{weak}.
\end{proposition}
\pf Let $p \stackrel{X}{=} q$ denote that the equation
$p=q$ is derivable from the laws A1, A2 and $X$.
\begin{itemize}
\item $\alpha.(\tau.(x+y)+x) ~\stackrel{\rm DT2}{=}~ \alpha.\tau.(x+y)
       ~\stackrel{\rm T1}{=}~ \alpha.(x+y)$.
\item $\tau^* x ~\stackrel{\rm FIR}{=}~ \tau.x ~\stackrel{\rm T2}{=}~\tau.x+x$.
\item $a.a^*(\tau.a^*(x+y)+x) ~\stackrel{\rm DMI1}{=}~\\
a.a^*(\tau.(a^*(x+y)+x+y)+x) ~\stackrel{\rm DT2}{=}~\\
a.a^*\tau.(a^*(x+y)+x+y) ~\stackrel{\rm DMI1}{=}~\\
a.a^*\tau.a^*(x+y) ~\stackrel{\rm MT2}{=}~\\
a.\tau.a^*(x+y) ~\stackrel{\rm T1}{=}~\\ a.a^*(x+y)$.\hfill $\Box$
\end{itemize}

\begin{definition}{saturated} 
The {\em derivatives} of a closed BCCS$^*$ expression $p$ are defined
recursively by
\begin{list}{{\bf --}}{\topsep 0pt \itemsep 0pt \parsep 0pt}
\item $p$ is a derivative of $p$
\item if $s$ is a derivative of $p$, and $s \goto{\alpha} t$, then so
is $t$.
\end{list}
A process $p$ is {\em saturated} if for
each of its derivatives $r, s$ and $t$ and $\alpha \in A_\tau$ we have:
$$r \goto{\alpha} s \goto{\tau} t \Rightarrow  r \goto{\alpha} t 
~~~\mbox{and}~~~
r \goto{\tau} s \goto{\alpha} t	\Rightarrow  r \goto{\alpha} t.$$
\end{definition}

\begin{theorem}{saturated}\cite{GW90} If $p$ and $q$ are saturated and
weakly congruent, then they are branching congruent.
\end{theorem}

\begin{proof} If \plat{t \dto{} t_1 \goto{(\alpha)} t_2 \dto{} t'} for
a derivative $t$ of a saturated process $q$, then
\plat{t \goto{(\alpha)} t'}. This also holds with $\alpha$ instead
of \plat{(\alpha)}. Thus if $p$ and $q$ are saturated and
weakly equivalent, then $p {\cal R} q$ for a symmetric relation $\cal
R$ such that $s{\cal R}t \wedge s\goto{\alpha} t' \mbox{
implies } \exists t': t \goto{{(\alpha)}} t' \wedge s'{\cal R}t'.$
\end{proof}

\begin{proposition}{saturated}
Any BCCS$^*$ term $s$ is provably equal to a saturated one.
\end{proposition}

\begin{proof}
A BCCS$^*$ expression $p$ is {\em in head normal form} if
\plat{p\stackrel{\rm A0}{=}\Sigma_{i\in I} \alpha_i . p_i} (with $I$ finite).
By induction on the structure of a process $s$, I prove $s$ equal to a
process that is both saturated and in head normal form.

   The case $s=0$ is trivial.

   Let $s=p+q$. By induction $p$ can be transformed into the required
form $p'$, and similarly $q$ can be brought in saturated head
normal form $q'$. Now $p'+q'$ is saturated and in head normal form.

   Let $s=a.p$ with $a\neq \tau$. Prove $p$ equal to a
saturated process $p'=\Sigma_{i\in I}b_i . p_i + \Sigma_{j\in J}\tau
. q_j$. By T3, $s$ can be proven equal to $s'=a.p' + \Sigma_{j\in J}a.q_j$.
This process is in head normal form and saturated. Namely the
derivatives $p'$ and $q_j$ are saturated by assumption. So let $s'
\goto{\alpha} q \goto{\tau} r$. Then $\alpha =a$ and $q$ must be $p'$ or
$q_j$ with $j \in J$. In case $q=p'$ it must be that $r=q_k$ with
$k\in J$. It follows that $s' \goto{a} r$. In case $q=q_j$
one has $p'\goto{\tau}q\goto{\tau}r$ so it must be that $p'\goto{\tau}
r$ since $p'$ is saturated, and hence $r=q_k$ for certain $k \in J$.
Again $s'\goto{a} r$. The case \plat{s' \goto{\tau} q \goto{\alpha} r}
does not apply.

   Let $s= \tau.p$. Prove $p$ equal to a saturated
process $p'=\Sigma_{i\in I}\alpha_i . p_i$. By T2, $s$ can be proven
equal to $\tau.p' + \Sigma_{i\in I} \alpha_i.p_{i}$.  Just as above, this
process is saturated and in head normal form.

   Let $s=a^*p$ with $a\neq \tau$. Prove $p$ equal to a saturated
process $p'=\Sigma_{i\in I}b_i . p_i + \Sigma_{j\in J}
\tau . q_j$. By MT3, $s$ can be proven equal to $a^*p' + \Sigma_{j
\in J}a.q_j$ which by MI1 equals $a.a^* p' + p' + \Sigma_{j \in J}a.q_j$.
Applying MT1 gives $\vdash s = a.a^*(p' + \Sigma_{j\in J} a . q_j)
+ p' + \Sigma_{j \in J}a.q_j$.
I show that this process $s'$ is saturated.
\begin{list}{$\bullet$}{\labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}
\item All derivatives other than $s'$ itself and $t=a^*(p' + \Sigma_{j\in
J}a . p_i)$ are saturated by assumption.
\item Let $s' \goto{\alpha} q \goto{\tau} r$. There are three possibilities:
\begin{list}{{\bf --}}{\leftmargin 15pt
			\labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 2pt \itemsep 2pt \parsep 0pt}
\item $\alpha=a$ and $q=t$. Then $r=q_k$ with $k \in J$ and $s' \goto{a} r$.
\item $p' \goto{\alpha} q \goto{\tau} r$. In that case $s' \goto{\alpha} r$
since $p'$ is saturated.
\item $\alpha=a$ and $q=q_j$ for certain $j \in J$.
In that case $p'\goto{\tau}q_j\goto{\tau}r$ so it must be that $p'\goto{\tau}
r$ since $p'$ is saturated, and hence $r=q_k$ for certain $k \in J$.
Again $s' \goto{a} r$.
\end{list}
\item Let $s' \goto{\tau} q \goto{\alpha} r$. Then $p' \goto{\tau} q
\goto{\alpha} r$ and since $p'$ is saturated $s' \goto{\alpha} r$.
\item Let $t \goto{\alpha} q \goto{\tau} r$. There are three possibilities:
\begin{list}{{\bf --}}{\leftmargin 15pt
			\labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 2pt \itemsep 2pt \parsep 0pt}
\item $\alpha=a$ and $q=t$. Then $r=q_k$ with $k \in J$ and $t \goto{a} r$.
\item $p' \goto{\alpha} q \goto{\tau} r$. In that case $t \goto{\alpha} r$
since $p'$ is saturated.
\item $\alpha=a$ and $q=q_j$ for certain $j \in J$.
In that case $p'\goto{\tau}q_j\goto{\tau}r$ so it must be that $p'\goto{\tau}
r$ since $p'$ is saturated, and hence $r=q_k$ for certain $k \in J$.
Again $t\goto{a} r$.
\end{list}
\item Let $t \goto{\tau} q \goto{\alpha} r$. Then $p' \goto{\tau} q
\goto{\alpha} r$ and since $p'$ is saturated $t \goto{\alpha} r$.
\end{list}

   Let $s= \tau^*p$. Applying FIR reduces this to the case $s = \tau.p$.
\end{proof}
\pagebreak

\begin{corollary}{complete} The axiom system of Figure~\ref{weak} is
complete for weak congruence.
\end{corollary}
\pf Suppose $s$ is weakly congruent to $t$. Prove $s$ and $t$ equal
to saturated processes $s'$ and $t'$. These must be branching
congruent. Hence $\vdash s' = t'$ using the axioms for branching
congruence.

\section{A complete axiomatization for delay bisimulation}

The technique from the previous section can easily be simplified to find a
complete axiomatization of delay bisimulation. Call a process 
{\em $d$-saturated} if for each of its derivatives $r$, $s$ and $t$ we have
$$r \goto{\tau} s \goto{\alpha} t \Rightarrow  r \goto{\alpha} t.$$
As before it follows that if two processes are $d$-saturated and delay
congruent, they must be branching congruent.

\begin{proposition}{delay}
Any BCCS$^*$ term $s$ can be proven equal to a saturated one, using
axioms A1-2, MI1, T1 and FIR only.
\end{proposition}

\begin{proof} Exactly as before, except for the cases $s= a.p$ and $s =a^*p$.
Note that the axiom T2 (used in the case $s=\tau.p$) is derivable from
FIR, MI1 and T1.

   Let $s=a.p$ with $a\neq \tau$. By induction I may assume that $p$
is $d$-saturated. But then $s$ is also $d$-saturated (and in head normal form).

   Let $s=a^*p$ with $a\neq \tau$. By induction I assume that $p$ is
$d$-saturated and in head normal form. Now ${\rm MI1} \vdash s = a.a^*p + p$, which
is $d$-saturated and in head normal form.
\end{proof}

\begin{corollary}{delay} The axioms A0--3, MI1--2, T1, MT2 and FIR are
complete for delay congruence.
\end{corollary}

\begin{proof} 
As before. The derivations used in \pr{derivable} only employ the
axioms listed above.
\end{proof}
This axiomatization is also sound, as follows from inspection of the axioms.

Using the other saturation property of \df{saturated}, one can easily
find a complete axiomatization for the notion of {\em
$\eta$-bisimulation} \cite{BG87,GW90}.

%\bibliography{/uf/rvg/lib/abbreviations,/uf/rvg/lib/dbase,/uf/rvg/lib/new}
\begin{thebibliography}{10}

\bibitem{AFGI95}
{\sc L.~Aceto, W.J. Fokkink, R.J. van Glabbeek \& A.~Ing\'olfsd\'ottir} (1995):
\newblock {\em Equational axiomatizations for prefix iteration with silent steps.}
\newblock In preparation.
\vspace{-2pt}
\bibitem{AI95}
{\sc L.~Aceto \& A.~Ing\'{o}lfsd\'{o}ttir} (1995):
\newblock {\em A complete equational axiomatization for prefix iteration with silent steps.}
\newblock Research Report RS--95--5, BRICS (Basic Research in Computer Science), Department of Mathematics and Computer Science, Aalborg University, Denmark.
\newblock Available at {\tt ftp://ftp.daimi.aau.dk/pub/BRICS/RS/95/5/BRICS-RS-95-5.dvi.gz}.
\vspace{-2pt}
\bibitem{AkBa90}
{\sc G.J. Akkerman \& J.C.M. Baeten} (1990):
\newblock {\em Term rewriting analysis in process algebra.}
\newblock Report P9006, Programming Research Group, University of Amsterdam.
\vspace{-2pt}
\bibitem{BG87}
{\sc J.C.M. Baeten \& R.J.~van Glabbeek} (1987):
\newblock {\em Another look at abstraction in process algebra.}
\newblock In Th. Ottmann, editor: {\sl Proceedings $\it 14^{th}$ ICALP, {\sl Karlsruhe}}, {\sl \rm LNCS} 267, Springer-Verlag, pp. 84--94.
\vspace{-2pt}
\bibitem{Bas95}
{\sc T.~Basten} (1995):
\newblock {\em Branching bisimulation is an equivalence indeed!}
\newblock Unpublished manuscript.%
\vspace{-2pt}
\bibitem{DIN90}
{\sc R.~De~Nicola, P.~Inverardi \& M.~Nesi} (1990):
\newblock {\em Using axiomatic presentation of behavioural equivalences for manipulating {CCS} specifications.}
\newblock In J.~Sifakis, editor: {\sl Automatic Verification Methods for Finite State Systems}, {\sl \rm LNCS} 407, Springer-Verlag, pp. 54--67.
\vspace{-2pt}
\bibitem{DMV90}
{\sc R.~De~Nicola, U.~Montanari \& F.W. Vaandrager} (1990):
\newblock {\em Back and forth bisimulations.}
\newblock In J.C.M. Baeten \& J.W. Klop, editors: {\sl Proceedings CONCUR 90, {\rm Amsterdam}}, {\sl \rm LNCS} 458, Springer-Verlag, pp. 152--165.
\vspace{-2pt}
\bibitem{DV95}
{\sc R.~De~Nicola \& F.W. Vaandrager} (1995):
\newblock {\em Three logics for branching bisimulation.}
\newblock {\sl Journal of the ACM} 42(2), pp. 458--487.
\vspace{-2pt}
\bibitem{Fok94}
{\sc W.J. Fokkink} (1994):
\newblock {\em A complete equational axiomatization for prefix iteration.}
\newblock {\sl Information Processing Letters} 52, pp. 333--337.
\vspace{-2pt}
\bibitem{Fok95a}
{\sc W.J. Fokkink} (1995):
\newblock {\em A complete axiomatization for prefix iteration in branching bisimulation.}
\newblock Logic Group Preprint Series 126, Utrecht University.
\newblock To appear in {\sl Fundamenta Informaticae}. Available at {\tt ftp://ftp.phil.ruu.nl/pub/logic/PREPRINTS/preprint126.ps}.%
\vspace{-2pt}
\bibitem{Fok95b}
{\sc W.J. Fokkink} (1995):
\newblock Personal communication.
\vspace{-2pt}
\bibitem{vG93a}
{\sc R.J.~van Glabbeek} (1993):
\newblock {\em A complete axiomatization for branching bisimulation congruence of finite-state behaviours.}
\newblock In A.M. Borzyszkowski \& S.~Soko\l owski, editors: {\sl {\rm Proceedings} Mathematical Foundations of Computer Science 1993 (MFCS), {\rm Gdansk, Poland, August/September 1993}}, {\sl \rm LNCS} 711, Springer-Verlag, pp. 473--484.
\newblock Available by anonymous ftp at {\tt ftp://Boole.stanford.edu/pub/DVI/complete.dvi.gz}.
\vspace{-2pt}
\bibitem{vG93c}
{\sc R.J.~van Glabbeek} (1994):
\newblock {\em What is branching time semantics and why to use it?}
\newblock In M.~Nielsen, editor: {\sl The Concurrency Column}, {\sl Bulletin of the EATCS} 53, pp. 190--198.
\newblock Also available as Report STAN-CS-93-1486, Stanford University, 1993, and by ftp at {\tt ftp://Boole.stanford.edu/pub/DVI/branching.dvi.gz}.
\vspace{-2pt}
\bibitem{GW89ea}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1989):
\newblock {\em Branching time and abstraction in bisimulation semantics (extended abstract).}
\newblock In G.X. Ritter, editor: {\sl Information Processing 89, {\rm Proceedings of the IFIP 11th World Computer Congress, San Fransisco 1989}}, North-Holland, pp. 613--618.
\newblock Full version appeared as \cite{GW90}.
\vspace{-2pt}
\bibitem{GW89a}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1989):
\newblock {\em Refinement in branching time semantics.}
\newblock Report CS-R8922, CWI, Amsterdam.
\newblock Also appeared in: Proceedings AMAST Conference, May 1989, Iowa, USA, pp. 197--201.
\vspace{-2pt}
\bibitem{GW90}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1990):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock Technical Report TUM-I9052, SFB-Bericht Nr.\ 342/29/90 A, Institut f\"{u}r Informatik, Technische Universit\"{a}t M\"{u}nchen, Germany.
\newblock Extended abstract appeared as \cite{GW89ea}.
\vspace{-2pt}
\bibitem{GW96}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1995):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock Revision of \cite{GW90}.
\newblock {\sl {\rm To appear in the} Journal of the ACM}.
\vspace{-2pt}
\bibitem{GrV90}
{\sc J.F. Groote \& F.W. Vaandrager} (1990):
\newblock {\em An efficient algorithm for branching bisimulation and stuttering equivalence.}
\newblock In M.~Paterson, editor: {\sl Proceedings $17^{th}$ ICALP, {\rm Warwick}}, {\sl \rm LNCS} 443, Springer-Verlag, pp. 626--638.
\vspace{-2pt}
\bibitem{Mi80}
{\sc R.~Milner} (1980):
\newblock {\em A Calculus of Communicating Systems}, {\sl \rm LNCS} 92.
\newblock Springer-Verlag.
\vspace{-2pt}
\bibitem{Mi81}
{\sc R.~Milner} (1981):
\newblock {\em A modal characterisation of observable machine-behaviour.}
\newblock In G.~Astesiano \& C.~Bohm, editors: {\sl Proceedings CAAP 81}, {\sl \rm LNCS} 112, Springer-Verlag, pp. 25--34.

\end{thebibliography}
\end{document}
