%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Sizes, first for US letter format %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentstyle[11pt]{article} % Fontsize 11 point
\textwidth 6.5 in % paper = 8.5x11in
\textheight 8.58in % + foot 30pt = 9.00in
\oddsidemargin 0 pt % 1 inch margin comes for free
\evensidemargin 0 pt % 1 inch margin comes for free
\topmargin 0 pt % 4 margins of 1in each
\headheight 0 pt % default 12pt = 0.42cm
\headsep 0 pt % default 25pt = 0.88cm
\unitlength 1 mm % This is used in pictures
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% On A4 paper the right margin is 6 mm smaller, %%%%
%%%% whereas the bottom margin is 17.6 mm longer. %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside} \newlength{\shifttop}
\setlength{\shiftside}{-3mm} \setlength{\shifttop}{8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 0 for American paper or 1 for A4.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% 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{\th}[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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Macros %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\title}[1]{ \vspace*{5pt}
\setcounter{footnote}{0}
\renewcommand{\thefootnote}{\fnsymbol{footnote}}
\begin{center}
{\LARGE \bf #1\\ \ \\}
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.}
\renewcommand{\thefootnote}{\arabic{footnote}}
\setcounter{footnote}{0}
\vspace{5pt} }
\renewcommand{\abstract}[1]{\begin{list}{}
{\rightmargin\leftmargin
\listparindent 1.5em
\parsep 0pt plus 1pt}
\small\item #1\end{list}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\cdot}{\cup}} % disjoint union
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}} % openface letter
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox % openface character
[0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}} % no vertical space
\newcommand{\Id}[1]{[\hspace{-1.4pt}[#1]\hspace{-1.2pt}]} % denotation
\newcommand{\In}[1]{\plat{ % notation
\stackrel{\mbox{\tiny $/\hspace{-2.1pt}/$}}
{\raisebox{-.3ex}[.3ex]{\tiny $\backslash
\hspace{-2.1pt}\backslash$}}\!\!#1\!\!
\stackrel{\mbox{\tiny $\backslash\hspace{-1.8pt}\backslash$}}
{\raisebox{-.3ex}[.3ex]{\tiny $/\hspace{-1.8pt}/$}} }}
\newcommand{\rec}[1]{\plat{ % recursion
\stackrel{\mbox{\tiny $/$}}
{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
\!\!#1\!\!
\stackrel{\mbox{\tiny $\backslash$}}
{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\lto}[1]{\stackrel{#1}{\rightarrow}} % subtransition
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}} % transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt} % no transition
\stackrel{#1\ }{\longrightarrow}}
\newcommand{\dto}[1]{\stackrel{#1}{\Longrightarrow}} % abstract transition
\newcommand{\bis}[1]{ \; % bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt} % no bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}\,$}}
\newcommand{\pf}{{\bf Proof:\ }} % beginning of proof
\newcommand{\qed}{\hfill $\Box$ \par \vskip 2.5ex \noindent} % end of proof
\newcommand{\bsection}[1]{\section*{\refstepcounter{section}\thesection
\hspace{1em} #1} \addcontentsline{toc}{subsection}{\thesection
\hspace{1.5em} #1}} % fooling .toc file
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Abbreviations %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}} % natural numbers
\newcommand{\fE}{{\cal E}} % expressions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\bibliographystyle{plain} % Actually the vG-style is used here
\title{A Complete Axiomatization for Branching Bisimulation
Congruence of Finite-State Behaviours}
\abstract{This paper offers a complete inference system for branching
bisimulation congruence on a basic sublanguage of CCS for representing
regular processes with silent moves. Moreover, complete
axiomatizations are provided for the guarded expressions in this
language, representing the divergence-free processes, and for the
recursion-free expressions, representing the finite processes.
Furthermore it is argued that in abstract interleaving semantics (at
least for finite processes) branching bisimulation congruence is the
finest reasonable congruence possible. The argument is that for closed
recursion-free process expressions, in the presence of some standard
process algebra operations like partially synchronous parallel
composition and relabelling, branching bisimulation congruence is
completely axiomatized by the usual axioms for strong congruence
together with Milner's first $\tau$-law $a\tau X = aX$.}
\tableofcontents
\bsection{Introduction}
An important class of mathematical models for concurrent systems are
the {\em term models}, in which a {\em process} or behaviour (of a
system) is represented as a congruence class of expressions in a {\em
system description language}. The best known system description
language is {\sc Milner}'s {\em Calculus of Communicating Sytems}
(CCS), and the best known congruence on CCS expressions\footnote{In
this first paragraph I restrict myself to expressions that model
behaviours without hidden moves ($\tau$-actions).} is {\em bisimulation
congruence} \cite{Mi90ccs}. The choice of bisimulation congruence was
originally motivated by a notion of {\em observability}: ``processes
are equal iff they are indistinguishable by any experiment based on
observation'' \cite{Mi90ccs}. However, since the appearance of
bisimulation congruence, many alternative notions of observability, or
{\em testing scenarios}, have been proposed, all leading to
different---and invariably coarser---congruences. See {\sc Van
Glabbeek} \cite{vG90a} for an overview. What makes bisimulation
congruence special among all these alternatives is not so much the
underlying notion of observation, but the fact that it is the {\em
finest} reasonable congruence. To be precise, this is the case in {\em
interleaving semantics}, where the ``concurrent occurrence of two
observable actions is not distinguished from their occurrence in
arbitrary sequence'' \cite{Mi90ccs}. In non-interleaving semantics one
finds finer congruences, but the finest ones are just variations of
bisimulation congruence that take {\em causal dependence} between
action occurrences explicitly into account. What makes bisimulation
congruence the finest reasonable congruence are two properties:
\begin{itemize}
\item Any two bisimilar process expressions have the same internal
structure, to be precise the same {\em branching structure}. As the
observable behaviour of processes according to any alternative
(interleaving based) testing scenario is completely determined by their
branching structure, it follows that other observable congruences must
be coarser.
\item Finer equivalences than bisimulation congruence (such as {\em
tree equivalence} or {\em graph isomorphism}) suffer from serious
drawbacks such as a higher complexity (to decide the equivalence of
finite-state behaviours) and the inequivalence of standard operational
and denotational interpretations of CCS-like system description
languages.
\end{itemize}
A crucial tool in practical applications of system description
languages like CCS, especially for verification purposes, is an {\em
abstraction} mechanism. Abstraction is usually performed by turning
actions that are considered unimportant into the {\em invisible}
action $\tau$. Then, a system that after some activity reaches a state
from which only an invisible action is possible, leading to another
state, is considered equivalent to an otherwise identical system, that
after said activity immediately reaches the other state. Thus the
mechanism of abstraction by hiding of irrelevant or unobservable
actions needs support from the congruence notion employed.
There are many ways to extend bisimulation congruence to processes with
hidden moves. The simplest generalization is {\em strong (bisimulation)
equivalence}, in which $\tau$-actions are treated no different than
visible actions. For this reason strong congruence is not {\em
abstract} in the sense stipulated above. Another option is to take the
testing scenario underlying bisimulation equivalence as primary,
incorporating the unobservable nature of hidden moves. This yields {\sc
Milner}'s notion of {\em weak (bisimulation) congruence} \cite{Mi90ccs},
also called {\em observation congruence}, in spite of the rather
far-going assumptions about the capabilities of observers that need to
be made for weak congruence to be truly observable. In {\sc Van Glabbeek
\& Weijland} \cite{GW90} another generalization of bisimulation
congruence was proposed. {\em Branching (bisimulation) congruence} is
not so much motivated in terms of its testing scenario (although it has
one that is arguably only twice as contrived as that of weak
bisimulation congruence), but generalizes the property of bisimulation
congruence of being the finest reasonable interleaving congruence to an
abstract setting. To be precise: it preserves the branching structure
of processes (unlike weak congruence) \cite{GW90}, and (at least for
finite processes) any finer or incomparable abstract version of
bisimulation congruence violates the {\em expansion theorem}
\cite{Mi90ccs}, that is characteristic for interleaving semantics.
Besides a substantiation of the last claim, this paper offers a
complete axiomatization of branching bisimulation congruence for a
sublanguage BCCS$^\omega$ of CCS, only containing operators for
action, inaction, choice and recursion. The B stands for {\em Basic}
and $\omega$ is a strict upper bound for the number of arguments of the
choice and recursion operators. This language represents all and only
the {\em regular processes} or {\em finite-state behaviours}. Moreover,
complete axiomatizations for two sublanguages are given: the language
of {\em recursion-free} BCCS$^\omega$ expressions, representing the
{\em finite} processes, and the language of {\em guarded} BCCS$^\omega$
expressions, representing the {\em divergence-free}
processes, where a processes is {\em divergent} if it has a state from
which an infinite sequence of hidden moves is possible.
A complete axiomatization for strong congruence on BCCS$^\omega$ was
provided in {\sc Milner} \cite{Mi84}. It consisted of the axioms E1-4,
A0-3 and R1-3 of Section 4 (as well as $\alpha$-conversion,
which is derivable). A complete axiomatization for weak congruence on a
slightly different language was first provided in {\sc Bergstra \&
Klop} \cite{BK88}. A more aesthetic axiomatization (on BCCS$^\omega$),
partly inspired by the one in \cite{BK88}, was given in {\sc Milner}
\cite{Mi89a}. It consisted of the axioms for strong congruence, 3
so-called $\tau$-laws, and 2 extra axioms for unguarded recursion
(besides R3). The present axiomatization counts, besides the axioms for
strong congruence, only one $\tau$-law, but 3 extra axioms for
unguarded recursion (all weaker than the axioms for weak congruence).
In all three cases the axioms for unguarded recursion can be dropped to
obtain complete axiomatizations for guarded expressions, and on top of
that R1 and R2 can be dropped to obtain complete axiomatizations for
finite processes.
Milner's completeness proof was delivered in five steps:
\newcounter{steps}
\begin{list}{(\alph{steps})\hfill}{\usecounter{steps}
\setlength{\leftmargin}{25pt}
\setlength{\labelwidth}{\leftmargin}
\addtolength{\labelwidth}{-\labelsep}
}% \setlength{\topsep}{3pt}
% \setlength{\itemsep}{3pt}
% \setlength{\parsep}{0pt}}
\item Any expression can be converted into a guarded one.
\item Any guarded expression provably satisfies a standard guarded set
of equations.
\item Any standard guarded set of equations can be converted into a saturated
one (preserving the property of being provably satisfied by an expression).
\item Two congruent processes that each provably satisfy a saturated standard
guarded set of equations, provably satisfy a common guarded
set of equations.
\item If two guarded expressions satisfy the same guarded set of
equations, they are provably equal.
\end{list}
Steps (b) and (e) only use the axioms for strong congruence, and can thus
be applied in the setting of branching bisimulation as well. Step (a) can
be made completely analogous, even though the present axioms for
unguarded recursion are much more complicated (in particular, the
side-condition of R4 can not be eliminated, as could be done for the
corresponding axiom R5 in \cite{Mi89a}). Step (c) must be skipped as
saturation is unsound in branching bisimulation semantics, and
therefore step (d) needs to be made more subtle. But the absence of step
(c) makes it possible to incorporate step (b) into step (d) at no extra cost.
The completeness theorem for branching congruence on recursion-free
process expressions, at least the closed ones, was already proven in
\cite{GW90} by the method of graph transformations, due to {\sc
Bergstra \& Klop} \cite{BK85}. The present proof is distinctly shorter.
On the other hand, the method of graph transformations, once mastered,
tends to deliver completeness proofs on finite closed terms for
arbitrary interleaving equivalences almost instantaneously, whereas the
method used here seems rather bisimulation oriented and requires more
thought.
\bsection{A language for finite-state behaviours}
Let the nonempty set $A$ of {\em visible actions} and the disjoint
infinite set $V$ of variables be given.
Let $\tau\not\in A$ be the {\em invisible action} or {\em hidden move}
and write $A_{\tau} = A \cup \{\tau\}$.
\begin{definition}{expressions}
The set $\fE$ of {\em process expressions} over BCCS$^{\omega}$ is
given by
$$\begin{array}{llll}
\hline
X & \in \fE & \mbox{for } X \in V & (\mbox{variable}) \\
0 & \in \fE & & (\mbox{inaction}) \\
aE & \in \fE & \mbox{for } a\in A_{\tau}
\mbox{ and } E \in \fE & (\mbox{action}) \\
E+F & \in \fE & \mbox{for } E,F \in \fE & (\mbox{choice}) \\
\mu XE & \in \fE & \mbox{for } X\in V_S
\mbox{ and } E \in \fE & (\mbox{recursion}) \\
\hline
\end{array}$$
\end{definition}
The expression $0$ represents a process that is unable to perform any
action. $aE$ represents a process that first performs the action $a$
and then proceeds as $E$. $E+F$ represents a process that will
behave as either $E$ or $F$, and $\mu XE$ represents a solution of
the equation $X=E$.
\begin{definition}{free}
An occurrence of a variable $X$ in an expression $E \in \fE$ is {\em
bound} if it occurs in a subexpression of the form $\mu XF$. Otherwise
it is {\em free}. $E$ is {\em open} if it contains a free occurrence of
a variable, and {\em closed} otherwise. $E\{F/X\}$ denotes the result
of substituting $F$ for all free occurrences of $X$ in $E$, if
necessary\footnote{Renaming is necessary if a free occurrence of $X$
appears in a subterm $\mu YG$ of $E$ with $Y$ occurring free in $F$.}
renaming bound variables in $E$ in order to ensure that no free
occurrence of a variable in $F$ becomes bound in $E\{F/X\}$. Likewise
$E\{E_X/X\}_{X\in V'}$, for $V' \subseteq V$, denotes the result of
simultaneously substituting $E_X$ for $X$ in the same fashion.
\end{definition}
\begin{definition}{transitions}
The transition relation $\longrightarrow \subseteq \fE\times (A_{\tau}\cup V)
\times\fE$ is the smallest relation satisfying
\begin{itemize}
\item \plat{X \goto{X} 0} for $X \in V$
\item $aE \goto{a} E$ for $a\in A_{\tau}$
\item if $E \goto{x} G$ or $F \goto{x} G$ then $E+F \goto{x} G$
\item if $E\{\mu XE/X\} \goto{x} F$ then $\mu XE \goto{x} F$
\end{itemize}
Here $E \goto{a} F$ for $a\in A_{\tau}$ means that the system represented
by $E$ can perform the action $a$, thereby evolving into $F$, and \plat{E
\goto{X} 0} means that the system represented by $E$ has the
possibility to continue as whatever system is substituted for the
variable $X$.
\end{definition}
\begin{definition}{reachable}
Let $E \in \fE$. The set $\fE_E$ of process expressions {\em reachable}
from $E$ is defined as the smallest subset of $\fE$ satisfying
$E \in \fE_E$ and if $F \goto{a} G$ with $a\in A_{\tau}$ and $F \in
\fE_E$ then $G\in \fE_E$.
\end{definition}
\begin{proposition}{regular}
$\fE_E$ is finite for $E \in \fE$.
\end{proposition}
\pf Consider the transition relation $\rightarrow \subseteq \fE' \times
(A_\tau \dcup \{+,\mu\})\times \fE'$, given by
\begin{itemize}
\item $aE \lto{a} E$
\item $E+F \lto{+} E$ and $E+F \lto{+} F$
\item $\mu XE \lto{\mu} E\{\mu XE/X\}$
\end{itemize}
Here $\fE'$ is defined as $\fE$, except that every operator symbol
($X,0,a,+,\mu X$) in an expression $E \in \fE'$ is coloured either red
or black. Furthermore, if in a subexpression $aF$, $F+G$ or $\mu XF$
of $E$ the leading operator $a$, $+$ or $\mu X$ is coloured black, the
entire subexpression must be black. Whether an occurrence of a variable
is free or bound does not depend on its colour. Substitution on $\fE'$
is defined such that $E\{F/X\}$ means $E\{black(F)/X\}$ (i.e. a black
version of $F$ is substituted for any free red or black occurrence of
$X$), and renaming of bound variables doesn't change their colour.
Furthermore colours are preserved under transitions.
Choose $E\in \fE$ and let $\fE'_E$ be the set of coloured expressions in
$\fE'$ that are reachable by $\rightarrow$ from $red(E)$.
If $F \goto{a} F'$ for $F,F'\in \fE$, and $F_0\in \fE'$ is a coloured
version of $F$, then there must be $F_1, \ldots, F_{n+1} \in \fE'$ with $n \in
\IN$ such that $F_{i-1} \lto{+} F_i$ or $F_{i-1} \lto{\mu} F_i$ for
$i=1,\ldots,n$, $F_n \lto{a} F_{n+1}$ and $F_{n+1}$ is a coloured version
of $F'$. Thus for any $F \in \fE_E$ a coloured version appears in
$\fE'_E$, and it suffices to proof that $\fE'_E$ is finite, or becomes
finite after forgetting the colours.
Observe that if an expression $F$ is partly red and $F\lto{}F'$
then the red part of $F'$ is smaller than the red part of $F$. Thus
there are only finitely many expressions in $\fE'_E$ that are partly red.
Furthermore observe that for any $F \in \fE'_E$, if $F$ contains a
subexpression $\mu YG$ with $\mu Y$ red, then no black subexpression
of $G$ contains a free occurrence of $Y$. This property is trivially true
for $red(E)$, trivially preserved under $\lto{a}$ and $\lto{+}$, and
preserved under $\lto{\mu}$ by the renaming-of-bound-variables
convention of \df{free}. It follows that if $F \in
\fE'_E$ is partly red and $F \lto{} F'$, then the black subexpressions
of $F$ that are inherited by $F'$---unlike the red ones---are
unchanged in $F'$. Thus if $H \in \fE'_E$ is partly red, $H \lto{} H'$
and $H'$ is completely black, then $H'$ has the form $\mu XG$ and has
been generated by a derivation $\mu XG \lto{\mu} G\{\mu XG/X\}$. Hence
the black term $H=\mu XG \in \fE'_E$ also occurs as a partly red
term $\mu XG \in \fE'_E$.
It follows that $\fE_E$ is finite. In fact $\fE_E$ contains at most
one element more than it has subexpressions of the form $aF$. \hfill $\Box$
\begin{definition}{guarded}
A free occurrence of a variable $X$ in an expression $E \in \fE$ is
{\em guarded} if it occurs in a subexpression of the form $aF$ with
$a\in A$ (i.e. $a \neq \tau$). $X$ is {\em (un)guarded} in $E$ if (not)
every free occurrence of $X$ in $E$ is guarded. A process expression
$E \in \fE$ is {\em guarded} if for every subexpression $\mu XF$, $X$
is guarded in $F$. Let $\fE^g \subseteq \fE$ be the set of guarded
process expressions over BCCS$^\omega$.
\end{definition}
\begin{definition}{finite}
A process expression $E \in \fE$ is called {\em finite} or, more accurately,
{\em recursion-free} if it has no subexpression of the form $\mu XF$. Let
$\fE^f \subseteq \fE^g \subseteq \fE$ be the set of finite process
expressions over BCCS$^\omega$.
\end{definition}
\begin{lemma}{finite}
If $E\in \fE^f$, then the relation $\goto{}$ is well-founded in $\fE_E$.
This means that there are no $F_i \in \fE_E$ and $a_i \in A_\tau$ for
$i \in \IN$ with $F_i \goto{a_i} F_{i+1}$ for $i \in \IN$.
\end{lemma}
\pf If $F \in \fE^f$ and $F \goto{a} F'$ then $F' \in \fE^f$ and
$F'$ is smaller than $F$.\hfill $\Box$
\begin{lemma}{guarded}
If $E\in \fE^g$, then the relation $\goto{\tau}$ is well-founded in $\fE_E$.
\end{lemma}
\begin{proof}
First note that if $E$ is guarded and $F \in \fE_E$ then $F$ is
guarded. This follows with a straightforward induction on derivations.
For $F \in \fE$, let $F^*$ be $F$, in which every occurrence of a
subterm $aG$ with $a \in A$ is replaced by $0$. Note that if $F$ is
guarded then $F^*$ is guarded, and if $F \goto{\tau} G$ then $F^*
\goto{\tau} G^*$. Now suppose there is an infinite path $F_0
\goto{\tau} F_1 \goto{\tau} F_2 \goto{\tau} \cdots$ as denied in the
lemma. Then there must be an infinite path $F_0^* \goto{\tau} F_1^*
\goto{\tau} F_2^* \goto{\tau} \cdots$, only passing through guarded
process expressions without subexpressions of the form $aG$ for $a
\in A$. But if $H$ is such an expression and $H \goto{\tau} H'$, then
$H'$ is smaller than $H$, yielding a contradiction.
\end{proof}
Write $E \dto{} E'$ if there are $E_0 , \dots , E_n \in \fE$ with
$E=E_0 \goto{\tau} E_1 \goto{\tau} \cdots \goto{\tau} E_n = E'$.
\begin{lemma}{X}
$X \in V$ is unguarded in $E\in \fE$ iff $E \dto{}E'\goto{X} 0$.\\
\pf Straightforward.\hfill $\Box$
\end{lemma}
\begin{definition}{alpha} Renaming of bound variables is called {\em
$\alpha$-conversion}. Write $E =_\alpha F$ if $E,F \in \fE$ only
differ by $\alpha$-conversion.
\end{definition}
\begin{lemma}{substitution} Let $x \in A_\tau \cup V$.
\begin{enumerate}
\item \plat{H \goto{X} 0 \wedge E \goto{x} F ~~\Rightarrow~~H\{E/X\}
\goto{x} F}
\item \plat{H \goto{x} H'\wedge x\neq X ~~\Rightarrow~~H\{E/X\}
\goto{x} H''\{E/X\}} with $H' =_\alpha H''$
\item \plat{H\{E/X\} \goto{x} F ~~\Rightarrow~~ (H \goto{X} 0 \wedge E
\goto{x} F) \vee (x\neq X \wedge H \goto{x} H' =_\alpha
H'' \wedge F=H''\{E/X\})}
\end{enumerate}
\end{lemma}
\begin{proof} 1.\ and 2.\ are straightforward by induction on inference. I
will prove 3.\ by induction on the inference of $H\{E/X\} \goto{x} F$.
In case $H=X$ the first alternative applies: $\plat{H \goto{X} 0} \wedge E
\goto{x} F$. The cases $F=Y\neq X$, $H=aG$, $H=H_1 + H_2$ and $H=\mu
XG$ are straightforward, so assume $H=\mu YG$ with $Y \neq X$. Let
$\tilde{H}= \mu \tilde{Y}\tilde{G}$ be the result of renaming bound
variables in $H$, as described in \df{free}. Now, by a
shorter inference $\tilde{G}\{E/X\}\{\tilde{H}\{E/X\}/\tilde{Y}\}
= \tilde{G}\{\tilde{H}/\tilde{Y}\}\{E/X\} \goto{x} F$, so by
induction $(\plat{\tilde{H} \goto{X} 0} \wedge E \goto{x} F) \vee
(x\neq X \wedge \tilde{H} \goto{x} \tilde{H}' =_\alpha H'' \wedge
F=H''\{E/X\})$, from which the desired conclusion follows.
\end{proof}
\bsection{Branching bisimulation congruence}
\begin{definition}{bb}
A {\em branching bisimulation} is a symmetric relation ${\cal R} \subseteq
\fE\times\fE$ such that $\forall x\in A_{\tau} \cup V$:
$$\mbox{ if } (E,F)\in {\cal R} \wedge E\goto{x} E'
\mbox{ then } \begin{array}{l}x=\tau \mbox{ and } (E',F)\in {\cal R}\\
\mbox{or } \exists F'',F': F \dto{} F'' \goto{x} F' \wedge (E,F'')\in {\cal R}
\wedge (E',F')\in {\cal R}. \end{array}$$
Two expressions $E$ and $F$ are {\em branching (bisimulation)
equivalent}---notation $E \bis{b} F$---if there exists a branching
bisimulation ${\cal R}$ with $(E,F)\in {\cal R}$.
\end{definition}
For further motivation of branching bisimulation equivalence see
{\sc Van Glabbeek \& Weijland} \cite{GW90}. The consise definition
above is possible thanks to the following lemma.
\begin{lemma}{stutter}
If $E\bis{b}F$, $E\bis{b}F''$ and $F \dto{} F''$, then $E \bis{b} F'$
for any $F'$ with $F \dto{} F' \dto{} F''$.\\
\pf In \cite{GW90}.\hfill $\Box$
\end{lemma}
It is more common to use \df{bb} for closed process
expressions only, thereby avoiding the use of the transitions
\plat{\goto{X}}, and to extend the definition to open
process expressions by $$E\bis{b} F \mbox{ iff for all closed process
expressions $G$, } E\{G/X\} \bis{b} F\{G/X\}$$
By Propositions \ref{pr-substitution} and \ref{pr-openbb} below both
approaches yield the same equivalence relation. The way of defining
$\bis{b}$ on open process expressions employed here is a mild
variation of the way weak equivalence was defined in {\sc Milner}
\cite{Mi89a}. It does not carry over to full CCS.
\begin{proposition}{substitution}
$\bis{b} \subseteq \fE \times \fE$ is a bisimulation and an equivalence,
satisfying, for $E,F,G \in \fE$
$$E \bis{b} F \Rightarrow E\{G/X\} \bis{b} F\{G/X\}.$$
\end{proposition}
\pf
The identity relation Id$_\fE$ is a branching bisimulation and if $\cal
R$ and $\cal S$ are branching bisimulations, then so are ${\cal
R}^{-1}$ and ${\cal R} \circ {\cal S} = \{(E,F)\mid \exists G \in \fE
\mbox{ with } (E,G)\in {\cal R} \mbox{ and } (G,F)\in {\cal S}\}$.
Hence $\bis{b}$ is an equivalence.
If ${\cal R}_i$ ($i \in I$) are branching bisimulations, so
is $\bigcup_{i \in I} {\cal R}_i$. Thus $\bis{b}= \bigcup\{ {\cal R}
\mid {\cal R} \mbox{ is a bisimulation} \}$ is a branching bisimulation.
$\{(E\{G/X\},F\{G/X\})\mid E \bis{b} F,~G \in \fE\} \cup {\rm Id}_\fE$
is a bisimulation by Lemma~\ref{lem-substitution} (using $=_\alpha
\subseteq \!\bis{b}\!$).$\Box$
\begin{proposition}{openbb}
If $E\{G/X\} \bis{b} F\{G/X\}$ for all closed process expressions $G$,
then $E \bis{b} F$.
\end{proposition}
\pf As $A$ is nonempty, there is an $a \in A$. It is easy to see
that $a^m \nobis{b} a^n$ for $m \neq n$, where $a^n = aa \cdots a0$
with $n$ $a$'s. Thus, by \pr{regular}, for given $E$
and $F$ it is possible to choose $n \in \IN$ such that $a^{n-1} \nobis{b}
H$ and thus $a^{n-1} \nobis{b} H\{a^{n}/X\}$ for $H \in \fE_E
\cup \fE_F$. By assumption $E\{a^{n}/X\} \bis{b} F\{a^{n}/X\}$.
It suffices to prove that $\{(E',F') \subseteq \fE_E \times \fE_F \mid
E'\{a^{n}/X\} \bis{b} F'\{a^{n}/X\} \}$ is a branching bisimulation,
which is a straightforward application of Lemma~\ref{lem-substitution}.
\qed
The following is a powerful tool for establishing statements $E \bis{b}
F$. It is analogous to {\sc Milner}'s notions of {\em strong bisimulation
up to $\bis{s}$} and {\em weak bisimulation up to $\bis{w}$}. As for
weak bisimulation up to $\bis{w}$, versions of the notion below without
the double arrow in the premises are easily seen to be unsound \cite{Mi90ccs}.
\begin{definition}{upto}
A {\em branching bisimulation up to $\bis{b}$} is a symmetric relation
${\cal R} \subseteq \fE \times \fE$ such that
if $E {\cal R} F$ and $E \dto{} E' \goto{x} E''$ with $E \bis{b} E'$
and $x\neq\tau \vee E' \nobis{b} E''$
then $\exists E'_1,E''_1,F'_1,F''_1,F',F''$ such that
$$\begin{array}{ccccccc}
E &&&{\cal R}&&& F \\
\left\Downarrow\rule{0pt}{15pt}\right. &&&&&&
\left\Downarrow\rule{0pt}{15pt}\right. \\
E' & \bis{b} & E'_1 & {\cal R} & F'_1 & \bis{b} & F' \\
\left\downarrow\rule{0pt}{15pt}\right. \makebox[0pt]{$x$} &&&&&&
\left\downarrow\rule{0pt}{15pt}\right. \makebox[0pt]{$x$} \\
E'' & \bis{b} & E''_1 & {\cal R} & F''_1 & \bis{b} & F'' \\
\end{array}$$
\end{definition}
\begin{proposition}{upto}
If {\cal R} is a branching bisimulation up to $\bis{b}$ and $E {\cal
R} F$, then $E \bis{b} F$.
\end{proposition}
\pf
It suffices to prove that the relation $\bis{b} {\cal R} \bis{b} =
\{(E_0,F_0)\mid \exists E,F: E_0 \bis{b} E {\cal R} F \bis{b} F_0\}$
is a branching bisimulation. So suppose $E_0, E, F$ and $F_0$ are as
indicated, and $E_0 \goto{x} E_0''$. Then either $x=\tau$ and $E_0'' \bis{b}
E$, which completes the proof, or there are $E'$ and $E''$ with $E
\dto{} E' \goto{x} E''$, $E' \bis{b} E_0 \bis{b} E$
and $E'' \bis{b} E_0'' (\nobis{b} E$ if $x=\tau$). In the latter case
apply \df{upto}, and use that $F_0 \bis{b} F \dto{} F'
\goto{x} F''$ implies $x=\tau \wedge F'' \bis{b} F_0$ or $F_0 \dto{}
F_0' \goto{x} F_0''$ with $F' \bis{b} F_0'$ and $F'' \bis{b} F_0''$ by
\df{bb} (and in one case Lemma \ref{lem-stutter} to
find $F_0'$).\qed
Just like weak bisimulation equivalence, branching equivalence is not a
congruence on BCCS$^\omega$. Also the simplest counterexample is the
same: $a \bis{b} \tau a$ but, for $b \neq a$, $a+b \nobis{b} \tau
a+b$. Here, as usual, $a0$ is abbreviated by $a$ and action
prefixing binds stronger than choice. Milner selected weak bisimulation
congruence to be the largest (= coarsest) congruence contained in weak
equivalence, and the same solution is applied here. Just like weak
congruence, branching congruence has a nice characterization, showing
that it is close to the original equivalence.
\begin{definition}{rbb}
Two expressions $E$ and $F$ are {\em rooted branching bisimulation
equivalent} or {\em branching (bisimulation) congruent}---notation $E
\bis{rb} F$---if $\forall x\in A_{\tau} \cup V$:
$$E\goto{x} E' \mbox{ implies } \exists F': F \goto{x} F' \wedge E'\bis{b}F'$$
$$F\goto{x} F' \mbox{ implies } \exists E': E \goto{x} E' \wedge E'\bis{b}F'.$$
\end{definition}
\begin{proposition}{congruence} ({\bf Congruence})
$\bis{rb}$ is an equivalence relation such that
$$\mbox{if } E=F \mbox{ then } aE=aF,~~E+G=F+G,~~G+E=G+F \mbox{ and
}~\mu XE=\mu XF.$$
Moreover it is the coarsest relation with these properties contained in
$\bis{b}$.
\end{proposition}
{\bf Proof:} Similar to the congruence proofs for strong and weak
bisimulation congruence in \cite{Mi90ccs}.
\qed
The following shows that the definition of $\bis{rb}$ for open expressions
yields the same notion as the standard approach based on substitution
of closed terms.
\begin{proposition}{subst-rbb}
Let $E,F \in \fE$. Then $E \bis{b} F$ implies $E\{G/X\} \bis{b}
F\{G/X\}$ for $G \in \fE$, and
if $E\{G/X\} \bis{b} F\{G/X\}$ for closed $G\in \fE$, then $E \bis{b} F$.
\end{proposition}
\pf Straightforward with Lemma~\ref{lem-substitution}, using
Propositions \ref{pr-substitution} and \ref{pr-openbb} and the same
$G$ as before.\qed
{\sc Milner} \cite{Mi90ccs} listed two results that show how close weak
equivalence and congruence are to each other. The first was that for
{\em stable} processes (processes without outgoing $\tau$-transitions)
the equivalence and congruence coincide. This result carries over to
branching bisimulation, as follows immediately from the definitions.
The second result says that in each weak bisimulation equivalence class
there are at most two congruence classes, with representatives $E$ and
$\tau E$ for some $E \in \fE$. This is not true for branching
bisimulation, indicating that branching equivalence and congruence are
less close than weak equivalence and congruence. However, a corollary of
this property does hold, showing that the distance is still
reasonable.
\begin{proposition}{equiv-congr}
$E \bis{b} F ~\Leftrightarrow~ \tau E \bis{rb} \tau F$.\\
\pf Immediate from \df{rbb}.\hfill $\Box$
\end{proposition}
This proposition effectively turns any complete axiomatization for
$\bis{rb}$ into one for $\bis{b}$.
\bsection{The axioms}
The following set of axioms will be proven to be sound and complete for
$\bis{rb}$. The entries below are actually axiom schemes, in metavariables
$E,F,G \in \fE$, $X\in V$ and (in the axiom B) $a \in A_\tau$. This means that
there is an axiom for every choice of $E,F,G,X$ and $a$. The axiom
schemes E1-3 and A1-4 could be replaced by single axioms, by using real
variables $X,Y$ and $Z$ instead of the metavariables $E,F$ and $G$, and
adding the law of substitution: if $E=F$ then $E\{G/X\} = F\{G/X\}$,
which is sound by \pr{subst-rbb}. However, this
would not work for R1-6, since the bound variable X is allowed to
occur in $E,F$ and $G$. The axioms $\mu XE = \mu Y(E\{Y/X\})$
({\em $\alpha$-conversion}) are derivable\pagebreak[2] from R1-6, using Theorem
\ref{th-guarded} and R2.
$$\begin{array}{ll}\label{axioms}
{\rm E1} & E=E \\
{\rm E2} & \mbox{if } E=F \mbox{ then } F=E \\
{\rm E3} & \mbox{if } E=F \mbox{ and } F=G \mbox{ then } E=G \\
{\rm E4} & \mbox{if } E=F \mbox{ then } aE=aF,~~E+G=F+G,~~G+E=G+F,
\mbox{ and }~\mu XE=\mu XF \\
\\
{\rm A0} & E+0 = E \\
{\rm A1} & E+F = F+E \\
{\rm A2} & E+(F+G) = (E+F)+G \\
{\rm A3} & E+E=E \\
\\
{\rm B } & a(\tau(E+F)+E) = a(E+F)~ \mbox{ for } a \in A_\tau \\
\\
{\rm R1} & \mu XE = E \{\mu XE/X\} \\
{\rm R2} & \mbox{if } F=E\{F/X\} \mbox{ then } F=\mu XE, \mbox{ provided $X$
is guarded in $E$} \\
{\rm R3} & \mu X(X+E) = \mu XE \\
{\rm R4} & \mu X(\tau(\tau E+F)+G) = \mu X(\tau (E+F)+G), \mbox{ provided $X$
is unguarded in $E$} \\
{\rm R5} & \mu X(\tau(X+E)+\tau(X+F)+G) = \mu X(\tau(X+E+F)+G) \\
{\rm R6} & \mu X(\tau(X+E)+F) = \mu X(\tau(E+F)+F) \\
\end{array}$$
One writes $T \vdash E=F$, with $T$ a list of axiom names, if the
equation $E=F$ is derivable from the axioms in $T$. Moreover, in this
paper the convention is adopted that the axioms E1-4 and A0-3 are
always in $T$, even if not explicitly listed.
In the next 3 sections I will establish the following completeness
theorems.
\begin{itemize}
\item For $E,F \in \fE^g$: $~E \bis{rb} F ~\Leftrightarrow \mbox{
BR1-2} \vdash E=F$
\item For $E,F \in \fE^f$: $~E \bis{rb} F ~\Leftrightarrow~ {\rm
B} \vdash E=F$
\item For $E,F \in \fE$: $~~E \bis{rb} F ~\Leftrightarrow~{\rm BR} \vdash E=F$
\end{itemize}
The rest of this section will be devoted to the soundness of the axioms.
\\[1.5ex]
{\bf Soundness}: The soundness of E1-4 is established in
\pr{congruence}. As far as R1 concerns, one has
$\mu XE \goto{x} F ~\Leftrightarrow~ E\{\mu XE/X\} \goto{x} F$
from which it follows that $\mu XE \bis{rb} E\{\mu XE/X\}$ (the terms
are even {\em strongly} bisimilar). In the same way the soundness of
A0-4 is established. By inspection of their outgoing transitions, it
follows that $\{(\tau (E+F)+E , E+F)\} \cup {\rm Id}_\fE$ is a branching
bisimulation and hence $a(\tau (E+F)+E) \bis{rb} a(E+F)$.
\begin{proposition}{R2}
If $F\bis{rb}E\{F/X\}$ then $F\bis{rb}\mu XE$, provided $X$ is
guarded in $E$.
\end{proposition}
\pf For $G,H \in \fE$ write $H(G)$ for $H\{G/X\}$. Let $E,F,G \in
\fE$, such that $X$ is guarded in $E$, $F \bis{rb} E(F)$ and
$G \bis{rb} E(G)$. I will show that the symmetric closure of
$\{(H(E(F)),H(E(G)))\mid H \in \fE\}$ is a bisimulation up to
$\bis{b}$. So suppose that $H(E(F)) \dto{} K' \goto{x} K''$ (in this
proof one doesn't even need to assume that $H(E(F)) \bis{b} K'$ and
$x\neq\tau \vee K' \nobis{b} K''$). As $X$ is guarded in $E$ and
hence in $H(E)$, it cannot be that \plat{H(E) \dto{}\goto{X} 0}, by Lemma
\ref{lem-X}. Thus $K'$ and $K''$ are of the form $H'(F)$ and $H''(F)$
by Lemma \ref{lem-substitution}.3, and by Lemma
\ref{lem-substitution}.2 $H(E(G))\dto{} H'''(G) \goto{x} H''''(G)$
with $H''' =_\alpha H'$ and $H'''' =_\alpha H''$. Furthermore, by
\pr{congruence}, $H'(E(F)) \bis{b} H'(F)$, $H'''(G)
\bis{b} H'(E(G))$, $H''(E(F)) \bis{b} H''(F)$ and $H''''(G) \bis{b}
H''(E(G))$. The requirement starting with $H(E(G))$ follows by
symmetry, so the relation is a branching bisimulation up to $\bis{b}$ and by
\pr{upto} $H(E(F)) \bis{b} H(E(G))$ for $H \in \fE$.
Using this, a repeat of the argument above with $K'=H(E(F))$ gives
$H(E(F)) \bis{rb} H(E(G))$, so in particular $E(F) \bis{rb} E(G)$, and
hence $F \bis{rb} G$. Finally take $G=\mu XE$.\hfill $\Box$
\begin{proposition}{R4} $\mu X(\tau(\tau E+F)+G) ~\bis{rb}~ \mu X(\tau
(E+F)+G)$, provided $X$ is unguarded in $E$.
\end{proposition}
\pf By Lemma \ref{lem-X} there are $E_0, \ldots, E_n$ such that
$\tau E+F \goto{\tau} E_0 \goto{\tau} E_1 \goto{\tau} \cdots E_n
\goto{X}$ with $E_0=E$ and $n \in \IN$. Write
$E'_{-1}$ for $\tau E+F$ and $E''_0$ for $E+F$. Then by Lemma
\ref{lem-substitution} $$L \goto{\tau} E'_{-1}\{L/X\}
\goto{\tau} E'_0\{L/X\}\goto{\tau} E'_1\{L/X\} \goto{\tau} \cdots E'_n\{L/X\}
\goto{\tau} E'_{-1}\{L/X\}$$ for certain $E'_i =_\alpha E_i$
($i=0,...,n$) and $$R \goto{\tau} E''_0\{R/X\}\goto{\tau} E''_1\{R/X\}
\goto{\tau} \cdots E''_n\{R/X\} \goto{\tau} E''_{0}\{R/X\}$$ for
certain $E''_j =_\alpha E_j$ ($j=1,...,n$).
Let ${\cal R} \subseteq \fE \times \fE$ be the symmetric closure of
$$\{(H\{L/X\},H'\{R/X\})\mid H \!=_\alpha\! H'\} \cup
\{(E'_i\{L/X\},E''_j\{R/X\})\mid -1\!\leq\! i \!\leq\! n,~0\!\leq\! j
\!\leq\! n\}$$
Then $\cal R$ is a branching bisimulation and $L \bis{rb} R$ by Lemma
\ref{lem-substitution}.\hfill $\Box$
\begin{proposition}{R5}
$\mu X(\tau(X+E)+\tau(X+F)+G) ~\bis{rb}~ \mu X(\tau(X+E+F)+G)$.
\end{proposition}
\pf The closure under symmetry and $\alpha$-recursion of
$\{(H\{L/X\},H\{R/X\})\mid H \in \fE\} \cup$ $$\{(\tau
(X+E)\{L/X\},\tau(X+E+F)\{R/X\}) \cup \{(\tau
(X+F)\{L/X\},\tau(X+E+F)\{R/X\})\}$$
is a branching bisimulation.\qed
In the same way one proves the soundness of R3 and R6.
\begin{proposition}{R3}$\mu X(X+E) ~\bis{rb}~ \mu XE$.\hfill $\Box$
\end{proposition}
\begin{proposition}{R6}
$\mu X(\tau(X+E)+F) ~\bis{rb}~ \mu X(\tau(E+F)+F)$.\hfill $\Box$
\end{proposition}
\begin{corollary}{Soundness}({\bf Soundness})
For $E,F \in \fE$: $~\mbox{BR} \vdash E=F ~\Rightarrow~ E \bis{rb} F$.
\end{corollary}
\bsection{Completeness for guarded process expressions}
Let, for $S=\{E_1, \ldots ,E_n\}$, $\sum S$ be an abbreviation for $E_1 +
\cdots + E_n$. This notation is justified by the axioms A0-3.
\begin{lemma}{hnf} For $E \in \fE^g$, $~{\rm R1} \vdash E = \sum \{
aE' \mid E \goto{a} E' \} + \sum \{ W \mid E \goto{W} 0 \}$.
\end{lemma}
\pf By induction on the number of recursion operators in $E$, not
counting the ones that occur in a subterm $aG$. If this
number is $0$, then $E$ has the form $\sum_{i\in I} a_i E_i + \sum_{j\in
J} W_j$ with $a_i \in A_\tau$ and $W_j \in V$ (the so-called {\em
head normal form}) and the statement holds trivially. Otherwise $E$
has a summand $\mu XF$, which can be replaced by $F\{\mu XF/X\}$ using
R1, yielding $E''$. As $E$ is guarded, $E'$ has less recursion
operators that don't occur in a subterm $aG$, so by induction \
${\rm R1} \vdash E'' = \sum \{aE' \mid E'' \goto{a} E' \} + \sum \{ W
\mid E'' \goto{W} 0 \}$. As $E''\goto{x} E' \Leftrightarrow E \goto{x}
E'$ for $x \in A_\tau \cup V$, the statement follows. \hfill $\Box$
\begin{definition}{satisfaction}
A {\em recursive specification} $S$ is a set of equations $\{X=S_X
\mid X \in V_S \}$ with $V_S \subseteq V$ and $S_X \in \fE$ for $X \in
V_S$. $E \in \fE$ {\em $T$-provably satisfies} the recursive specification $S$
{\em in} the variable $X_0 \in V_S$ if there are expressions $E_X$ for
$X \in V_S$ with $E=E_{X_0}$, such that for $X \in V_S$ $$T \vdash E_X =
S_X\{E_Y /Y\}_{Y \in V_S}.$$
\end{definition}
\begin{definition}{guarded-rs}
Let $S$ be a recursive specification. The relations $\goto{o}
\subseteq V_S \times V_S$ and $\goto{u} \subseteq V_S \times V_S$ are
defined by
\begin{itemize}
\item $X \goto{o} Y$ if $Y$ occurs free in $S_X$
\item $X \goto{u} Y$ if $Y$ occurs free and unguarded in $S_X$
\end{itemize}
Now $S$ is called {\em well-founded} if $\goto{o}$ is well-founded on
$V_S$, and {\em guarded} if $\goto{u}$ is well-founded on $V_S$.
\end{definition}
\begin{proposition}{unique}({\bf Unique solutions})
If $S$ is a finite guarded recursive specification and $X_0 \in V_S$,
then there is an expression $E$ which R1-provably satisfies $S$ in $X_0$.
Moreover if there are two such expressions $E$ and $F$, then ${\rm R2}
\vdash E=F$.
\end{proposition}
\pf In {\sc Milner} \cite{Mi89a}.\hfill $\Box$
\begin{theorem}{crucial}
Let $E_0,F_0\in \fE^g$ with $E_0 \bis{rb} F_0$. Then there is a finite
guarded recursive specification $S$ BR1-provably satisfied in the same
variable $X_0 \in V_S$ by both $E_0$ and $F_0$.
\end{theorem}
\pf Take a fresh set of variables $V_S = \{X_{EF} \mid E \in
\fE_{E_0}, F \in \fE_{F_0}, E \bis{b} F \}$. $X_0 = X_{E_0 F_0}$.
Now for $X_{EF} \in V_S$, $S$ contains the equation
$$X_{EF} = \sum \{ W \mid E \goto{W} 0 \mbox{ and } F
\goto{W} 0\} + \sum \{ aX_{E'F'} \mid E \goto{a} E',~F \goto{a}
F' \mbox{ and } E' \bis{b} F'\}+$$ $$\mbox{\small $\displaystyle \sum
\{ \tau X_{E'F} \mid X_{EF} \neq X_0,~E \goto{\tau} E' \mbox{ and } E'
\bis{b} F\} + \sum \{ \tau X_{EF'} \mid X_{EF} \neq X_0,~F \goto{\tau}
F' \mbox{ and } E \bis{b} F'\}.$}$$
Using that $X_{EF} \goto{u} X_{E'F'}$ iff $S_{X_{EF}}$ has a summand
$\tau X_{E'F'}$, it is easy to show that any infinite $u$-path $X_{EF}
\goto{u} X_{E'F'} \goto{u} \cdots$ implies an infinite $\tau$-path $E
\goto{\tau} E' \goto{\tau} \cdots$ or $F \goto{\tau} F' \goto{\tau}
\cdots$, which cannot exist by Lemma \ref{lem-guarded} since $E_0$ and
$F_0$ are guarded. Hence $S$ is a guarded recursive specification.
Moreover $S$ is finite by \pr{regular}.
It remains to be established that $E_0$ BR1-provably satisfies $S$ in
$X_0$. The same statement for $F_0$ then follows by symmetry.\\[1ex]
For $X_{EF} \in V_S$, let $H_{EF}$ be the expression
$\displaystyle \sum \{ W \mid E \goto{W} 0 \mbox{ and } F \goto{W}
0\} +$ $$+ \sum \{ aE' \mid E \goto{a} E',~F \goto{a} F' \mbox{ and }
E' \bis{b} F'\} + \sum \{ \tau E' \mid X_{EF} \neq X_0,~E \goto{\tau}
E' \mbox{ and } E' \bis{b} F\}$$ and define the expression $G_{EF}$ by
$$G_{EF} = \left\{ \begin{array}{ll}H_{EF} + \tau E & \mbox{if }
X_{EF} \neq X_0 \mbox{ and } \exists F' \mbox{ with } F \goto{\tau}
F' \mbox{ and } E \bis{b} F'\\
E & \mbox{otherwise.} \end{array} \right.$$
It follows from Lemma \ref{lem-hnf} that ${\rm R1} \vdash E = E + H_{EF}$ and
hence ${\rm BR1} \vdash a(H_{EF} + \tau E) = aE$. Thus
\begin{equation}\label{aG=aE}
{\rm BR1} \vdash aG_{EF}=aE~~~\mbox{for } a \in A_{\tau}.
\end{equation}
It suffices to prove that for $X_{EF} \in V_S$
$${\rm BR1} \vdash G_{EF} = \sum \{ W \mid E \goto{W} 0 \mbox{ and } F
\goto{W} 0\} + \sum \{ aG_{E'F'} \mid E \goto{a} E',~F \goto{a}
F' \mbox{ and } E' \bis{b} F'\}+$$ $$\mbox{\small $\displaystyle \sum
\{ \tau G_{E'F} \mid X_{EF} \neq X_0,~E \goto{\tau} E' \mbox{ and } E'
\bis{b} F\} + \sum \{ \tau G_{EF'} \mid X_{EF} \neq X_0,~F \goto{\tau}
F' \mbox{ and } E \bis{b} F'\}.$}$$
By (\ref{aG=aE}) this is equivalent to
\begin{equation}\label{GH}
{\rm BR1} \vdash G_{EF} = H_{EF} + \sum \{\tau E \mid X_{EF} \neq X_0,~F
\goto{\tau} F' \mbox{ and } E \bis{b} F'\}.
\end{equation}
In case $X_{EF} \neq X_0$ and $\exists F'$ with $F
\goto{\tau} F'$ and $E \bis{b} F'$, this follows from the
definition of $G_{EF}$. In case $X_{EF} \neq X_0$ and $\not\!\!\exists F'$
with $F \goto{\tau} F'$ and $E \bis{b} F'$, (\ref{GH}) reduces to
${\rm BR1} \vdash E=H_{EF}$, and by Lemma \ref{lem-hnf} if suffices to
establish, for $x \in A_{\tau} \cup V$, that $$\mbox{ if } E\goto{x} E'
\mbox{ then } \begin{array}{l}x=\tau \mbox{ and } E' \bis{b} F\\
\mbox{or } \exists F': F \goto{x} F' \wedge E' \bis{b} F'. \end{array}$$
But this follows from $E \bis{b} F$, using that if $F \goto{\tau} F_1
\dto{} F''$ with $F'' \bis{b} E \bis{b} F$, then $E \bis{b} F_1$ by
Lemma \ref{lem-stutter}, violating the assumptions.
Finally, in case $X_{EF} = X_0$, (\ref{GH}) also reduces to
${\rm BR1} \vdash E=H_{EF}$, and this time I have to establish, for $x \in
A_{\tau} \cup V$, that $$\mbox{ if } E\goto{x} E' \mbox{ then }
\exists F': F \goto{x} F' \wedge E' \bis{b} F',$$
which follows immediately from $E \bis{rb} F$. \hfill $\Box$
\begin{corollary}{guarded-completeness}({\bf Completeness})
For $E,F \in \fE^g$: $~E \bis{rb} F ~\Leftrightarrow~ \mbox{BR1-2} \vdash E=F$.
\end{corollary}
\bsection{Completeness for finite process expressions}
\begin{theorem}{finite}
Let $E_0,F_0\in \fE^f$ with $E_0 \bis{rb} F_0$. Then there is a finite
well-founded recursive specification $S$ B-provably satisfied in the
same variable $X_0 \in V_S$ by both $E_0$ and $F_0$.
\end{theorem}
\pf The construction of $S$ is exactly as in the proof of Theorem
\ref{th-crucial}.
Using that $X_{EF} \goto{o} X_{E'F'}$ iff $S_{X_{EF}}$ has a summand
$a X_{E'F'}$ with $a \in A_\tau$, it is easy to show that any infinite
$o$-path $X_{EF} \goto{o} X_{E'F'} \goto{o} \cdots$ implies an infinite path $E
\goto{a_1} E' \goto{a_2} \cdots$ or $F \goto{b_1} F' \goto{b_2}
\cdots$, which cannot exist by Lemma \ref{lem-finite} since $E_0$ and
$F_0$ are finite. Hence $S$ is a well-founded recursive specification.
The proof that $S$ is finite and provably satisfies both $E_0$ and
$F_0$ in $X_0$ is exactly as before, except that Lemma \ref{lem-hnf}
is not needed, as recursion-free process expression are already in
head normal form and therefore satisfy $$\vdash E = \sum \{aE' \mid E
\goto{a} E' \} + \sum \{ W \mid E \goto{W} 0 \}$$
without using axiom R1. As this was the only call for this axiom in
the proof of Theorem \ref{th-crucial} it follows that $S$ is
B-provably satisfied in $X_0 \in V_S$ by both $E_0$ and $F_0$.\hfill $\Box$
\begin{proposition}{unique-finite}({\bf Unique solutions})
If $S$ is a finite well-founded recursive specification and $X_0 \in V_S$,
then there is an expression $E$ which provably satisfies $S$ in $X_0$.
Moreover if there are two such expressions $E$ and $F$, then $\vdash E=F$.
\end{proposition}
\pf
% This is a matter of repeatedly substituting $S_Y$ for $Y$ ($Y\in
% V_S$) in the equations of $S$. A detailed proof is omitted due to lack
% of space. It can be found in the technical report version of this paper.
% Note that this proposition does not follow from
% \pr{unique}, as one may not use axioms R1 and R2.
By induction on the number of equations in $S$ I find expressions
$E_X$ for $X \in V_S$, such that $$\vdash E_X = S_X\{E_Y /Y\}_{Y \in V_S}$$
and if there are $F_X \in \fE$ for $X \in V_S$ such that $\vdash F_X =
S_X\{F_Y /Y\}_{Y \in V_S}$ then $\vdash E_X = F_Y$ for $X \in V_S$.
If $S$ has only one equation $X=S_X$ then $X$ does not occur free in
$S_X$ by the well-foundedness of $\goto{o}$. Hence $S_X$ provably
satisfies $S$, and for any other expression $F$ satisfying $S$ one has
$\vdash F = S_X$.
Now suppose that $S$ has more than one equation. By the
well-foundedness of $\goto{o}$ there must be a variable $Z \in V_S$
such that $Y \goto{o} Z$ for no $Y \in V_S$. Obtain $T$ from $S$ by
deleting the equation $Z=S_Z$. By induction there are
$E_X \in \fE$ for $X\in V_T$, such that $\vdash E_X = S_X\{E_Y /Y\}_{Y
\in V_T}$ and if there are $F_X \in \fE$ for $X \in V_T$ such that
$\vdash F_X = S_X\{F_Y /Y\}_{Y \in V_T}$ then $\vdash E_X = F_Y$ for
$X \in V_T$. Let $E_Z = S_X\{E_Y/Y\}_{Y \in V_T}$. Then, for $X \in
V_S$, $$\vdash E_X = S_X\{E_Y /Y\}_{Y \in V_T} = S_X\{E_Y /Y\}_{Y \in
V_S}$$ and if there are $F_X \in \fE$ for $X \in V_S$ such that
$\vdash F_X = S_X\{F_Y /Y\}_{Y \in V_S}$ then $\vdash E_X = F_Y$ for
$X \in V_T$ and hence $\vdash F_Z = S_Z\{F_Y/Y\}_{Y \in V_S} =
S_Z\{F_Y/Y\}_{Y \in V_T} \stackrel{\rm E4}{=} S_Z\{E_Y/Y\}_{Y \in V_T}
= E_Z$.
\hfill $\Box$
\begin{corollary}{finite-completeness}({\bf Completeness})
For $E,F \in \fE^f$: $~E \bis{rb} F ~\Leftrightarrow~ \mbox{B} \vdash
E=F$.
\end{corollary}
\bsection{Completeness for all process expressions}
\begin{theorem}{guarded}
For every $E \in \fE$ there exists a guarded expression $E'$ with
$\mbox{R1,3-6} \vdash E=E'$.
\end{theorem}
\pf It suffices to prove this for expressions of the form $E=\mu XF$.
Following Milner, I prove a stronger result by induction on the
depth of nesting of recursions in $F$, namely
\begin{center}
\begin{tabular}{l}
For every $F \in \fE$, there exists a guarded expression $F'$ for which\\
$\bullet~$ $X$ is guarded in $F'$\\
$\bullet~$ No free unguarded occurrence of any variable in $F'$ lies within
a recursion in $F'$\\
$\bullet~$ $\mbox{R1,3-6} \vdash \mu XF=\mu XF'$.
\end{tabular}
\end{center}
Assume that this property holds for every $G$ whose recursion depth
is less than that of $F$. Then for each recursion $\mu YG$ in $F$ that lies
within no other recursion in $F$, there must be a guarded expression $G'$
such that $Y$ is guarded in $G'$, no free unguarded occurrence of any
variable in $G'$ lies within a recursion in $G'$, and $\mbox{R1,3-6}
\vdash \mu YG=\mu YG'$. These conditions ensure that no free unguarded
occurrence of any variable in $G'\{\mu YG'/Y\}$ lies within a recursion
in this expression.
Let $F_1$ be the result of simultaneously replacing every such
top-level recursion $\mu YG$ in $F$ by $G'\{\mu YG'/Y\}$. Clearly $F_1$
is guarded, $\mbox{R1,3-6} \vdash F=F_1$, and no free unguarded occurrence
of any variable in $F_1$ lies within a recursion in $F_1$. In
converting $F_1$ to $F'$ such that $\mbox{R1,3-6} \vdash \mu XF_1=\mu
XF'$, it remains only to remove all free unguarded occurrences of $X$
from $F_1$, knowing that they do not lie within recursions. Here the
axioms R3-6 are applied.
First any free unguarded occurrence of $X$ that is not in the scope of a
$\tau$ prefixing operator can be removed by R3. Next for any free
unguarded occurrence of $X$ that is in the scope of 2 or more $\tau$'s,
this number can be lowered by application of R4. Applying R4 from left
to right does not change the number of free unguarded occurrences of
$X$, and does not raise the number of $\tau$'s scoping any particular
such occurrence. So after finitely many applications all free unguarded
occurrences of $X$ are in the scope of exactly one $\tau$ operator, and
applying R5 makes that they are all in the scope of the same $\tau$.
Finally by A3 at most one such occurrence remains, and this one is
eliminated by R6.\hfill $\Box$
\begin{corollary}{completeness}
For $E,F \in \fE$: $~E \bis{rb} F ~\Leftrightarrow~ \mbox{BR} \vdash E=F$.
\end{corollary}
\bsection{Concluding remarks}
The notion of branching bisimulation congruence employed here
\begin{list}{$\bullet$}{
\setlength{\itemsep}{3pt}
\setlength{\parsep}{0pt}
\setlength{\topsep}{3pt}}
\item equates livelock and deadlock: $~\mu X(\tau X) = \tau 0$
\item does not equate divergence and livelock: $~\mu X(\tau X +E) \neq
\mu X(\tau X) +E$
\item abstracts from divergence: $~\mu X(\tau X +\tau E) = \tau E$
\item and chooses minimal solutions in case of underspecification: $\mu
XX = 0$,
\end{list}
just as Milner's standard version of weak bisimulation congruence.
As in the case of weak congruence, there are alternative versions of
branching congruence where these choices are made differently
\cite{GW90}. Complete axiomatizations for these notions remain to be
provided. For weak bisimulation, such work has been done in {\sc
Walker} \cite{Wa90}.
For arbitrary cardinals $\kappa$, one could define the language
BCCS$^\kappa$ by allowing sets of expressions as argument of a
choice operator $\sum$, and functions $V_S \rightarrow \fE$ for $V_S
\subseteq V$ as argument of a recursion operator $\mu$, as long as the
size of these sets and functions is less than $\kappa$. Such a language
would represent all and only the behavious with less than $\kappa$
states. In generalizing the completeness theorem for guarded BCCS$^\kappa$
expressions, one has to reformulate most axioms in an obvious way to
deal with the new operators, slightly adapt the proof of Lemma
\ref{lem-hnf} and make sure that there are at least $\kappa$ variables in
order for the first act in the proof of Theorem \ref{th-crucial} to be
possible. But nothing in my proof essentially depends on finiteness,
and the result generalizes smoothly to guarded infinite-state
behaviours. One could even take $V$ to be a proper class and do away
with all cardinality restrictions. Of course these axiomatizations are
not effective, as some axioms have infinitely many premisis.
The case for unguared expressions does not generalize in this way, as
not every unguarded BCCS$^\kappa$ expression is branching congruent
with a guarded one.
By combining the axioms presented here with the complete
axiomatizations for strong bisimulation that allow closed CCS, CSP and
ACP expressions to be converted into head normal form, one obtains
complete axiomatizations for closed terms in the language BCCS$^\omega$
to which the ACCSP operators have been added, provided that they do not
occur in the scope of recursion operators (cf. {\sc Milner} \cite{Mi89a}).
Remarkably, in this setting the axiom B can be simplified to $a\tau X =aX$.
\begin{theorem}{B}
Every closed instance of B is derivable from $a\tau X=aX$.
\end{theorem}
\pf (sketch) $a(bc+cb)+cab = ab \| c = a \tau b \| c =
a(\tau(bc+cb)+c\tau b)+ca\tau b$.
Placing both sides in CSP's synchronous composition with $a(b+c)$
yields $a(b+c) = a (\tau (b + c) + c)$. In this proof $b$ can be
replaced by $\sum_{i \in I} b_i$ and similarly for $c$. Now a parallel
composition with $a(\sum_{i\in I}b_i E_i + \sum_{j\in J}c_j F_j)$, in
which synchronization is required (only) for $a,b_i$ and $c_j$ yields
$$a(\sum_{i\in I}b_i E_i+\sum_{j\in J}c_j F_j) = a (\tau (\sum_{i\in
I}b_i E_i + \sum_{j\in J}c_j F_j) + \sum_{j\in J}c_j F_j).$$
(In fact, one needs to assume here that the $b_i$ and $c_j$ are
pairwise distinct, and do not occur in $E_h$ and $F_k$, but this restriction
can be removed with a relabelling.)\hfill $\Box$ \\[1.5ex]
If one would now require an abstract congruence to satisfy
$a\tau X = aX$, and an interleaving congruence to be a
congruence for all the operators needed above and to satisfy the
equations needed above (which are standard and already satisfied by
strong congruence), and if one agrees that any
finite process is representable by an expression $\sum a_i E_i$, then it
follows that for finite processes branching bisimulation is the finest
abstract interleaving congruence that generalizes $\tau$-less
bisimulation.
% \bibliography{abbreviations,dbase,new}
\begin{thebibliography}{1}
\bibitem{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{BK88}
{\sc J.A. Bergstra \& J.W. Klop} (1988):
\newblock {\em A complete inference system for regular processes with silent moves.}
\newblock In F.R. Drake \& J.K. Truss, editors: {\sl Proceedings Logic Colloquium 1986, {\rm Hull}}, North-Holland, pp. 21--81.
\newblock First appeared as: Report CS-R8420, CWI, Amsterdam, 1984.
\bibitem{vG90a}
{\sc R.J.~van Glabbeek} (1990):
\newblock {\em The linear time -- branching time spectrum.}
\newblock In J.C.M. Baeten \& J.W. Klop, editors: {\sl Proceedings CONCUR 90, {\rm Amsterdam}}, LNCS 458, Springer-Verlag, pp. 278--297.
\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, Munich, Germany.
\newblock Extended abstract in G.X. Ritter, editor: {\sl Information Processing 89}, Proceedings of the IFIP 11th World Computer Congress, San Fransisco, USA 1989, Elsevier Science Publishers B.V. (North-Holland), 1989, pp. 613-618.
\bibitem{Mi84}
{\sc R.~Milner} (1984):
\newblock {\em A complete inference system for a class of regular behaviours.}
\newblock {\sl Journal of Computer and System Sciences} 28, pp. 439--466.
\bibitem{Mi89a}
{\sc R.~Milner} (1989):
\newblock {\em A complete axiomatisation for observational congruence of finite-state behaviours.}
\newblock {\sl Information and Computation} 81, pp. 227--247.
\bibitem{Mi90ccs}
{\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.
\newblock Alternatively see {\it Communication and Concurrency}, Prentice-Hall International, Englewood Cliffs, 1989, of which an earlier version appeared as {\it A Calculus of Communicating Systems}, LNCS 92, Springer-Verlag, 1980.
\bibitem{Wa90}
{\sc D.J. Walker} (1990):
\newblock {\em Bisimulation and divergence.}
\newblock {\sl Information and Computation} 85(2), pp. 202--241.
\end{thebibliography}
\end{document}
- alternative axioms (KFAR) (postponed for next version).