%% Last modified: Nov 14 by Luca
%% Last spell-checked: November 14, 1995, by Luca
\documentstyle[11pt]{article}
\makeatletter
%%% a4.sty --- Aalborg hack
% Set up LaTeX parameters for British A4 paper.
\newdimen\mainfontsize \mainfontsize=1\@ptsize pt
\setlength{\oddsidemargin}{.25 true in} % left margin 1.25 inch
\setlength{\evensidemargin}{.25 true in} % left margin 1.25 inch
\setlength{\textwidth}{14.85 true cm} % 21.2 cm - 2.5*(2.54 cm)
\topskip=\mainfontsize % plain has 10pt, so this is the equivalent
\maxdepth=.4\mainfontsize % plain has 4pt
\@maxdepth=\maxdepth % this has to be set as well (cf. latex.tex)
\setlength{\headheight}{\mainfontsize}
\dimen0=2\mainfontsize
\setlength{\headsep}{\dimen0} % headline gets depth shaved off
\setlength{\topmargin}{\dimen0}
\setlength{\footheight}{\mainfontsize}
\dimen0=2.5\mainfontsize
\setlength{\footskip}{\dimen0}
\setlength{\textheight}{21.34 true cm} % 30cm - 2in - (8.5\mainfontsize pt)
\makeatother
%\input{amssym.def}
%\input{amssym}
%%% Macros
\newcommand{\wild}{\aleph}
%%%%%% yammer %%%%%%%%%%%%%%%
\def\alyammer#1{\b{(A+L: #1 :A+L)}}
\def\ryammer#1{\b{(R: #1 :R)}}
\def\wyammer#1{\b{(W: #1 :W)}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\epsilon}{\varepsilon}
%\input luca
% I cleaned up 10/25/90 -- lots of stuff in misc.tex which used to be in here.
% Commented out the theorem-like environments on May 3 1994 for use
% with llncs.sty
% Uncommented out the theorem-like environments on May 6 1994.
\makeatletter % so we can use it in names, like a style file.
%\newcommand{\yammer}[1]{\marginpar{\framebox{$\oint$}}{\bf \{ #1 \} }}
\newcommand{\mathify}[1]{\ifmmode{#1}\else\mbox{$#1$}\fi}
\def\mathy[[#1]]{\mathify{#1}}
% This is mathify, except that it's easier for emacs to detect its scope.
\def\.#1{\mathify{#1}}
% English things in Latin
\newcommand{\ie}{{\rm i.e.}}
\newcommand{\viz}{{\rm viz.}}
\newcommand{\cf}{{\rm cf.}}
\newcommand{\Eg}{{\rm E.g.}}
\newcommand{\eg}{{\rm e.g.}}
\let\TT=\tt
\newenvironment{idem}{\mbox{}}{\mbox{}}
\newcommand{\subheading}[1]{\vspace{0.2in}{\large #1}\vspace{0.2in}}
\newcommand{\heading}[1]{
{\bf
\begin{center}
\Large #1
\end{center}
\vspace{0.3in}
}}
\newcommand{\bbth}[1]{\mathify{{}^{{{\it#1}}}}}
\newcommand{\th}{\bbth{th}}
%\setlength{\topmargin}{0 in}
%\setlength{\oddsidemargin}{0 in} % distance from left edge of page to text
%\setlength{\textwidth}{6.5 in}
%\setlength{\textheight}{8.2 in}
\newcommand{\Cal}[1]{\mathify{{\cal #1}}}
% From John Mitchell...
\newcommand{\r}[1]{{\rm #1}} % for roman font in math mode
\renewcommand{\b}[1]{{\bf #1}} % bold face
\renewcommand{\t}[1]{{\TT #1}}
\newcommand{\e}[1]{{\em #1\/}}
\newcommand{\scap}[1]{{\sc #1}}
\newcommand{\s}[1]{{\sf #1}}
\newcommand{\ital}[1]{{\it #1}}
\def\boldinmath#1{\mbox{\boldmath{\mathy[[{\bf #1}]]}}}
% I always get confused about style, so:
\newcommand{\sectref}[1]{Section~\ref{#1}}
\newcommand{\thmref}[1]{Theorem~\ref{#1}}
\newcommand{\corref}[1]{Corollary~\ref{#1}}
\newcommand{\defref}[1]{Definition~\ref{#1}}
\newcommand{\factref}[1]{Fact~\ref{#1}}
\newcommand{\lemref}[1]{Lemma~\ref{#1}}
\newcommand{\propref}[1]{Prop.~\ref{#1}}
\newcommand{\figref}[1]{Figure~\ref{#1}}
\newcommand{\chapref}[1]{Chapter~\ref{#1}}
\newcommand{\tableref}[1]{Table~\ref{#1}}
\newcommand{\eqnref}[1]{(\ref{#1})}
\newcommand{\Ruleref}[1]{\scap{(#1)}}
\newcommand{\ruleref}[1]{Rule \ref{#1}}
% for code:
\newcommand{\codeline}[1]{\\ \indent {\TT #1}\\}
\newenvironment{code}{\TT \begin{tabbing}
1234\=1234\=1234\=1234\=1234\=1243\=1234\=1234\=\kill}{\end{tabbing}}
% fixing some greek letters:
\let\phivar=\phi
\let\phi=\varphi
%\newif\ifBBmath \BBmathfalse
%\newif\ifBBsem \BBsemfalse
%\newif\ifBBthesis \BBthesisfalse
%\ifBBmath
% MATH SYMBOLS
\newcommand{\N}{{\bf N}}
\newcommand{\Z}{{\bf Z}}
\newcommand{\B}{{\bf B}}
\newcommand{\nullstring}{\mathify{{\scriptstyle \langle\rangle}}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{informalProposition}[theorem]{Informal Proposition}
\newtheorem{informalDefinition}[theorem]{Informal Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{convention}[theorem]{Convention}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{hope}[theorem]{Hope}
\newtheorem{claim}[theorem]{Claim}
\def\athenasymbol
{\hbadness=10000000 \hfuzz = 10000pt
\hbox{\raise 4pt\hbox to -3.1pt {{$\bigtriangleup$}}
\lower3pt\hbox{{\rm +}}
}}
\newenvironment{proof}{{\bf Proof:}\small}{\mbox{}\unskip~~\hfill$\Box$\medskip}
\newenvironment{remark}{{\bf Remark:}\small}{\mbox{}\medskip}
\newenvironment{example}{\medskip\noindent{\bf Example:}}{\mbox{}\unskip~~\hfill$\Box$\medskip}
\newenvironment{ack}{\medskip\noindent{\bf Acknowledgements:}}{\mbox{}\unskip~~\hfill\medskip}
% Constructors:
% \bigger{\left(}{\right)}{X} puts parens around X that get bigger, roughly,
% with every two nestings. \Bigger gets bigger with every nesting.
\newcommand{\bigger}[3]{\setbox0=\hbox{$#3$}\ht0=1.05\ht0\mathify{#1\box0#2}}
\newcommand{\Bigger}[3]{\setbox0=\hbox{$#3$}\ht0=1.10\ht0\mathify{#1\box0#2}}
%Also we need something to adapt to changing sizes. It's expensive
% so don't use it except in scripts and such.
\def\Biggerch#1#2#3#4#5{{
\setbox0=\hbox{$#1#4$}\ht0=#5\ht0\dp0=#5\dp0\mathify{#2\box0#3}}
}
\def\Biggersty#1#2#3#4{
\mathify{\mathchoice
{\Biggerch{\displaystyle}{#1}{#2}{#3}{#4}}
{\Biggerch{\textstyle}{#1}{#2}{#3}{#4}}
{\Biggerch{\scriptstyle}{#1}{#2}{#3}{#4}}
{\Biggerch{\scriptscriptstyle}{#1}{#2}{#3}{#4}}}
}
\def\.#1{\ifmmode%
\Biggersty{\left(}{\right)}{#1}{1.00}%
\else(#1)\fi}
\def\tuple#1{\bigger{\left\langle}{\right\rangle}{#1}}
\def\set#1{\bigger{\left\{}{\right\}}{#1}}
\def\parens#1{\bigger{\left(}{\right)}{#1}}
\def\abs#1{\bigger{\left|}{\right|}{#1}}
\def\norm#1{\bigger{\left\|}{\right\|}{#1}}
\def\bracket#1{\bigger{\left[}{\right]}{#1}}
\def\brackets#1{\bigger{\left[}{\right]}{#1}}
\def\ceil#1{\bigger{\left\lceil}{\right\rceil}{#1}}
\def\floor#1{\bigger{\left\lfloor}{\right\rfloor}{#1}}
\def\Tuple#1{\Bigger{\left\langle}{\right\rangle}{#1}}
\def\Set#1{\Bigger{\left\{}{\right\}}{#1}}
\def\Parens#1{\Bigger{\left(}{\right)}{#1}}
\def\Abs#1{\Bigger{\left|}{\right|}{#1}}
\def\Norm#1{\Bigger{\left\|}{\right\|}{#1}}
\def\Bracket#1{\Bigger{\left[}{\right]}{#1}}
\def\Brackets#1{\Bigger{\left[}{\right]}{#1}}
\def\Ceil#1{\Bigger{\left\lceil}{\right\rceil}{#1}}
\def\Floor#1{\Bigger{\left\lfloor}{\right\rfloor}{#1}}
\def\tuplesty#1{\Biggersty{\left\langle}{\right\rangle}{#1}{1.05}}
\def\setsty#1{\Biggersty{\left\{}{\right\}}{#1}{1.05}}
\def\parenssty#1{\Biggersty{\left(}{\right)}{#1}{1.05}}
\def\abssty#1{\Biggersty{\left|}{\right|}{#1}{1.05}}
\def\normsty#1{\Biggersty{\left\|}{\right\|}{#1}{1.05}}
\def\bracketsty#1{\Biggersty{\left[}{\right]}{#1}{1.05}}
\def\ceilsty#1{\Biggersty{\left\lceil}{\right\rceil}{#1}{1.05}}
\def\floorsty#1{\Biggersty{\left\lfloor}{\right\rfloor}{#1}{1.05}}
\def\Tuplesty#1{\Biggersty{\left\langle}{\right\rangle}{#1}{1.1}}
\def\Setsty#1{\Biggersty{\left\{}{\right\}}{#1}{1.1}}
\def\Parenssty#1{\Biggersty{\left(}{\right)}{#1}{1.1}}
\def\Abssty#1{\Biggersty{\left|}{\right|}{#1}{1.1}}
\def\Normsty#1{\Biggersty{\left\|}{\right\|}{#1}{1.1}}
\def\Bracketsty#1{\Biggersty{\left[}{\right]}{#1}{1.1}}
\def\Ceilsty#1{\Biggersty{\left\lceil}{\right\rceil}{#1}{1.1}}
\def\Floorsty#1{\Biggersty{\left\lfloor}{\right\rfloor}{#1}{1.1}}
% Better names for things
\newcommand{\Or}{\vee}
\newcommand{\And}{\wedge}
\newcommand{\AND}{\bigwedge}
\newcommand{\OR}{\bigvee}
\newcommand{\andrm}{\mbox{ and }}
\newcommand{\orrm}{\mbox{ or }}
\newcommand{\implies}{\mathrel{\Rightarrow}}
\newcommand{\Implies}{\mathrel{\Rightarrow}}
\newcommand{\IMplies}{\mathrel{\longRightarrow}}
\newcommand{\impliesrm}{\mbox{ implies }}
\newcommand{\Iff}{\mathify{\mathrel{\Leftrightarrow}}}
\newcommand{\iffrm}{\mbox{ iff }}
\newcommand{\ifrm}{\mbox{ if }}
\newcommand{\nin}{\mathrel{\not\in}}
\newcommand{\pos}[1]{\tuplesty{#1}}
\newcommand{\nec}[1]{\bracketsty{#1}}
\newcommand{\bottom}{\mathord{\perp}}
\newcommand{\sle}{\mathrel{\sqsubseteq}}
\newcommand{\slt}{\mathrel{\sqsubset}}
\newcommand{\sge}{\mathrel{\sqsupseteq}}
\newcommand{\sgt}{\mathrel{\sqsupset}}
\newcommand{\nsle}{\mathrel{\not\sqsubseteq}}
\newcommand{\Union}{\mathop{\bigcup}}
\newcommand{\union}{\mathbin{\cup}}
\newcommand{\intersect}{\mathbin{\cap}}
\newcommand{\intersection}{\intersect}
\newcommand{\Intersect}{\mathop{\bigcap}}
\newcommand{\Intersection}{\mathop{\bigcap}}
\def\nintersect{\mathrel{\pitchfork}}
\newcommand{\setplus}{\mathop{\mbox{\c{+}}}}
\newcommand{\seq}[2]{\mathify{#1_{1},\ldots, #1_{#2}}}
\newcommand{\seqij}[3]{\mathify{#1_{#2},\ldots, #1_{#3}}}
\newcommand{\comp}{\circ}
\newcommand{\casedef}[1]{
\left\{\begin{array}{ll} #1
\end{array}\right.
}
% use \cases{}, which is similar but TeX and second component is not in
% mathmode.
\newcommand{\token}[1]{\mbox{{\sf #1}}}
\def\subsetne{\subsetneq}
\let\oldemptyset=\emptyset
%\renewcommand{\emptyset}{\mathify{\varnothing}}
\newcommand{\nullset}{\emptyset}
\newcommand{\notexists}{\nexists}
%% Assorted LaTeX symbol glomming stuff.
\def\StackArray#1{\begin{array}{c} #1 \end{array}}
% lousy TeX hack to get two symbols on top of each other.
% lousy in part because it ignores display style.
\def\clap#1#2{
{
\setbox0=\hbox{\mathify{#1}}
\setbox1=\hbox{\mathify{#2}}
\ifdim\wd0>\wd1
\setbox2=\box0
\setbox0=\box1
\setbox1=\box2
\fi
% box 1 is now the longer
\dimen0=\wd1
\advance\dimen0 by -\wd0
\divide\dimen0 by 2
\dimen1=-\wd0
\advance\dimen1 by -\dimen0
\hskip\dimen0\box0\hskip \dimen1
\box1
}
}
% slightly smarter version
\def\clapsty#1#2{
\mathify{\mathchoice
{\clap{\displaystyle #1}{\displaystyle #2}}
{\clap{\textstyle #1}{\textstyle #2}}
{\clap{\scriptstyle #1}{\scriptstyle #2}}
{\clap{\scriptscriptstyle #1}{\scriptscriptstyle #2}}
}}
% \fi %BBmath
% \ifBBsem
% CCS/CSP stuff -- semantics
\newcommand{\mv}[1]{\mathrel{\stackrel{#1}{\rightarrow}}}
\newcommand{\mvt}[1]{\mathrel{\stackrel{#1}{\Rightarrow}}}
\newcommand{\nv}[1]{\mathrel{\stackrel{#1}{\not\rightarrow}}}
\newcommand{\nvt}[1]{\mathrel{\stackrel{#1}{\not\Rightarrow}}}
% CCS/CSP language constructs
\newcommand{\fix}[2]{\mathify{\r{rec} \left[#1 \Leftarrow #2\right]}}
\def\rec#1.#2{\fix{#1}{#2}}
\newcommand{\nil}{\b{0}}
%
\def\bisim{\mathrel{\underline{\leftrightarrow}}}
\def\wbisim{\mathrel{\underline{\Leftrightarrow}}}
\def\nbisim{\mathrel{\underline{\nleftrightarrow}}}
\def\nwbisim{\mathrel{\underline{\nLeftrightarrow}}}
\newcommand{\sat}{\mathrel{\models}}
\newcommand{\nsat}{\mathrel{\not\models}}
\newcommand{\cant}[1]{\mathify{\r{Can\mbox{'}t}(#1)}}
% Ready simulation
\def\mathbox#1{\hbox{$#1$}}
\def\rsap{\mathrel{\lower4pt\mathbox{\stackrel{\textstyle\sqsubset}{
\raise1pt\mathbox{\scriptstyle\rightharpoondown}}}}}
\def\rsge{\mathrel{\lower4pt\mathbox{\stackrel{\textstyle\sqsupset}{
\raise1pt\mathbox{\scriptstyle\leftharpoondown}}}}}
\newcommand{\rs}{\mathrel{\rightleftharpoons}}
% \let is a TeX command which assigns the current meaning of a symbol.
\def\rseq{\rs}
\newif\ifttordinaire\ttordinairefalse
\def\ttt{\rlap{\rm t}\kern .5ex{\rm t}}
\renewcommand{\tt}{\ifttordinaire\TT\else\ifmmode\ttt\else\TT\fi\fi}
\newcommand{\ff}{\rlap{\rm f}\kern .5ex{\rm f}}
\newcommand{\mean}[1]{\mathify{\left[ \! \left[ #1 \right]\! \right]}}
\newcommand{\proves}{\vdash}
% Denotational Semantics stuff
%\renewcommand{\sup}{\mathify{\sqcup}}
\renewcommand{\inf}{\mathify{\sqcap}}
\newcommand{\Sup}{\mathify{\bigsqcup}}
\newcommand{\SUP}{\mathify{\bigsqcup}}
\def\bigsqcap{\prod}
\def\Inf{\mathy[[\bigsqcap]]}
\def\INF{\mathy[[\bigsqcap]]}
% Syntactic Rules
\def\aswellas{,\quad}
\newcommand{\Rule}[2]
{\[
\begin{array}{c}
\StackArray{#1} \\\hline \StackArray{#2}
\end{array}
\]
}
\newcommand{\inlinerule}[2]{
\mathify{ #1 \mathrel{/\!-} #2}
}
\newcommand{\RuleLab}[3]{
\begin{equation}
\label{#3}
\begin{array}{c}
#1 \\\hline #2
\end{array}
\end{equation}
}
\newcommand{\RuleName}[3]{
\noindent
\begin{equation}
\label{#3}
\begin{array}{lc}
\b{(#3)} &
\begin{array}{c}
\StackArray{#1} \\\hline \StackArray{#2}
\end{array}
\end{array}
\end{equation}
}
\newcommand{\nestrule}[2]{\begin{array}{c}#1\\\hline#2\end{array}}
\newcommand{\TwoRules}[4]{
\begin{displaymath}
\begin{array}{c}
#1 \\\hline
#2
\end{array}
\qquad
\begin{array}{c}
#3 \\\hline
#4
\end{array}
\end{displaymath}
}
\newcommand{\TwoRulesLab}[5]{
\begin{displaymath}
\begin{array}{c}
#1 \\\hline
#2
\end{array}
\qquad
\begin{array}{c}
#3 \\\hline
#4
\end{array}
\label{#5}
\end{displaymath}
}
\newcommand{\ThreeRules}[6]{
\begin{displaymath}
\begin{array}{c}
#1 \\\hline
#2
\end{array}
\qquad
\begin{array}{c}
#3 \\\hline
#4
\end{array}
\qquad
\begin{array}{c}
#5 \\\hline
#6
\end{array}
\end{displaymath}
}
\newcommand{\ThreeRulesLab}[7]{
\begin{displaymath}
\begin{array}{c}
#1 \\\hline
#2
\end{array}
\qquad
\begin{array}{c}
#3 \\\hline
#4
\end{array}
\qquad
\begin{array}{c}
#5 \\\hline
#6
\end{array}
\end{displaymath}
\label{#7}
}
\newcommand{\FourRules}[8]{
\begin{displaymath}
\begin{array}{c}
#1 \\\hline
#2
\end{array}
\qquad
\begin{array}{c}
#3 \\\hline
#4
\end{array}
\qquad
\begin{array}{c}
#5 \\\hline
#6
\end{array}
\qquad
\begin{array}{c}
#7 \\\hline
#8
\end{array}
\end{displaymath}
}
\newcommand{\FourRulesLab}[9]{
\begin{displaymath}
\begin{array}{c}
#1 \\\hline
#2
\end{array}
\qquad
\begin{array}{c}
#3 \\\hline
#4
\end{array}
\qquad
\begin{array}{c}
#5 \\\hline
#6
\end{array}
\qquad
\begin{array}{c}
#7 \\\hline
#8
\end{array}
\end{displaymath}
\label{#9}
}
% Kinds of Reduction
\newcommand{\goesto}{\mathrel{\rightarrow}}
\iffalse %03/05/1994
\newcommand{\getsto}{\mathrel{\twoheadrightarrow}}
\fi %03/05/1994
\newcommand{\notgetsto}{\mathify{\mathrel{\not\twoheadrightarrow}}}
\newcommand{\stopsat}{\mathrel{\looparrowright}}
% Combinators
\renewcommand{\S}{{\bf S}}
\newcommand{\K}{{\bf K}}
\newcommand{\Y}{{\bf Y}}
% Metamath
\newcommand{\ite}[3]{\mbox{if } #1 \mbox{ then } #2 \mbox{ else } #3 }
\newcommand{\FV}{\r{FV}}
\newcommand{\lam}[2]{\mathify{\lambda #1 . #2}}
% BNF Grammar:
\newcommand{\bnfIS}{::==}
\newcommand{\bnfOR}{\,|\,}
% Standard example of ready similar but not bisimilar processes:
\def\Prsnbs{\mathify{P_{\star}}}
\def\Qrsnbs{\mathify{Q_{\star}}}
% Synchronization tree isomorphism
\newcommand{\Act}{{\sf Act}}
\newcommand{\Var}{\s{Var}}
\newcommand{\cisim}{\mathrel{\mbox{\mathify{\clap{\circ}{\bisim}}}}}
\newcommand{\hoare}[3]{\mathify{\Set{{#1}}#2\Set{{#3}}}}
% Indexing commands:
% Put something in the text and the index both:
\def\ix#1{#1\index{#1}}
% ... and italicize it
\def\eix#1{\e{\ix{#1}}}
% hacking notes in bibliographies
\def\ui/{\"\i} % i-umlaut
\def\naive{na{\"\i}ve}
\def\Quantify#1#2{\mathify{#1 #2 \b{.}\,}}
\def\Forall#1.{\Quantify{\forall}{#1}}
\def\Exists#1.{\Quantify{\exists}{#1}}
\def\Nexists#1.{\Quantify{\nexists}{#1}}
\makeatother % undo @=wierd
\def\suchthat{\r{s.t.}}
\def\xor{\mathbin{\oplus}}
\def\leftmerge{\mathbin{\clap{|}{\sf L}}}
\def\WORD#1#2{\mathy[[\r{#1}\parens{#2}]]}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}} % openface letter
\newcommand{\Nat}{\dl{N}} % natural numbers
\newcommand{\Der}[1]{\mbox{\sf Der}(#1)}
\newcommand{\Derdef}[1]{\mbox{\em {\sf Der}}(#1)}
\newcommand{\coppia}[2]{\langle #1 , #2 \rangle}
\newcommand{\Rel}[1]{\mathrel{\cal #1}} % The argument must be a capital letter
\newcommand{\Bin}[1]{\mbox{\sf Rel}(#1)}
\newcommand{\Bindef}[1]{\mbox{\em {\sf Rel}}(#1)}
\newcommand{\nildef}{\mbox{\em $\nil$}}
\renewcommand{\Var}{\mbox{\sf Var}}
\newcommand{\casesdef}[4]{% Cases definition
\left\{ \begin{array}{ll}
#1 & #2 \\
#3 & #4
\end{array} \right.}
\newtheorem{notation}[theorem]{Notation}
%\newtheorem{convention}[theorem]{Convention}
\newenvironment{esempio}{\medskip \noindent{\bf Example:}}{\quad\medskip}
%\def\peq{\mathrel{\doteq}}
\def\peq{=}
\def\syneq{\equiv}
%\deq : equal by definition
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}
\newcommand{\der}[1]{\mbox{\sf der}\parens{#1}}
\newcommand{\derdef}[1]{\mbox{\em {\sf der}}\parens{#1}}
\newcommand{\Vardef}{\mbox{\em $\Var$}}
%%% Paper specific macros
\newcommand{\LMPA}{\mbox{\sc BCCS}^{\scriptstyle p*}(A_\tau)}
\newcommand{\MPA}{\mbox{\sc T(BCCS)}^{\scriptstyle p*}(A_\tau)}
%\newcommand{\MPAdef}{\mbox{\em T(BCCS)}^{\scriptstyle p*}(A_\tau)}
%\newcommand{\OMPA}{\mbox{{$\Bbb T$}(BCCS)}^{\scriptstyle p*}(A_\tau)}
%\newcommand{\OMPAdef}{\mbox{\em $\Bbb T$(BCCS)}^{\scriptstyle p*}(A_\tau)}
\newcommand{\OpenT}{
\setlength{\unitlength}{1ex}
\begin{picture}(1.25,1.45)
\put(0.4,0){\line(0,1){1.45}}
\put(0.85,0){\line(0,1){1.45}}
\put(-0.1,1.5){\line(1,0){1.45}}
\put(0,1.45){\line(1,0){1.25}}
\put(0.4,0){\line(1,0){0.45}}
\end{picture}}
\newcommand{\OMPA}{\mbox{$\OpenT$(BCCS)}^{\scriptstyle p*}(A_\tau)}
\newcommand{\OMPAdef}{\mbox{\em $\OpenT$(BCCS)}^{\scriptstyle p*}(A_\tau)}
\newcommand{\LMPAdef}{\mbox{\em BCCS}^{\scriptstyle p*}(A_\tau)}
\newcommand{\bis}[2]{ \; % bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}^{#2}\,}
\newcommand{\nobis}[2]{\mbox{$\,\not\hspace{-2.5pt} % no bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}^{#2}\,$}}
\newcommand{\obseq}{\bis{w}{}} %% weak eq.
\newcommand{\obscong}{\bis{w}{c}} %% weak cong.
\newcommand{\braeq}{\bis{b}{}} %% branching eq.
\newcommand{\bracong}{\bis{b}{c}} %% branching cong.
\newcommand{\deleq}{\bis{d}{}} %% delay eq.
\newcommand{\delcong}{\bis{d}{c}} %% delay cong.
\newcommand{\etaeq}{\bis{\eta}{}}
\newcommand{\etacong}{\bis{\eta}{c}}
\newcommand{\ACeq}{=_{\mbox{\tiny\rm AC}}}
%%% End of paper specific macros
\begin{document}
\title{Axiomatizing Prefix Iteration
with Silent Steps}
\author{Luca Aceto\thanks{Department of Mathematics and Computer Science,
Aalborg University, Fr.~Bajersvej 7E,
9220 Aalborg \O, Denmark. On leave from the
School of Cognitive and Computing Sciences,
University of Sussex, Brighton BN1 9QH, UK.
Partially supported by HCM project {\sc express}.
Email: {\tt luca@iesd.auc.dk}.} \\
{\small
{\bf BRICS},
% \footnote{Basic Research in Computer Science,
% Centre of the Danish National Research Foundation.},
Aalborg University
} \\[3mm]
Rob van Glabbeek\thanks{Computer Science Department,
Stanford University, Stanford,
CA 94305, USA.
Partially supported by ONR
under grant number N00014-92-J-1974.
Email: {\tt rvg@cs.stanford.edu}.} \\
{\small Stanford University }
\and Wan Fokkink\thanks{Utrecht University, Department of Philosophy,
Heidelberglaan 8, 3584 CS Utrecht,
The Netherlands.
Email: {\tt fokkink@phil.ruu.nl}.} \\
{\small Utrecht University} \\[3mm]
Anna Ing\'{o}lfsd\'{o}ttir\thanks{
Department of Mathematics and Computer Science,
Aalborg University, Fr.~Bajersvej 7E,
9220 Aalborg \O, Denmark.
% Partially supported by a grant from the
% Danish Research Council.
Email: {\tt annai@iesd.auc.dk}.} \\
{\small {\bf BRICS}, Aalborg University}
}
\date{}
\maketitle
\begin{abstract}
Prefix iteration is a variation on the original binary version of the Kleene
star operation $P^*Q$, obtained by restricting the first argument to be an
atomic action. The interaction of prefix iteration with silent steps is
studied in the setting of Milner's basic CCS. Complete equational
axiomatizations are given for four notions of behavioural congruence over
basic CCS with prefix iteration, viz.~branching congruence, $\eta$-congruence,
delay congruence and weak congruence. The completeness proofs for
$\eta$-, delay, and weak congruence are obtained %as corollaries of
by reduction to the completeness theorem for branching congruence. It is
also argued that the use of
the completeness result for branching congruence in obtaining the
completeness result for weak congruence leads to a considerable
simplification with respect to the only direct proof presented in the
literature. The preliminaries and the completeness proofs focus on
open terms, {\ie}, terms that may contain process variables.
As a byproduct, the $\omega$-completeness of the axiomatizations is
obtained as well as their completeness for closed terms.
%Using a technique due to Groote, it is also shown that all of the proposed
%axiomatizations are $\omega$-complete, {\ie}, complete for equality of open
%terms.
\medskip
\noindent
{\sc AMS Subject Classification (1991):} 68Q10, 68Q40, 68Q55.
\noindent
{\sc CR Subject Classification (1991):} D.3.1, F.1.2, F.3.2.
\noindent
{\sc Keywords and Phrases:} Concurrency, process algebra, basic CCS,
prefix iteration, branching bisimulation,
$\eta$-bisimulation, delay bisimulation, weak bisimulation,
equational logic, complete axiomatizations.
\end{abstract}
%%%% The paper starts here
\section{Introduction}\label{Sect:intro}
The research literature on process theory has recently witnessed a
resurgence of interest in the study of Kleene star-like operations
(cf., {\eg}, the papers
\cite{BBP94,FZ94,Fok94,DL94,Sew94,CDL95,Fok95,AI95,AG95}).
Some of these studies, notably \cite{BBP94}, have investigated the expressive
power of variations on standard process description languages in which infinite
behaviours are defined by means of Kleene's star operation
\cite{Kleene56,CEW58} rather than by means of systems of recursion
equations. Some others (see, {\eg}, \cite{FZ94,Sew94,Fok94,AG95})
have studied the possibility of giving finite equational axiomatizations
of bisimulation-like equivalences \cite{Pa81,Mi89} over simple process
algebras that include variations on Kleene's star operation. De Nicola and his
co-workers have instead focused on the study of tree-based models for
what they call ``nondeterministic Kleene algebras'', and on the proof
systems these models support to reason about regular expressions and
more expressive languages built on top of those; see, {\eg},
\cite{DL94,CDL95} for details on this line of research.
This paper aims at giving a contribution to the study of complete
equational axiomatizations for Kleene star-like operations from the point
of view of process theory. Our starting point is the work presented in
\cite{Fok94}. In that reference, a {\sl finite}, complete equational
axiomatization of strong bisimulation equivalence has been given for $\MPA$,
{\ie}, the language of closed terms obtained by extending the fragment of
Milner's CCS \cite{Mi89} containing the basic operations needed to express
finite synchronization trees with prefix iteration.
Prefix iteration is a variation on the original binary
version of the Kleene star operation $P^*Q$ \cite{Kleene56} obtained by
restricting the first argument to be an atomic action. Intuitively, at any
time the process term $a^*P$ can decide to perform action $a$ and evolve
to itself, or an action from $P$, by which it exits the $a$-loop. The
behaviour of $a^*P$ is captured very clearly by the rules that give its
Plotkin-style structural operational semantics:
\TwoRules{}{a^*P \mv{a} a^*P}
{P \mv{b} P'}{a^*P \mv{b} P'}
Equationally, as shown in \cite{Fok94}, such an operation can be completely
characterized by the following two natural laws:
\begin{eqnarray*}
a. (a^*x) + x & = & a^*x\\
a^*(a^*x) & = & a^*x
\end{eqnarray*}
The reader familiar with Hennessy's work on complete axiomatizations
for the delay operation of Milner's SCCS \cite{He81,He84} will have noticed
the similarity between the above laws and those presented in \cite{He81} (see
also \cite[Page 40]{ABV94}). This is not surprising as such a delay operation
is an instance of the prefix iteration construct.
\subsection{Results}
In this paper, we extend the results in \cite{Fok94}
to a setting with the unobservable action $\tau$.
More precisely, we consider four versions of bisimulation equivalence
that, to different degrees, abstract away from the internal evolution of
processes (viz.~delay equivalence \cite{Mi81}, weak equivalence \cite{Mi89},
$\eta$-equivalence \cite{BG87} and branching equivalence
\cite{GW89}), and provide complete equational axiomatizations for each of
the congruences they induce over the language $\OMPA$ of {\sl open} terms
over the signature of $\MPA$.
% by giving a complete
% equational axiomatization of Milner's weak congruence \cite{Mi89}
% over $\MPA$.
The axiomatizations we present are obtained by extending the axiom system
from \cite{Fok94} with the relevant $\tau$-laws known from the literature for
each of the congruences we consider (cf.~\cite{GW90} for a discussion of these
laws), and with collections of laws that
describe the interplay between the silent nature of $\tau$ and prefix
iteration. For instance, the axiomatization of weak congruence
uses Milner's well-known $\tau$-laws \cite{Mi89} and the following
axioms describing the interaction of prefix iteration with the silent action
$\tau$:
\begin{eqnarray*}
\tau^* x & = & \tau . x \\
\tau . (a^* x) & = & a^* (\tau .a^* x) \\
a^* (x + \tau . y) & = & a^*(x + \tau . y + a.y) \enspace .
\end{eqnarray*}
The first of these equations was introduced in \cite{BBP94} under the name of
{\sl Fair Iteration Rule}, and expresses a fundamental property of weak
congruence, namely the abstraction from $\tau$-loops, that underlies the
soundness of {\sl Koomen's Fair Abstraction
Rule} \cite{BBK87a}. The other two equations are from \cite{AI95},
%, to the best of our knowledge, new.
and describe a rather subtle interplay between prefix iteration and the
silent action $\tau$.
%, and will play a crucial role in the proof of our completeness theorem.
The completeness results for weak and branching congruence were
first proven in \cite{AI95} and \cite{Fok95}, respectively. However,
the proofs of these results
presented in this paper are new, and we consider them to be an improvement
on the original ones. In particular, unlike the one given in \cite{Fok95},
the proof for branching congruence does
not rely on the completeness result for strong bisimulation presented in
\cite{Fok94}, and that for weak congruence is obtained by a simple
and natural reduction to the completeness result for branching congruence.
Perhaps surprisingly, the proof for weak congruence presented here
is considerably simpler then the one given in \cite{AI95} which uses only
properties of weak congruence.
All the authors' attempts to obtain a direct proof of the completeness
theorem for weak congruence which is simpler than the one presented
in \cite{AI95} have been to no avail.
The axiomatizations of $\eta$-congruence and delay
congruence are also given by reduction to the one for branching bisimulation,
and are, to the best of our knowledge, new.
All the axiomatizations we present are {\sl finite}, if so is the set of
observable actions, and irredundant.
Another notable feature of the proofs of the completeness theorems we
present is that, unlike those in \cite{AI95,Fok95}, they apply to open
terms directly, and thus yield the $\omega$-completeness of the axiomatizations
as well as their completeness for closed terms.
Following \cite{Mi89a,vG93}, this is achieved
by defining a structural operational semantics and notions of bisimulations
directly on open terms. For all the notions of bisimulation equivalence so
defined for open terms in the language $\OMPA$, we prove that
two terms are equivalent iff all their closed instantiations are.
This ensures that our definitions are in agreement with the standard ones
in the literature on process theory.
The $\omega$-completeness of the axiomatizations for branching, $\eta$-
and delay congruence are all new. The axiomatization for weak congruence
was first shown to be $\omega$-complete in \cite{AI95} in the presence
of a denumerable set of observable actions.
%, under the
%assumption that the set of observable actions were countably infinite.
Our result in this paper sharpens the one in the aforementioned reference
in that, like the ones for branching, $\eta$- and delay congruence, it only
requires that the set of observable actions be non-empty.
\subsection{Outline of the paper}
%\alyammer{Of course the outline of the paper has to be modified.}
The paper is organized as follows. Section~\ref{Sect:MPA-syntax} introduces
the language of basic CCS with prefix iteration, $\OMPA$, and its
operational semantics. In that section we also give the definition of
branching, $\eta$-, delay and weak congruence over open terms, and show that
two open terms are related by any of those congruences iff all their closed
instantiations are. Section 2 concludes with a study of several properties of
the congruence relations we study that will be used in the remainder of the
paper. The axiom systems that will
be shown to completely characterize the aforementioned congruences over
$\OMPA$ are analyzed in Section~\ref{Sect:axiomatization}.
Detailed proofs of the completeness of our axiom
systems with respect to the relevant congruences over $\OMPA$ are
presented in Section~\ref{Sect:completeness}.
%is entirely devoted to detailed proofs of the completeness of our axiom
%systems with respect to the relevant congruences over $\OMPA$.
The paper concludes with a brief comparison between the proof of completeness
for weak congruence given in \cite{AI95} and the one offered in this paper.
\section{Basic CCS with Prefix Iteration}\label{Sect:MPA-syntax}
We assume a non-empty, countable set $A$ of observable actions not containing
the distinguished symbol $\tau$. Following Milner \cite{Mi89}, the symbol
$\tau$ will be used to denote an internal, unobservable action of a system.
We define $A_\tau \deq A \cup \set{\tau}$, and use $a,b$ to range
over $A$ and $\alpha,\beta,\gamma$ to range over $A_\tau$.
We also assume a countably infinite set of process variables $\Var$, ranged
over by $x,y,z$, that is disjoint from $A_\tau$. The meta-variable
$\xi$ will stand for a typical member of the set $A_\tau \cup \Var$.
The language of basic CCS with prefix iteration, denoted by
$\mbox{BCCS}^{\scriptstyle p*}(A_\tau)$, is given by the following BNF grammar:
\[
P :: = x \mid 0 \mid \alpha . P \mid P + P \mid \alpha^*P
\]
where $x\in\Var$ and $\alpha \in A_\tau$. The set of (open) terms over
$\mbox{BCCS}^{\scriptstyle p*}(A_\tau)$ is denoted by $\OMPA$, and the
set of closed terms, {\ie}, terms that do not contain occurrences of
process variables, by $\MPA$. We shall use $P,Q,R,S,T$
%(possibly subscripted and/or superscripted)
to range over $\OMPA$.
In writing terms over the above syntax, we shall always
assume that the operations $\alpha^*$ and $\alpha.\_$ bind stronger
than $+$. We shall use the symbol $\equiv$ to stand for syntactic
equality of terms. The set of process variables occurring in a term
$P$ will be written $\Var(P)$.
A (closed) substitution is a mapping from process variables to (closed)
terms over $\LMPA$. For every term $P$ and (closed) substitution $\sigma$,
the (closed) term obtained by replacing every occurrence of a variable
$x$ in $P$ with the (closed) term $\sigma(x)$ will be written $P\sigma$.
%We write $\sigma[x \mapsto P]$ for the substitution mapping the variable
%$x$ to the term $P$, and agreeing with $\sigma$ on all the other variables.
We shall use $[x \mapsto P]$ to stand for the substitution mapping $x$ to
$P$, and acting like the identity on all the other variables.
The operational semantics for the language $\LMPA$
is given by the labelled transition system \cite{Ke76,Pl81}
\[
\parens{ \OMPA , \set{ \mv{\xi} \mid \xi\in A_\tau \cup \Var} }
\]
where the transition
relations $\mv{\xi}$ are the least subsets of $\OMPA \times \OMPA$
satisfying the rules in Fig.~\ref{Fig:action-rules}. Intuitively,
a transition $P \mv{\alpha} Q$ ($\alpha\in A_\tau$) means that the system
represented by the term $P$ can perform the action $\alpha$, thereby evolving
into $Q$, whereas $P \mv{x} P'$ means that the initial behaviour of $P$
may depend on the term that is substituted for the process variable $x$.
It is not hard to see that if $P\mv{x} P'$ then $P'\equiv x$.
\begin{figure}[htb]
\FourRules{}{x \mv{x} x}
{}{\alpha . P \mv{\alpha} P}
{P \mv{\xi} P'}{P + Q \mv{\xi} P'}
{Q \mv{\xi} Q'}{P + Q \mv{\xi} Q'}
\TwoRules{}{\alpha^*P \mv{\alpha} \alpha^*P}
{P \mv{\xi} P'}{\alpha^*P \mv{\xi} P'}
\caption{\label{Fig:action-rules}Transition rules}
% for $\mbox{$\OpenT$(BCCS)}^{\scriptstyle p*}(A_\tau)$}
\end{figure}
The derived transition relations $\mvt{\epsilon}$ and $\mvt{\xi}$
($\xi\in A_\tau \cup \Var$)
are defined in the standard way as follows:
$\left\{ \begin{array}{@{}l@{}}
\mvt{\epsilon} \mbox{ is the reflexive, transitive closure of $\mv{\tau}$,} \\
P \mvt{\xi} Q ~~ \mbox{iff} ~~ \exists P_1,P_2:~ P \mvt{\epsilon}
P_1 \mv{\xi} P_2 \mvt{\epsilon} Q \enspace .
\end{array} \right.$
\begin{definition}
The set $\derdef{P}$ of {\em derivatives} of $P$
is the least set containing $P$ that is closed under action-transitions.
Formally, $\derdef{P}$ is the least set satisfying:
\begin{enumerate}
\item $P \in\derdef{P}$;
\item if $Q \in\derdef{P}$ and $Q \mv{\alpha} Q'$ for some $\alpha\in A_\tau$,
then $Q'\in\derdef{P}$.
\end{enumerate}
\end{definition}
The following basic fact can be easily shown by structural induction on terms:
\begin{fact}\label{Fact:finite-state}
For every $P\in\OMPAdef$, the set of derivatives of $P$ is finite.
\end{fact}
A fundamental semantic equivalence in the study of reactive systems is
{\sl bisimulation equivalence} \cite{Pa81,Mi89}. In this study, we shall
consider four versions of this notion which, to different degrees, abstract
away from invisible actions, viz.~branching equivalence \cite{GW89},
$\eta$-equivalence \cite{BG87}, delay equivalence \cite{Mi81} and
weak equivalence \cite{Mi89}.
These we now proceed to define for the sake of completeness. The interested
reader is referred to the aforementioned references and to
\cite{GW90,Mi89a,vG93} for discussion and motivation.
\begin{definition}[Branching Equivalence]
\label{Def:branch-bisim}
A binary relation $\Rel{B}$ over $\OMPAdef$ is a
{\em branching bisimulation},
or {\em $b$-bisimulation} for short, iff it is symmetric and,
whenever $P \Rel{B} Q$, for all $\xi\in A_\tau \cup
\Vardef$,
\begin{description}
\item if $P \mv{\xi} P'$ then
\begin{itemize}
\item $\xi = \tau$ and $P' \Rel{B} Q$, or
\item $Q \mvt{\epsilon} Q_1 \mv{\xi} Q_2 \mvt{\epsilon} Q'$
for some $Q_1, Q_2, Q'$
such that $P \Rel{B} Q_1$, $P' \Rel{B} Q_2$ and $P' \Rel{B} Q'$.
\end{itemize}
\end{description}
Two process terms $P,Q$ are {\em branching equivalent}, denoted by
$P \braeq Q$, iff there exists a branching bisimulation $\Rel{B}$ such that
$P \Rel{B} Q$.
\end{definition}
The notions of $\eta$-, delay, and weak bisimulation are obtained by
relaxing (some of) the constraints imposed by branching bisimulation on the
way that two processes can match each other's behaviours. Compare the following
definitions:
\begin{definition}[$\eta$-, Delay and Weak Equivalence]
\label{Def:eta-bisim}
The notion of {\em $\eta$-bisimulation} is defined just
as a branching
bisimulation above, but without the requirement $P' \Rel{B} Q_2$.
Two process terms $P,Q$ are {\em $\eta$-equivalent}, denoted by
$P \etaeq Q$, iff there exists an $\eta$-bisimulation $\Rel{B}$ such that
$P \Rel{B} Q$.
\label{Def:delay-bisim}
Likewise, a {\em delay bisimulation}, or {\em $d$-bisimulation}
for short, is defined just as a branching bisimulation, but
omitting the requirement $P \Rel{B} Q_1$.
Two process terms $P,Q$ are {\em delay equivalent}, denoted by
$P \deleq Q$, iff there exists a delay bisimulation $\Rel{B}$ such that
$P \Rel{B} Q$.
\label{Def:weak-bisim}
Finally, a {\em weak bisimulation}, or {\em $w$-bisimulation}, lacks
both the requirements $P \Rel{B} Q_1$ and $P' \Rel{B} Q_2$, and two process
terms $P,Q$ are {\em weakly equivalent}, denoted by $P \obseq Q$, iff there
exists a weak bisimulation $\Rel{B}$ such that $P \Rel{B} Q$.
\end{definition}
\begin{remark}
It is easy to see that in the definitions of both branching and delay
bisimulation the existence requirement of a term $Q'$ such that $Q_2
\mvt{\epsilon} Q'$ and $P' \Rel{B} Q'$ is redundant.
\end{remark}
\noindent
The notions of delay and weak equivalence were originally both introduced
by Milner under the name of {\sl observation(al) equivalence}.
\begin{proposition}\label{Propn:relations}
Each of the relations $\bis{\wild}{}$ {\em
($\wild\in\set{b,\eta,d,w}$) }
is an equivalence relation and the largest $\wild$-bisimulation.
Furthermore, for all $P,Q$,
\begin{enumerate}
\item $P \braeq Q$ implies $P\etaeq Q$ implies $P\obseq Q$;
\item $P \braeq Q$ implies $P\deleq Q$ implies $P\obseq Q$.
\end{enumerate}
\end{proposition}
\begin{proof}
For $\wild\in\set{\eta,d,w}$, the identity relation, the converse of a
$\wild$-bisimulation and the symmetric closure of the composition of two
$\wild$-bisimulations are all $\wild$-bisimulations. Hence $\bis{\wild}{}$
is an equivalence relation. This argument does not apply for $\wild=b$ because
the symmetric closure of the composition of two $b$-bisimulations need not be
a $b$-bisimulation, but in \cite{Bas95} it is shown that also $\bis{b}{}$ is
an equivalence relation.
That $\bis{\wild}{}$ is the largest $\wild$-bisimulation (for
$\wild\in\set{b,\eta,d,w}$) follows immediately from the
observation that the set of $\wild$-bisimulations is closed under
arbitrary unions. The implications hold by definition.
\end{proof}
\noindent
The reader familiar with the literature on process theory might have noticed
that, in the above definitions, we have departed from the standard approach
followed in, {\eg}, \cite{Mi89} in that we have defined notions of
bisimulation equivalence that apply to open terms directly. Indeed, with the exception
of studies like \cite{Mi89a,vG93}, bisimulation equivalences like those
presented in Defs.~\ref{Def:branch-bisim}--\ref{Def:weak-bisim} are usually
defined for closed process expressions only, and are extended to open
process expression thus ($\wild\in\set{b,\eta,d,w}$):
\[
P \bis{\wild}{} Q ~\Iff~ P\sigma \bis{\wild}{} Q\sigma, \mbox{ for every
closed substitution } \sigma \enspace .
\]
By the following result, first shown in \cite{vG93} for branching
bisimulation over basic CCS with recursion, both approaches yield the same
equivalence relation over open terms in the language $\LMPA$.
\begin{proposition}\label{Propn:same-equivalence}
For all $P,Q\in\OMPAdef$ and $\wild\in\set{b,\eta,d,w}$,
\begin{center}
$P \bis{\wild}{} Q$ iff $P\sigma \bis{\wild}{} Q\sigma$ for every closed
substitution $\sigma:\Vardef \rightarrow {\MPA}$.
\end{center}
\end{proposition}
\begin{proof}
In the proof of this result, we shall make use of the following, easily
established, facts, which relate the transitions of a term $P\sigma$ to
those of $P$ and those of the terms $\sigma(x)$:
\begin{enumerate}
\item If $P \mv{\alpha} P'$, then $P\sigma \mv{\alpha} P'\sigma$.
\item If $P \mv{x} x$ and $\sigma(x) \mv{\xi} Q$, then
$P\sigma \mv{\xi} Q$.
\item If $P\sigma \mv{\xi} Q$, then either
\begin{enumerate}
\item $\xi\in A_\tau$ and there exists a $P'$ such that
$P \mv{\xi} P'$ and $Q \equiv P'\sigma$, or
\item there exists an $x\in\Var$ such that
$P \mv{x} x$ and $\sigma(x) \mv{\xi} Q$.
\end{enumerate}
\end{enumerate}
We now prove the two implications in the statement of the proposition
separately.
\begin{itemize}
\item {\sc `Only If Implication'}.
Assume that $P \bis{\wild}{} Q$ ($\wild\in\set{b,\eta,d,w}$).
We shall show that
$P\sigma \bis{\wild}{} Q\sigma$ for every closed
substitution $\sigma:\Var \rightarrow \MPA$. To this end, it is
sufficient to prove that the relation:
\begin{eqnarray*}
\Rel{B}_\wild & \deq & \set{ (S\sigma,T\sigma) \mid
S \bis{\wild}{} T,
\mbox{ $\sigma$ a closed substitution}
}
\end{eqnarray*}
is a $\wild$-bisimulation. This is straightforward using
facts 1--3 above.
\item {\sc `If Implication'}.
Let $\wild\in\set{b,\eta,d,w}$.
Assume that $P\sigma \bis{\wild}{} Q\sigma$ for every closed
substitution $\sigma$. We shall show that $P \bis{\wild}{} Q$ holds.
This we prove by induction on the number of variables occurring
in $P$ or $Q$, {\ie}, on the cardinality of $\Var(P) \cup \Var(Q)$.
\begin{itemize}
\item {\sc Basis}: $\Var(P) \cup \Var(Q) = \emptyset$.
In this case, $P$ and $Q$ are closed terms, and the claim
follows immediately.
\item {\sc Inductive Step}: $\Var(P) \cup \Var(Q) \neq \emptyset$.
Choose a variable $x$ in $\Var(P) \cup \Var(Q)$. As the set
of observable actions $A$ is non-empty, we can pick $a\in A$.
It is easy to see that, for positive integers $n,m$,
\[
a^n.0 \bis{\wild}{} a^m.0 ~\Iff~ n=m \enspace .
\]
By Fact~\ref{Fact:finite-state}, $\der{P} \cup \der{Q}$ is a
finite set of
process terms. Therefore it is possible to choose a positive
integer $n$ such that, for every $R\in\der{P} \cup \der{Q}$,
\begin{eqnarray}\label{Eqn:1}
a^n.0 & \nobis{\wild}{} & R \enspace .
\end{eqnarray}
Note that the above inequality implies that, for every
$R\in\der{P} \cup \der{Q}$,
\begin{eqnarray}\label{Eqn:2}
a^n.0 & \nobis{\wild}{} & R[x \mapsto a^{n+1}.0] \enspace .
\end{eqnarray}
This is immediate by (\ref{Eqn:1}) if $x$ does not occur in $R$.
Otherwise, $x$ occurs in $R$, and it is not hard to see that
$R[x \mapsto a^{n+1}.0]$ can perform a sequence of transitions
leading to $0$ that has a suffix consisting of at least $n+1$
$a$-transitions, whereas $a^n.0$ cannot.
% \pagebreak
Now, note that, for every closed substitution $\sigma$,
\begin{eqnarray}\label{Eqn:3}
\parens{P[x \mapsto a^{n+1}.0]}\sigma & \bis{\wild}{} &
\parens{Q[x \mapsto a^{n+1}.0]}\sigma
\enspace .
\end{eqnarray}
As the set of variables occurring in $P[x \mapsto a^{n+1}.0]$ or
$Q[x \mapsto a^{n+1}.0]$ is strictly contained in $\Var(P) \cup
\Var(Q)$, we may apply the inductive hypothesis to (\ref{Eqn:3})
to infer that:
\begin{eqnarray}\label{Eqn:4}
P[x \mapsto a^{n+1}.0] & \bis{\wild}{} &
Q[x \mapsto a^{n+1}.0]
\enspace .
\end{eqnarray}
We prove that this implies $P \bis{\wild}{} Q$, as required.
To this end, in view of (\ref{Eqn:4}), it is sufficient to show
that the symmetric closure of the relation
\begin{eqnarray*}
\Rel{B}_\wild & \deq &
\set{ (S,T) \mid
(S,T) \in \der{P}\times\der{Q}
\mbox{ and }
S[x \mapsto a^{n+1}.0] \bis{\wild}{}
T[x \mapsto a^{n+1}.0]
}
\end{eqnarray*}
is a $\wild$-bisimulation. The details of this verification
are straightforward, using facts 1--3 above and
(\ref{Eqn:2}). In particular, condition (\ref{Eqn:2}) ensures
that whenever $S \Rel{B}_\wild T$ and $S \mv{x} x$, then
$T \mvt{x} x$.
\end{itemize}
This completes the proof of the inductive step, and thereby of
the `if' implication.
\end{itemize}
The proof of the proposition is now complete.
\end{proof}
\noindent
\begin{remark}
The reader may have noticed that the `if' implication in the above statement
would {\sl not} hold if the set of observable actions $A$ were empty. In
fact, in that, admittedly uninteresting, case, the universal relation over
$\MPA$ would be a branching bisimulation. This would imply, for instance,
that, for every closed substitution $\sigma$ and variables $x,y$,
\[
x \sigma \braeq y \sigma \enspace .
\]
On the other hand, $x$ is not branching equivalent to $y$.
\end{remark}
\noindent
For the standard reasons explained at length in, {\eg}, Milner's textbook
\cite{Mi89}, none of the aforementioned equivalences is a congruence with
respect to the summation operation. In fact, it is also the case
that none of the aforementioned equivalences is preserved by the
prefix iteration operation. As a
simple example of this phenomenon, consider the terms $b .0$ and
$\tau.b.0$. As it is well-known, $b.0 \bis{\wild}{}
\tau . b .0$ ($\wild\in\set{b,\eta,d,w}$);
however, it is not difficult to check that $a^*(b.0) \nobis{\wild}{}
a^*(\tau . b .0)$. Following Milner \cite{Mi89}, the solution to these
congruence problems is by now standard; it is sufficient to consider, for each
equivalence $\bis{\wild}{}$, the largest congruence over $\OMPA$ contained
in it. We now proceed to characterize the resulting congruences explicitly.
\begin{definition}\label{Def:congruences}
We say that:
\begin{itemize}
\item $P$ and $Q$ are {\em branching congruent}, written $P \bracong Q$,
iff for all $\xi\in A_\tau \cup \Vardef$,%
\vspace{-1ex}\begin{enumerate}
\item if $P \mv{\xi} P'$, then $Q \mv{\xi} Q'$ for some $Q'$ such that
$P' \braeq Q'$;
\item if $Q \mv{\xi} Q'$, then $P \mv{\xi} P'$ for some $P'$ such that
$P' \braeq Q'$.
\end{enumerate}
\item $P$ and $Q$ are {\em $\eta$-congruent}, written $P \etacong Q$,
iff for all $\xi\in A_\tau \cup \Vardef$,
\vspace{-1ex}\begin{enumerate}
\item if $P \mv{\xi} P'$, then $Q \mv{\xi} Q_1 \mvt{\epsilon} Q'$ for
some $Q_1, Q'$ such that $P' \etaeq Q'$;
\item if $Q \mv{\xi} Q'$, then $P \mv{\xi} P_1 \mvt{\epsilon}P'$ for
some $P_1, P'$ such that $P' \etaeq Q'$.
\end{enumerate}
\item $P$ and $Q$ are {\em delay congruent}, written $P \delcong Q$,
iff for all $\xi\in A_\tau \cup \Vardef$,
\vspace{-1ex}\begin{enumerate}
\item if $P \mv{\xi} P'$, then $Q \mvt{\epsilon} Q_1 \mv{\xi}Q'$
for some $Q_1, Q'$ such that $P' \deleq Q'$;
\item if $Q \mv{\xi} Q'$, then $P \mvt{\epsilon} P_1 \mv{\xi} P'$ for
some $P_1, P'$ such that $P' \deleq Q'$.
\end{enumerate}
\item $P$ and $Q$ are {\em weakly congruent}, written $P \obscong Q$,
iff for all $\xi\in A_\tau \cup \Vardef$,
\vspace{-1ex}\begin{enumerate}
\item if $P \mv{\xi} P'$, then $Q \mvt{\xi} Q'$ for some $Q'$ such that
$P' \obseq Q'$;
\item if $Q \mv{\xi} Q'$, then $P \mvt{\xi} P'$ for some $P'$ such that
$P' \obseq Q'$.
\end{enumerate}
\end{itemize}
\end{definition}
\begin{proposition}\label{Propn:largest}
For every $\wild\in\set{b,\eta,d,w}$, the relation $\bis{\wild}{c}$ is the
largest congruence over $\OMPAdef$ contained in $\bis{\wild}{}$.
\end{proposition}
\begin{proof}
It is straightforward to check that $\bis{\wild}{c}$ is an equivalence
relation for $\wild\in\set{b,\eta,d,w}$, using that this is the
case for $\bis{\wild}{}$. Moreover, it
is trivial to see that $\bis{\wild}{c}$ is included in $\bis{\wild}{}$.
That $\bis{\wild}{c}$ is a congruence relation over $\OMPA$ follows
easily from Definition \ref{Def:congruences}, using that the relation
$$%\set{(P_1 + P_2 , Q_1 + Q_2) \mid P_i \bis{\wild}{c} Q_i,~~i=1,2} \cup
\{(\alpha^*P,\alpha^*Q) \mid \alpha \in A_\tau, P \bis{\wild}{c} Q\}
\cup \bis{\wild}{}$$
is a $\wild$-bisimulation. Here it is essential that, unlike $\bis{\wild}{}$,
the relations $\bis{\wild}{c}$ require that an initial
$\tau$-transition in a process can{\sl not} be matched by the other
staying idle.
To see that $\bis{\wild}{c}$ is indeed the largest congruence relation
over $\OMPA$ contained $\bis{\wild}{}$, assume that $=_\wild$ is another
relation with these properties and that $P =_\wild Q$.
We show that $P \bis{\wild}{c} Q$ holds.
As $A$ is non-empty, we can pick an action $a\in A$.
By Fact~\ref{Fact:finite-state}, $\der{P} \cup \der{Q}$ is a finite set of
process terms. Therefore it is possible to choose a positive
integer $n$ such that, for every $R\in\der{P} \cup \der{Q}$,
\begin{eqnarray*}\label{Eqn:choose-n}
a^n.0 & \nobis{\wild}{} & R \enspace .
\end{eqnarray*}
As $P =_\wild Q$ and $=_\wild$ is a congruence relation contained in
$\bis{\wild}{}$, it follows that $P + a^{n+1}.0$ $\bis{\wild}{} Q + a^{n+1}.0$.
For every $\wild\in\set{b,\eta,d,w}$, this implies that $P \bis{\wild}{c} Q$.
Consider, for instance, the case $\wild = b$. Let $P \mv{\xi} P'$
for some $\xi\in A_\tau \cup \Var$. As $P' \nobis{\wild}{} Q+a^{n+1}.0$,
it must be that $Q+a^{n+1}.0 \mvt{\epsilon} Q_1 \mv{\xi} Q'$ with $P+a^{n+1}.0
\bis{b}{} Q_1$ and $P' \bis{b}{} Q'$. Moreover, as $P+a^{n+1}.0$ cannot be
branching equivalent to a derivative of $Q$, it follows that $Q_1 \equiv
Q+a^{n+1}.0$. Finally $P' \nobis{\wild}{} a^{n}.0$, so $Q \mv{\xi}
Q'$, even when $\xi = a$. By symmetry, it follows
%Following the arguments in \cite[Chapter 7]{Mi89}, it is not hard to show
%that this implies
that $P \bis{b}{c} Q$, which was to be shown.
\end{proof}
\noindent
\begin{remark}
Again, note that, if the set of observable actions $A$ were empty, then the
relations $\bis{\wild}{c}$ ($\wild\in\set{b,\eta,d,w}$) would {\sl not}
be the largest congruences contained in $\bis{\wild}{}$ over $\OMPA$. In fact,
in that case, $\bis{\wild}{}$ itself would be a congruence, and it is
easy to see that, {\eg}, $\tau.0 \bis{\wild}{} 0$, but
$\tau.0 \nobis{\wild}{c} 0$.
\end{remark}
\noindent
\begin{remark}
Bloom \cite{Bl95} has formulated the `RWB cool' and `RBB cool' formats
for transition rules, which ensure that the relations
$\bis{w}{c}$ and $\bis{b}{c}$, respectively, are congruences.
Although both $\bis{w}{c}$ and $\bis{b}{c}$
are congruences for $\OMPA$, the transition rules for $\LMPA$ do
{\sl not} fit the RWB and RBB cool formats. In particular,
Bloom's formats require that operators for which weak or branching
equivalence is not a congruence are not to occur in the right-hand
sides of conclusions of transition rules. However, we already remarked
that weak and branching equivalence are not congruences for prefix
iteration, but this operator does occur at the right-hand side of the
transition rule $a^*P\mv{a}a^*P$.
Hence, we obtain a positive answer to the fourth open question
at the end of \cite{Bl95}, namely whether
there exist transition rules outside the RWB and RBB cool formats
which define `interesting' operators
for which $\bis{w}{c}$ and $\bis{b}{c}$ are congruences.
\end{remark}
\noindent
The following result is the counter-part of
Propn.~\ref{Propn:same-equivalence} for the aforementioned congruence
relations.
\begin{proposition}\label{Propn:same-congruence}
For $P,Q\in\OMPAdef$ and $\wild\in\set{b,\eta,d,w}$,
\begin{center}
$P \bis{\wild}{c} Q$ iff $P\sigma \bis{\wild}{c} Q\sigma$ for every closed
substitution $\sigma$.
\end{center}
\end{proposition}
\begin{proof}
A straightforward modification of the proof of
Propn.~\ref{Propn:same-equivalence}.
\end{proof}
\noindent
We end this section with two lemmas that will be of use in the completeness
proof for branching congruence. (Cf.~the proof of
Propn.~\ref{Propn:prove-nf}.) The first of these lemmas is a standard
result for branching bisimulation equivalence, whose proof may be found in
\cite{GW90,DMV90}.
\begin{lemma}[Stuttering Lemma]
\label{Lem.stuttering}
If $P_0\mv{\tau}\cdots\mv{\tau}P_n$ and $P_n\braeq P_0$, then
$P_i\braeq P_0$ for $i=1,...,n-1$.
\end{lemma}
The following result about the expressiveness of the language
$\OMPA$ stems from \cite{AI95}.
\begin{lemma}
\label{lem.Luca}
Let $a,b\in A$. If $a^*P\bis{\wild}{} b^*Q$ {\em ($\wild\in\set{b,\eta,d,w}$)},
then $a=b$.
\end{lemma}
\begin{proof}
In light of Propn.~\ref{Propn:relations}, it is sufficient to deal with the
case $\wild=w$. Let $a^* P \obseq b^* Q$.
Then there exist terms $P',Q'$ such that:
\begin{itemize}
\item $a^*P \mvt{b} P' \obseq b^* Q$, and
\item $b^* Q \mvt{a} Q' \obseq a^* P$.
\end{itemize}
This implies that $a^*P$ and $b^*Q$ both exhibit, for example,
an infinite sequence where $a$ and $b$ alternate, i.e.,
$\mvt{a}\mvt{b}\mvt{a}\mvt{b}\cdots$.
Thus, this lemma is an immediate consequence of the following fact.
\begin{itemize}
\item
If $P_n\mvt{a_n}P_{n+1}$ for $n=0,1,2,...$, then there
is an $N$ such that $a_n=a_N$ for $n>N$.
\end{itemize}
The proof of this fact is an easy exercise by structural induction
on terms, which is left to the reader.
\end{proof}
\section{Axiom Systems}\label{Sect:axiomatization}
The main aim of this study is to provide complete equational axiomatizations
for branching, $\eta$-, delay, and weak congruence over the language $\OMPA$.
In this section, we present the axiom systems that will be shown to completely
characterize these congruence relations over $\OMPA$, and prove
their soundness. We also present a proposition on the inter-derivability
of these axiom systems that will be useful
in the proofs of the promised completeness theorems, and address the issue of
the irredundancy of the axiom systems.
\subsection{The axioms}
Table \ref{Tab:Fokkink} presents the axiom system $\cal F$, which
was shown in \cite{Fok94} to characterize strong bisimulation over
$\mbox{T(BCCS)}^{\scriptstyle p*}(A)$.
In addition to the axioms in ${\cal F}$, the axiom systems
${\cal E}_\wild$ ($\wild\in\set{b,\eta,d,w}$)
include equations which express the unobservable nature of the $\tau$ action.
These equations may be found in
Tables~\ref{Tab:equations-bra-eta}--\ref{Tab:equations-wea};
%\ref{Tab:equations-del-wea}, and \ref{Tab:equations-eta-wea};
they reflect the different ways in which the
congruences we consider abstract away from internal computations in process
behaviours. The axiom system ${\cal E}_b$ is obtained by adding the axioms
presented in Table \ref{Tab:equations-bra-eta} to $\cal F$, and
${\cal E}_\eta$ extends ${\cal E}_b$ with the equations in
Table~\ref{Tab:equations-eta-wea}. The set of axioms ${\cal E}_d$ includes
the equations in $\cal F$ and those in Table~\ref{Tab:equations-del-wea}.
Finally, ${\cal E}_w$ extends ${\cal E}_d$ with the laws in
Table~\ref{Tab:equations-wea}.
\begin{table}[htb]
\[
\begin{array}{|lrll|}
\hline
&&&\\
\mbox{\sc A1} & x + y & = & y + x \\
\mbox{\sc A2} & (x + y) + z & = & x + (y + z) \\
\mbox{\sc A3} & x + x & = & x \\
\mbox{\sc A4} & x + 0 & = & x \\
\mbox{\sc PA1} & a. (a^*x) + x & = & a^*x\\
\mbox{\sc PA2} & a^*(a^*x) & = & a^*x \\
&&&\\
\hline
\end{array}
\]
\caption{\label{Tab:Fokkink}The axiom system ${\cal F}$}
\end{table}
\begin{table}[htb]
\[
\begin{array}{|lrll|}
\hline
&&&\\
\mbox{\sc B1} & \alpha . \parens{\tau . \parens{x+y}+x} & = & \alpha.\parens{x+y} \\
\mbox{\sc PB1} & \tau^*x & = & \tau. x + x \\
\mbox{\sc PB2} & \tau.a^*\parens{\tau.a^*\parens{x+y} + x} & = &
\tau.a^*\parens{x+y}\\
&&&\\
\hline
\end{array}
\]
\caption{\label{Tab:equations-bra-eta}Axioms for ${\cal E}_b$ and for ${\cal E}_\eta$}
\end{table}
\begin{table}[htb]
\[
\begin{array}{|lrll|}
\hline
&&&\\
\mbox{\sc T1} & \alpha . \tau . x & = & \alpha . x \\
\mbox{\sc T2} & \tau . x & = & \tau . x + x \\
\mbox{\sc PT1} & \tau^*x & = & \tau . x \\
\mbox{\sc PT2} & \tau. (a^* x) & = & a^* \parens{ \tau. \parens{a^*x} } \\
&&&\\
\hline
\end{array}
\]
\caption{\label{Tab:equations-del-wea}Axioms for ${\cal E}_d$ and for ${\cal E}_w$}
\end{table}
\begin{table}[htb]
\[
\begin{array}{|lrll|}
\hline
&&&\\
\mbox{\sc T3} &\alpha.(x+\tau.y)&=&\alpha.(x+\tau.y)+\alpha.y\\
\mbox{\sc PT3} & a^* (x + \tau .y) & = & a^* (x + \tau .y + a.y) \\
&&&\\
\hline
\end{array}
\]
\caption{\label{Tab:equations-eta-wea}Extra axioms for ${\cal E}_\eta$}
\end{table}
\begin{table}[htb]
\[
\begin{array}{|lrll|}
\hline
&&&\\
\mbox{\sc AT3} &a.(x+\tau.y)&=&a.(x+\tau.y)+a.y\\
\mbox{\sc PT3} & a^* (x + \tau .y) & = & a^* (x + \tau .y + a.y) \\
&&&\\
\hline
\end{array}
\]
\caption{\label{Tab:equations-wea}Extra axioms for
${\cal E}_w$}
\end{table}
The law B1 and the equations T1-3, AT3 are standard characterizations of the
silent action
$\tau$ in branching and weak congruence, respectively. (Note that AT3 is the
instance of T3 with $\alpha\in A$. We distinguish the laws T3 and AT3 in order
to obtain an irredundant axiom system for weak congruence.
Cf.~Propn.~\ref{Propn:independence} and the subsequent remark for more
details.)
The origins of the five remaining axioms, which describe the
interplay between $\tau$ and prefix iteration, are as follows.
The equations PB1 and PB2 stem from \cite{Fok95},
where a complete axiomatization for branching congruence over closed terms
in the language BPA \cite{BK84} with prefix iteration was presented.
(For the sake of precision, we remark here that equation PB2 was formulated
in \cite{Fok95} thus:
\begin{eqnarray*}
a.a^*\parens{\tau.a^*\parens{x+y} + x} & = &
a.a^*\parens{x+y} \enspace .
\end{eqnarray*}
The two versions of equation PB2 are easily shown to be
inter-derivable; each of them proves their common generalization
\begin{eqnarray*}
\mbox{\sc PB2}'~~~\gamma.a^*\parens{\tau.a^*\parens{x+y} + x} & = &
\gamma.a^*\parens{x+y} \enspace
\end{eqnarray*}
for $\gamma \in A_\tau$, using laws A1, A2, A4, PA1 and B1.)
The equation PT1 was
introduced in \cite{BBP94} under the name of
(FIR$_1$) ({\sl Fair Iteration Rule\/}). In \cite{BBP94} it was also noted
that this law is an equational formulation of {\sl Koomen's Fair Abstraction
Rule} \cite{BBK87a}. (To be precise, Koomen's Fair Abstraction Rule
is a general name for a family of proof rules KFAR$_n$, $n\geq 1$.
PT1 corresponds to KFAR$_1$.)
The laws PT2 and PT3
originate from \cite{AI95}, where the axiom system ${\cal E}_w$ was shown to
be complete for weak congruence over $\MPA$, and $\omega$-complete in the
presence of a denumerable set of observable actions $A$.
Note that each of the axiom systems ${\cal E}_\wild$
($\wild\in\set{b,\eta,d,w}$) is finite if so is the set of actions $A$.
\begin{notation}
For an axiom system ${\cal T}$, we
write ${\cal T} \proves P = Q$ iff the equation\linebreak $P = Q$ is provable
from the axiom system $\cal T$ using the rules of equational logic.
For axiom systems ${\cal T}, {\cal T}'$, we write ${\cal T} \proves
{\cal T}'$ iff ${\cal T} \proves P = Q$ for every equation $(P=Q)\in{\cal T}'$.
%We adopt the convention that the axioms A1 and A2 are included
%in all the axiom systems considered in this paper, even when they are
%not mentioned explicitly.
For a collection of equations $X$ over the signature of $\LMPAdef$, we write
$P \stackrel{\mbox{\tiny X}}{=} Q$ as a short-hand for
$\mbox{\em A1,A2,X} \proves P = Q$.
For $I = \set{i_1 ,\ldots, i_n}$ a finite index set, we write
$\sum_{i\in I}P_i$ or $\sum\set{P_i \mid i\in I}$ for
$P_{i_1} + \cdots + P_{i_n}$.
By convention, $\sum_{i\in\emptyset}P_i$ stands for $0$.
\end{notation}
\noindent
We establish the soundness of the axiom systems.
\begin{proposition}\label{Propn:soundness}
Let $\wild\in\set{b,\eta,d,w}$.
If ${\cal E}_\wild \proves P = Q $, then $P \bis{\wild}{c} Q$.
\end{proposition}
\begin{proof}
As $\bis{\wild}{c}$ ($\wild\in\set{b,\eta,d,w}$) is a congruence, it is
sufficient to show that each equation in ${\cal E}_\wild$ is sound with
respect to it.
The equations in the axiom system $\cal F$ are known to be sound with respect
to strong bisimulation equivalence over $\OMPA$; therefore they are, {\sl a
fortiori},
sound with respect to each of the congruences we consider. The soundness of
the axioms B1, T1-3 and AT3 is well-known, and that of
PB1-2 and PT1-3 is easy to check.
\end{proof}
\subsection{Expressiveness of the axiom systems}
For use in the promised completeness theorems, we now study the relative
expressive power of the axiom systems.
%, and present some useful derived
%equations.
\begin{proposition}\label{Propn:relative}
${\cal E}_w \proves {\cal E}_d \proves {\cal E}_b$ and
${\cal E}_w \proves {\cal E}_\eta \proves {\cal E}_b$.
\end{proposition}
{\bf Proof:} {\small %\begin{proof}
Since ${\cal E}_w$ incorporates ${\cal E}_d$, and ${\cal E}_\eta$
incorporates ${\cal E}_b$, the statements ${\cal E}_w \proves {\cal E}_d$
and ${\cal E}_\eta \proves {\cal E}_b$ are trivially true.
In order to prove the remaining two statements,
${\cal E}_d \proves {\cal E}_b$ and ${\cal E}_w \proves {\cal E}_\eta$,
it suffices to show that the three axioms in
Table \ref{Tab:equations-bra-eta} and the instance of T3 for $\alpha =\tau$
are derivable from ${\cal E}_d$.
%Let $P \stackrel{\scriptstyle X}{=} Q$ denote that the equation
%$P=Q$ is derivable from the laws A1, A2 and $X$.
%We deal with these three axioms separately. N
First of all, note that
\begin{equation}\label{Eqn:DT2}
%\mbox{A3,T2}\proves
\tau.(x+y) \stackrel{\mbox{\tiny A3,T2}}{=} \tau.(x+y)+x \enspace .
\end{equation}
The derivability of the instance of T3 with $\alpha =\tau$ from
${\cal E}_d$ follows immediately by observing that, modulo commutativity
of $+$, that equality
is a substitution instance of (\ref{Eqn:DT2}).
%We now deal with the three axioms in Table~\ref{Tab:equations-bra-eta}.
In deriving the laws in Table~\ref{Tab:equations-bra-eta} from ${\cal E}_d$,
we shall make use of the following derived equation:
\begin{equation}\label{Eqn:DPA1}
%\mbox{A3,PA1}\proves
a^*x+x \stackrel{\mbox{\tiny A3,PA1}}{=} a^*x\enspace .
\end{equation}
The derivation of the three axioms in Table~\ref{Tab:equations-bra-eta}
from ${\cal E}_d$ now proceeds as follows:
\\ \mbox{}\hfill
$\begin{array}[b]{llcl}
\\
\mbox{B1}&\multicolumn{3}{l}{\alpha.(\tau.(x+y)+x)~
\stackrel{\mbox{\tiny (\ref{Eqn:DT2})}}{=}~
\alpha.\tau.(x+y)~\stackrel{\mbox{\tiny T1}}{=}~\alpha.(x+y)\enspace.}\\
\\
\mbox{PB1}&\multicolumn{3}{l}{\tau^* x~\stackrel{\mbox{\tiny PT1}}{=}~\tau.x
~\stackrel{\mbox{\tiny T2}}{=}~\tau.x+x\enspace.}\\
\\
{\mbox{PB2}}&\tau.a^*(\tau.a^*(x+y)+x)
&\stackrel{\mbox{\tiny (\ref{Eqn:DPA1})}}{=}&\tau.a^*(\tau.(a^*(x+y)+x+y)+x)\\
&&\stackrel{\mbox{\tiny (\ref{Eqn:DT2})}}{=}&\tau.a^*(\tau.(a^*(x+y)+x+y))\\
&&\stackrel{\mbox{\tiny (\ref{Eqn:DPA1})}}{=}&\tau.a^*(\tau.a^*(x+y))\\
&&\stackrel{\mbox{\tiny PT2}}{=}&\tau.(\tau.a^*(x+y))\\
&&\stackrel{\mbox{\tiny T1}}{=}&\tau.a^*(x+y)\enspace .
\end{array}$\hfill$\Box$
}%\]
%\end{proof}
%%% Omitted Lemma 3.4
\iffalse
\noindent The following derived equation will be useful in the completeness
proof for weak congruence.
\begin{lemma}\label{Lem:derivable-equations}
${\cal E}_w\proves a^*\parens{x+\tau.y}=a^*\parens{x+\tau.y}+a.y$.
\end{lemma}
\begin{proof}\quad
\[
\begin{array}{rcl}
a^*\parens{ x + \tau . y}
&\stackrel{\mbox{\tiny PT3}}=& a^*\parens{ x + \tau . y + a.y}\\
&\stackrel{\mbox{\tiny (\ref{Eqn:DPA1})}}=& a^*\parens{x+\tau.y+a.y}+x+\tau.y+a.y\\
&\stackrel{\mbox{\tiny A3}}=& a^*\parens{ x + \tau . y + a.y} +
x + \tau . y + a.y + a.y\\
&\stackrel{\mbox{\tiny (\ref{Eqn:DPA1})}}=& a^*\parens{x+\tau.y+a.y}+a.y\\
&\stackrel{\mbox{\tiny PT3}}=& a^*\parens{x+\tau.y}+a.y\enspace .
\end{array}
\]
%Axiom PT3 is not essential in the derivation of this equation;
%there is an alternative derivation in ${\cal E}_w$ that uses PA1 and T3.
\end{proof}
\fi
%%% End of omitted Lemma 3.4
%%% Omitted notation 3.5
\iffalse
\begin{notation}
For $I = \set{i_1 ,\ldots, i_n}$ a finite index set, we write
$\sum_{i\in I}P_i$ or $\sum\set{P_i \mid i\in I}$ for
$P_{i_1} + \cdots + P_{i_n}$.
By convention, $\sum_{i\in\emptyset}P_i$ stands for $0$.
\end{notation}
\fi
%%% End of omitted notation 3.5
%%% Omitted Lemma 3.6
\iffalse
\noindent
Finally, we note that the axioms of ${\cal E}_b$ are sufficiently powerful
to reduce process terms to head normal form.
\begin{lemma}
\label{Lem.headnormalform}
If the collection of possible transitions from a process term $P$ is
$\{P\mv{\alpha_i}P_i~|~i=1,...,m\}\cup\{P\mv{x_j}x_j~|~j=1,...,n\}$,
then
\[
{\cal E}_b\proves P=\sum_i\alpha_i.P_i+\sum_j x_j\enspace.
\]
\end{lemma}
\begin{proof}
Straightforward by structural induction on $P$, using axioms A1, A2, A4, PA1
and the variant of PA1 with $\tau$ for $a$, which can be deduced
from ${\cal E}_b$ as follows:
\[
\begin{array}{rcl}
\tau.\tau^*x+x
&\stackrel{\mbox{\tiny PB1}}=&\tau.(\tau.x+x)+x\\
&\stackrel{\mbox{\tiny A3}}=&\tau.(\tau.(x+x)+x)+x\\
&\stackrel{\mbox{\tiny B1}}=&\tau.(x+x)+x\\
&\stackrel{\mbox{\tiny A3,PB1}}=&\tau^*x\enspace.
\end{array}
\]
The details of the proof are left to the reader.
\end{proof}
\fi
%%% End of omitted Lemma 3.6
%\subsection{Relative independence of the axioms}
\subsection{Irredundancy of the axiom systems}
A collection $\cal T$ of equations is said to be {\sl irredundant}
\cite[Page 389]{Taylor} iff for every proper subset ${\cal T}'$ of
${\cal T}$ there exists an equation which is derivable from ${\cal T}$,
but not from ${\cal T}'$.
Experience has shown that axiom systems can contain redundancies;
in the field of equational axiomatizations of behavioural congruences
this happens for instance in \cite{vG93}.
Therefore, we find it interesting to conclude this section by addressing the
issue of the irredundancy of the axiom systems ${\cal E}_\wild$
($\wild\in\set{b,\eta,d,w}$).
\begin{proposition}\label{Propn:independence}
For each $\wild\in\set{b,\eta,d,w}$, the axiom system ${\cal E}_\wild$
is irredundant.
\end{proposition}
{\bf Proof:} {\small %\begin{proof}
To show the irredundancy of the axiom system ${\cal E}_\wild$
($\wild\in\set{b,\eta,d,w}$), it is sufficient to prove that, for every
axiom $(P = Q)\in {\cal E}_\wild$,
\begin{equation}\label{Eqn:non-der}
{\cal E}_\wild \setminus \set{P = Q} \not\proves P = Q \enspace .
\end{equation}
The standard proof strategy to establish this kind of result is to find a
model for the axiom system ${\cal E}_\wild \setminus \set{P = Q}$ in which
the equation $P =Q$ is not valid.
As the axiom systems ${\cal E}_b$ and
${\cal E}_d$ are contained in ${\cal E}_\eta$ and ${\cal E}_w$, respectively,
it is sufficient to show (\ref{Eqn:non-der}) for ${\cal E}_\eta$ and
${\cal E}_w$. In what follows, we limit ourselves to the
proofs for the axioms PT$n$ ($n=1,2,3$) and PB$n$ ($n=1,2$).
We present the model explicitly
only for axioms PT2, PB2 and PT3. For axioms PT1 and PB1
we merely give the intuition underlying the construction of an
appropriate model. The reader will not have too much trouble
in finding models which capture this intuition.
\begin{description}
\item {\sc Axioms} PT1 and PB1. Intuitively, the reason why equations
PT1 and PB1 are not derivable from the axiom systems
${\cal E}_w\setminus \set{\mbox{\sc PT1}}$ and ${\cal E}_{\eta}
\setminus\set{\mbox{\rm PB1}}$, respectively, is that \mbox{\sc PT1}
and PB1 are the
only equations that can be used to completely eliminate occurrences
of the operation $\tau^*$ from terms.
\item {\sc Axioms} PT2 and PB2. These axioms can actually be regarded
as axiom schemes, in the sense that there is one axiom for each
choice of an action $a \in A$. Call these instantiations PT2$(a)$
and PT3$(a)$. We now show that for all $a \in A$
$${\cal E}_w \setminus\set{\mbox{\rm PT2}(a)}\not\proves\mbox{\sc PT2}(a)
\enspace \mbox{ and } \enspace {\cal E}_b \setminus
\set{\mbox{\rm PB2}(a)}
\not\proves \mbox{\sc PB2}(a) \enspace .$$
Let $a \in A$.
We say that a term $P$ is {\sl stable} iff $P \mv{\tau} P'$ for no $P'$.
A term whose sub-terms of the form $a^* P'$ are
stable is said to be {\sl $a^*$-stable}.
Intuitively, the reason why {\sc PT2$(a)$} and PB2$(a)$
cannot be derived from the other equations is that {\sc
PT2}$(a)$ and PB2$(a)$ are the only
axioms in ${\cal E}_w$ and ${\cal E}_\eta$, respectively, that can be
used to equate an $a^*$-stable term to one that is not.
Formally, define a denotational semantics for $\OMPA$ in the domain
$2^{\scriptstyle\set{0,1}}$ by:\vspace{-2ex}
\begin{eqnarray*}
\mean{x}\rho & = & \rho(x) \\
\mean{0}\rho & = & \emptyset \\
\mean{\tau .P}\rho & = & \mean{P}\rho \cup \set{1} \\
\mean{b.P}\rho & = & \mean{P}\rho \setminus \set{1} ~~~~~~~
\mbox{for } b \in A\\
\mean{P + Q}\rho & = & \mean{P}\rho \cup \mean{Q}\rho \\
\mean{\tau^*P}\rho & = & \mean{P}\rho \cup \set{1} \\
\mean{b^* P}\rho & = & \casedef{\mean{P}\rho \cup \set{0} &
\mbox{if $b=a \wedge 1\in\mean{P}\rho$} \\
\mean{P}\rho &
\mbox{otherwise} }
\end{eqnarray*}
where $\rho:\Var \rightarrow 2^{\scriptstyle\set{0,1}}$.
Here $1 \not\in \mean{P}\rho$ denotes stability and
$0 \not\in \mean{P}\rho$ denotes $a^*$-stability.
It is now simple to check
that this is a model for both the axiom systems
${\cal E}_w\setminus \set{\mbox{\sc PT2$(a)$}}$ and
${\cal E}_\eta\setminus\set{\mbox{\sc PB2$(a)$}}$. However, letting
$\rho_{\emptyset}$ map each variable in $\Var$ to $\emptyset$,
% \[
% \mean{a^*(x + \tau .y)}(\lambda x.~0) = 0 \neq 1 =
% \mean{a^*(x + \tau . y + a.y)}(\lambda x.~0)
% \]
\[
\mean{\tau.\parens{a^*x}}\rho_{\emptyset} = \set{1} \neq \set{0,1}
=
\mean{a^*\parens{\tau.\parens{a^*x}}}\rho_{\emptyset}
\]
and
\[
\mean{\tau.a^*\parens{\tau.a^*\parens{x+y} + x}}\rho_{\emptyset}
= \set{0,1} \neq \set{1} =
\mean{\tau.a^*\parens{x+y}}\rho_{\emptyset} \enspace .
\]
Therefore the above is neither a model of ${\cal E}_w$ nor one of
${\cal E}_\eta$.
\item {\sc Axiom} PT3. Again we consider the instantiations PT3$(a)$
and show ${\cal E}_w \setminus \set{\mbox{\rm PT3}(a)} \not\proves
\mbox{\sc PT3}(a)$. We say that a term $P$ is {\em $a$-stable}
iff $P \mvt{a} P'$ for no $P'$.
Intuitively, the reason why {\sc PT3}$(a)$
cannot be derived from the other equations is that {\sc PT3}$(a)$
is the only axiom in ${\cal E}_w$ that can be
used to equate a term $P$ with a
sub-term of the form $a^* P'$ such that $P'$ is $a$-stable
to a term $Q$ that does not have this property.
Formally, define a denotational semantics for $\OMPA$ in the domain
$2^{\set{0,1}}$ by:\vspace{-2ex}
\begin{eqnarray*}
\mean{x}\rho & = & \rho(x) \\
\mean{0}\rho & = & \emptyset \\
\mean{\tau .P}\rho & = & \mean{P}\rho \\
\mean{a.P}\rho & = & \mean{P}\rho \cup \set{1} \\
\mean{b.P}\rho & = & \mean{P}\rho \setminus \set{1} ~~~~~~~
\mbox{for } b \neq a\\
\mean{P + Q}\rho & = & \mean{P}\rho \cup \mean{Q}\rho \\
\mean{\alpha^*P}\rho & = & \mean{P}\rho ~~~~~~~~~~~~~~\,
\mbox{for } \alpha \neq a\\
\mean{a^* P}\rho & = & \casedef{
\set{0,1} & \mbox{if $1 \not\in \mean{P}\rho$} \\
\mean{P}\rho & \mbox{otherwise} }
\end{eqnarray*}
where $\rho:\Var \rightarrow 2^{\set{0,1}}$.
Here $1 \not\in \mean{P}\rho$ denotes $a$-stability and
$0 \in \mean{P}\rho$ denotes the property of having a subterm
$a^*P'$ with $P'$ $a$-stable.
It is now simple to check that this is a model for the axiom system
${\cal E}_w\setminus \set{\mbox{\sc PT3$(a)$}}$.
However, letting
$\rho_{\emptyset}$ map each variable in $\Var$ to $\emptyset$,
\[
\mean{a^*(x + \tau .y)}\rho_{\emptyset} = \set{0,1} \neq \set{1} =
\mean{a^*(x + \tau . y + a.y)}\rho_{\emptyset}
\]
and so the above is not a model of ${\cal E}_w$.\hfill $\Box$
\end{description}
}%\end{proof}
\noindent
\begin{remark}
In light of (\ref{Eqn:DT2}), the instance of axiom T3 with $\alpha = \tau$
is derivable from the axiom system ${\cal E}_d$, and, {\sl a fortiori}, from
${\cal E}_w$. Thus defining the axioms for weak congruence to include T3 in
lieu of AT3 would lead to a redundant axiomatization, like those presented
in, {\eg}, \cite{HM85,Mi89a}.
\end{remark}
\section{Completeness}\label{Sect:completeness}
This section is entirely devoted to detailed proofs of the completeness of
the axiom systems ${\cal E}_\wild$ ($\wild\in\set{b,\eta,d,w}$) with
respect to $\bis{\wild}{c}$ over the language of open terms $\OMPA$.
A common and, we believe, aesthetically pleasing
feature of our completeness proofs for the
behavioural congruences $\bis{\wild}{c}$
($\wild\in\set{\eta,d,w}$) is that they are derived in uniform fashion from
the corresponding results for branching congruence. Moreover, we shall
also argue that the proof of completeness for weak congruence
via reduction to the completeness result for branching congruence
is considerably shorter than the only direct proof of this result presented
in the literature. (Cf.~the reference \cite{AI95}.)
Because of the prominent r\^ole played by the completeness theorem
for branching congruence in the developments to follow, we begin by
presenting our proof of this result. We remark here that the completeness
of the theory ${\cal E}_b$ with respect to $\bracong$ over the language
of closed terms $\MPA$ was first shown in \cite{Fok95}.
The proof presented below is, however, new, and yields the completeness of
the axiom system ${\cal E}_b$ for the whole of the language $\OMPA$.
Moreover it may be argued that, even when restricted to the language
of closed terms, our proof improves on the one offered in the
aforementioned reference in that, unlike that proof, it does not rely on
the completeness result for strong bisimulation from \cite{Fok94}.
\subsection{Completeness for branching congruence}
We aim at identifying a subset of process terms of a special form,
which will be convenient in the proof of the completeness result
for branching congruence. Following a long-established tradition in the
literature on process theory, we shall refer to these terms as {\sl normal
forms}. The set of normal forms we are after is the smallest subset of
$\OMPA$ including process terms having one of the following
two forms:
\[
\sum_{i\in I}\alpha_i.P_i+\sum_{j\in J} x_j~~~~~\mbox{\rm or}~~~~~
a^*(\sum_{i\in I}\alpha_i.P_i+\sum_{j\in J} x_j),
\]
where the terms $P_i$ are themselves normal forms, and $I,J$ are finite index
sets. (Recall that the empty sum represents 0.)
\begin{lemma}
\label{Lem:normalforms}
Each term in $\OMPAdef$ can be proven equal to a normal form using equations
{\em A4, PA1} and {\em PB1}.
\end{lemma}
\begin{proof}
A straightforward induction on the structure of process terms.
\end{proof}
\begin{notation}
{\em $P\ACeq Q$} denotes that $P$ and $Q$ are equal modulo associativity and
commutativity of +, {\ie}, that {\em A1,A2} $\proves P = Q$.
%and we say that $P$ and $Q$ are of the same form.
\end{notation}
The following result is the key to the completeness theorem for
branching congruence.
\begin{proposition}\label{Propn:prove-nf}
For all $P,Q\in\OMPAdef$, if $P \braeq Q$, then, for all $\gamma\in A_\tau$,
${\cal E}_b \proves \gamma.P = \gamma.Q$.
\end{proposition}
\begin{proof}
First of all, note that, as the equations in ${\cal E}_b$ are sound with
respect to $\bracong$, and, {\sl a fortiori}, for $\braeq$, by
Lem.~\ref{Lem:normalforms} it is sufficient
to prove that the statement of the proposition holds for branching equivalent
normal forms $P$ and $Q$.
So, let us assume that $P$ and $Q$ be branching equivalent normal forms.
We prove that ${\cal E}_b\proves\gamma.P=\gamma.Q$ for all $\gamma\in A_\tau$,
by complete induction on the sum of the sizes of $P$ and $Q$.
Recall that normal forms can take the following two forms:
\[
\sum_i\alpha_i.P_i+\sum_j x_j~~~~~\mbox{\rm or}~~~~~
a^*(\sum_i\alpha_i.P_i+\sum_j x_j),
\]
where the $P_i$s are themselves normal forms.
So, in particular, $P$ and $Q$ have one of these forms. By symmetry,
it is sufficient to deal with the following three cases:
\begin{enumerate}
\item $P\ACeq\sum_i\alpha_i.P_i+\sum_k x_k$ and
$Q\ACeq\sum_j\beta_j.Q_j+\sum_l y_l$;
\item $P\ACeq a^*(\sum_i\alpha_i.P_i+\sum_k x_k)$ and
$Q\ACeq b^*(\sum_j\beta_j.Q_j+\sum_l y_l)$; and
\item $P\ACeq\sum_i \alpha_i.P_i+\sum_k x_k$ and
$Q\ACeq a^*(\sum_j\beta_j.Q_j+\sum_l y_l)$.
\end{enumerate}
We treat these three cases separately.
\begin{enumerate}
\item {\sc Case:}
$P\ACeq\sum_i\alpha_i.P_i+\sum_k x_k$ and
$Q\ACeq\sum_j\beta_j.Q_j+\sum_l y_l$.
Consider the following two conditions:
\begin{itemize}
\item[A.]
$\alpha_i=\tau$ and $P_i\braeq Q$ for some $i$;
\item[B.]
$\beta_j=\tau$ and $Q_j\braeq P$ for some $j$.
\end{itemize}
We distinguish three sub-cases in the proof, depending on which of the above
conditions hold.
\begin{itemize}
\item[I]
Suppose that neither A nor B holds. Then, as $P \braeq Q$, each transition
$P\mv{\xi}P'$ must be matched by a transition $Q\mv{\xi}Q'$ with
$P'\braeq Q'$. Hence, each summand $\alpha_i.P_i$ of $P$
matches with a summand $\beta_j.Q_j$ of $Q$, in the sense that
$\alpha_i=\beta_j$ and $P_i\braeq Q_j$. For each such pair of related
summands, induction yields
\[
{\cal E}_b \proves \alpha_i.P_i=\alpha_i.Q_j=\beta_j.Q_j \enspace .
\]
Moreover, each summand $x_k$ of $P$ must be a summand of $Q$. Hence, possibly
using axiom A3, it follows that ${\cal E}_b \proves P + Q =Q$. By symmetry,
we infer that ${\cal E}_b \proves P = P + Q =Q$. The fact that
${\cal E}_b \proves \gamma.P=\gamma.Q$ for all $\gamma\in A_\tau$ is now
immediate.
\item[II]
Suppose that both of A and B hold. In this case, there exist $i$ and $j$
such that $\alpha_i = \beta_j =\tau$ and $P_i \braeq Q \braeq P \braeq Q_j$.
Applying the inductive hypothesis to the equivalences $P \braeq Q_j$,
$P_i \braeq Q_j$ and $P_i \braeq Q$,
we infer that, for all $\gamma\in A_\tau$,
\[
{\cal E}_b \proves \gamma.P = \gamma . Q_j = \gamma . P_i = \gamma . Q
\]
and the inductive step follows.
\item[III]
Suppose that only one of A and B holds.
In the remainder of the proof for this case,
we shall assume, without loss of generality, that only A holds.
For every summand $\tau.P_i$ of $P$ with $P_i\braeq Q$ we obtain,
by induction, that
\[
{\cal E}_b \proves \tau.P_i=\tau.Q \enspace .
\]
Hence, as A holds, by possibly using axioms A3 and/or A4 we infer that
\[
{\cal E}_b \proves P=\tau.Q+S
\]
where $S \ACeq \sum\set{\alpha_i . P_i \mid \alpha_i \neq \tau ~~\mbox{or}~~
P_i \nobis{b}{} Q } + \sum_k x_k$.
Consider now a summand $\alpha_i.P_i$ of $S$.
As condition B does {\sl not}
hold and $P \braeq Q$, using Lem.~\ref{Lem.stuttering} it is not hard to
see that there must exist a summand $\beta_{j_i}.Q_{j_i}$ of $Q$ such that
$\alpha_i = \beta_{j_i}$ and $P_i \braeq Q_{j_i}$. By a similar reasoning, we
infer that each one of the variables $x_k$ must be a summand of $Q$.
For related summands $\alpha_i.P_i$ and $\beta_{j_i}.Q_{j_i}$ of $S$ and $Q$,
respectively, induction yields
\[
{\cal E}_b \proves \alpha_i.P_i=\beta_{j_i}.Q_{j_i} \enspace .
\]
It follows that ${\cal E}_b \proves Q=R+S$, where
\[
R \ACeq \sum\set{\beta_j . Q_j \mid j \neq j_i ~~\mbox{for all $i$}}
+ \sum \set{y_l \mid y_l\neq x_k ~~\mbox{for all $k$}} \enspace .
\]
Now, for every $\gamma\in A_\tau$,
\[
{\cal E}_b \proves \gamma.P=\gamma.(\tau.Q+S)=
\gamma.(\tau.(R+S)+S)\stackrel{\mbox{\tiny B1}}=\gamma.(R+S)=\gamma.Q
\]
and the inductive step follows.
\end{itemize}
\item {\sc Case:}
$P\ACeq a^*(\sum_i\alpha_i.P_i+\sum_k x_k)$ and
$Q\ACeq b^*(\sum_j\beta_j.Q_j+\sum_l y_l)$. First of all, note that,
by Lem.~\ref{lem.Luca}, it must be the case that $a=b$.
Consider the following two conditions:
\begin{itemize}
\item[A.]
$\alpha_i\in\{\tau,a\}$ and $P_i\braeq Q$ for some $i$;
\item[B.]
$\beta_j\in\{\tau,a\}$ and $Q_j\braeq P$ for some $j$.
\end{itemize}
We distinguish three sub-cases in the proof, depending on which of the above
conditions hold.
\begin{itemize}
\item[I]
Suppose that neither A nor B holds. Then it is easy to see that
\[
\sum_i\alpha_i.P_i+\sum_k x_k \braeq \sum_j\beta_j.Q_j+\sum_l y_l
\]
holds. As these two terms are normal forms whose combined size is smaller
that that of $P$ and $Q$, we may reason exactly as in the previous case 1.I
to obtain that
${\cal E}_b \proves
\sum_i\alpha_i.P_i+\sum_k x_k=\sum_j\beta_j.Q_j+\sum_l y_l$.
Hence ${\cal E}_b\proves P=Q$, and the inductive step follows immediately.
\item[II]
Suppose that both A and B hold. Then, as in case 1.II above,
there exist $i$ and $j$ such that $P_i \braeq Q \braeq P \braeq Q_j$.
Applying the inductive hypothesis to the equivalences $P \braeq Q_j$,
$P_i \braeq Q_j$ and $P_i \braeq Q$,
we infer that, for all $\gamma\in A_\tau$,
\[
{\cal E}_b \proves \gamma.P = \gamma . Q_j = \gamma . P_i = \gamma . Q
\]
and the inductive step follows.
\item[III]
Suppose that only one of A and B holds.
In the remainder of the proof for this case,
we shall assume, without loss of generality, that only A holds.
We distinguish three further sub-cases.
\item[IIIa]
Suppose that A holds for some indices $i_1,i_2$ with $\alpha_{i_1}=\tau$
and $\alpha_{i_2}=a$.
For every $i$ with $\alpha_i\in\{\tau,a\}$ and $P_i\braeq Q$,
induction yields ${\cal E}_b\proves\alpha_i.P_i=\alpha_i.Q$.
Hence, possibly using axioms A3 and/or A4, we infer that
\[
{\cal E} \proves P=a^*(\tau.Q+a.Q+S)
\]
where $S\ACeq \sum\set{\alpha_i . P_i \mid \alpha_i \not\in\set{\tau,a}
~~\mbox{or}~~
P_i \nobis{b}{} Q } + \sum_k x_k$.
Reasoning as in case 1.III above, we find that
${\cal E}_b \proves Q=a^*(R+S)$ for some term $R$. Now
\[
\begin{array}{rcl}
\gamma.P&=&\gamma.a^*(\tau.Q+a.Q+S)\\
&=&\gamma.a^*\Parens{\tau.a^*\Parens{R+S}+a.a^*\Parens{R+S}+S}\\
&\stackrel{\mbox{\tiny \rm PA2}}=&\gamma.a^*\Parens{\tau.a^*a^*\Parens{R+S}+a.a^*\Parens{R+S}+S}\\
&\stackrel{\mbox{\tiny \rm PA1}}=&\gamma.a^*\Parens{\tau.a^*\Parens{R+a.a^*\Parens{R+S}+S}+a.a^*\Parens{R+S}+S}\\
%&\stackrel{\mbox{\tiny \rm A4,B1}}=&\gamma.\tau.a^*\Parens{\tau.a^*\Parens{R+a.a^*\Parens{R+S}+S}+a.a^*\Parens{R+S}+S}\\
&\stackrel{\mbox{\tiny \rm PB2$'$}}=&\gamma.a^*\Parens{R+a.a^*\Parens{R+S}+S}\\
%&\stackrel{\mbox{\tiny \rm A4,B1}}=&\gamma.a^*\Parens{R+a.a^*\Parens{R+S}+S}\\
&\stackrel{\mbox{\tiny \rm PA1}}=&\gamma.a^*a^*(R+S)
~\stackrel{\mbox{\tiny \rm PA2}}=~\gamma.a^*(R+S)~=~\gamma.Q.
\end{array}
\]
\item[IIIb]
Suppose that A holds only for some $i$ with $\alpha_i=\tau$.
Then, reasoning as in the case above, we obtain that
${\cal E}_b \proves P=a^*(\tau.Q+S)$ (i.e., the summand $a.Q$ vanishes), and
${\cal E}_b \proves Q=a^*(R+S)$ for some terms $R$ and $S$.
This yields the following simplification of the argument above:
\[
\begin{array}{rcl}
\gamma.P &=& \gamma.a^*(\tau.Q+S) \\
&=&\gamma.a^*(\tau.a^*(R+S)+S)\\
%&\stackrel{\mbox{\tiny \mbox{\rm A4,B1}}}=&\gamma.\tau.a^*(\tau.a^*(R+S)+S)\\
&\stackrel{\mbox{\tiny \mbox{\rm PB2$'$}}}=&\gamma.a^*(R+S)\\
%&\stackrel{\mbox{\tiny \mbox{\rm A4,B1}}}=&\gamma.a^*(R+S)\\
&=&\gamma.Q \enspace .
\end{array}
\]
\item[IIIc]
Suppose that A holds only for some $i$ with $\alpha_i=a$.
Then, reasoning as in case IIIa above, we infer that
\[
{\cal E}_b \proves P=a^*(a.Q+S)
\]
where $S \ACeq \sum\set{\alpha_i . P_i \mid \alpha_i \neq a
~~\mbox{or}~~
P_i \nobis{b}{} Q } + \sum_k x_k$
(i.e., $\tau.Q$ vanishes).
Since B does not hold, it follows that
every summand $\beta_j.Q_j$ of $Q$ matches with a summand $\alpha_i.P_i$
of $S$, every $y_l$ is equal to an $x_k$, and vice versa. Possibly using
axiom A3, it follows that ${\cal E}_b \proves Q=a^*S$ (i.e., $R$ vanishes). Now
\[
\gamma.P=\gamma.a^*(a.Q+S)=\gamma.a^*(a.a^*S+S)\stackrel{\mbox{\tiny \rm PA1}}=
\gamma.a^*a^*S\stackrel{\mbox{\tiny \rm PA2}}=\gamma.a^*S=\gamma.Q.
\]
\end{itemize}
\item {\sc Case:}
$P\ACeq\sum_i \alpha_i.P_i+\sum_k x_k$ and
$Q\ACeq a^*(\sum_j\beta_j.Q_j+\sum_l y_l)$.
Consider the following two conditions:
\begin{itemize}
\item[A.]
$\alpha_i\in\{\tau,a\}$ and $P_i\braeq Q$ for some $i$;
\item[B.]
$\beta_j\in\{\tau,a\}$ and $Q_j\braeq P$ for some $j$.
\end{itemize}
Since $Q\mv{a}Q$ and $P\braeq Q$, it follows that $P\mvt{a}P'$
with $P'\braeq Q$, for some $P'$. By the Stuttering Lemma
\ref{Lem.stuttering}, the intermediate states in the derivation $P\mvt{a}P'$
are all branching equivalent to $Q$. Hence there exists an index $i$
such that $\alpha_{i}\in\{\tau,a\}$
and $P_{i}\braeq Q$. So we know that $A$ holds. We proceed by distinguishing
two sub-cases, depending on whether B holds or not.
\begin{itemize}
\item[I]
Suppose that B holds, so $Q_j\braeq P$ for some $j$.
Then $Q_j\braeq P_{i}$ also holds, and the inductive hypothesis yields
${\cal E}_b\proves\gamma.P=\gamma.Q_j=\gamma.P_{i}=\gamma.Q$,
for all $\gamma\in A_\tau$, as desired.
\item[II]
Suppose B does not hold. Reasoning as in case 2.III above,
we can distinguish three sub-cases:
\begin{itemize}
\item
A holds for some indices $i_1$ and $i_2$ with $\alpha_{i_1}=\tau$ and
$\alpha_{i_2}=a$.
Then, for some terms $R$ and $S$,
${\cal E}_b \proves P=\tau.Q+a.Q+S$ and ${\cal E}_b\proves Q=a^*(R+S)$.
\item
A holds only for some index $i$ such that $\alpha_i=\tau$.
Then, for some terms $R$ and $S$,
${\cal E}_b\proves P=\tau.Q+S$ and ${\cal E}_b\proves Q=a^*(R+S)$.
\item
A holds only for some index $i$ such that $\alpha_i=a$.
Then, for some term $S$, ${\cal E}_b\proves P=a.Q+S$, and, since B does not
hold, we find that ${\cal E}_b\proves Q=a^*S$.
\end{itemize}
In all three cases we obtain
${\cal E}_b\proves\gamma.P=\gamma.Q$, reasoning just as in case 2.III,
but skipping the applications of PA2 and using B1 (in the second case with PA1)
instead of PB2$'$.
\end{itemize}
\end{enumerate}
The proof of the inductive step is now complete.
\end{proof}
\begin{theorem}%[Completeness for Branching Congruence]
\label{Thm:branching-completeness}
Let $P,Q\in\OMPAdef$.
If $P \bracong Q$, then ${\cal E}_b \proves P = Q$.
\end{theorem}
\begin{proof}
Consider two process terms $P$ and $Q$ that are branching
congruent. We shall prove that ${\cal E}_b \proves P = P+Q = Q$, from which
the claim follows. In fact, by symmetry, it is sufficient to show that
if $P \bracong Q$, then ${\cal E}_b \proves P = P+Q$.
To this end, note, first of all, that, by Lem.~\ref{Lem:normalforms},
$P$ and $Q$ may be proven equal to some normal forms using equations A4, PA1
and PB1.
%{Lem.headnormalform} gives
Possibly using equation PA1 again, we may therefore derive that
\[
\begin{array}{l}
{\cal E}_b \proves P = \sum\set{ \alpha_i. P_i \mid i \in I} +
%P \mv{\alpha_i} P_i} +
\sum\set{ x_j \mid j\in J}
% P \mv{x_j} x_j}
~~~\mbox{and} \\
{\cal E}_b \proves Q = \sum\set{ \beta_k. Q_k \mid k \in K} +
% + Q \mv{\beta_k} Q_k} +
\sum\set{ y_l \mid l\in L}
%Q \mv{y_l} y_l}
\end{array}
\]
for some finite index sets $I, J, K, L$.
As $P\bracong Q$ and the equations in ${\cal E}_b$ are sound with
respect to branching congruence, it follows that
\begin{enumerate}
\item for every $k$ there exists an index $i_k$ such that $\alpha_{i_k} = \beta_{k}$
and $P_{i_k} \braeq Q_k$, and
\item for every $l$ there exists an index $j_l$ such that $x_{j_l} \syneq y_l$.
\end{enumerate}
By Propn.~\ref{Propn:prove-nf}, for every $k$ we may infer that
\[
{\cal E}_b \proves \alpha_{i_k}.P_{i_k} = \alpha_{i_k}.Q_k = \beta_k.Q_k
\enspace .
\]
The fact that ${\cal E}_b \proves P = P+Q$ is now immediate using axiom A3.
\end{proof}
\subsection{Completeness for $\eta$-, delay, and weak congruence}
We now proceed to derive completeness results for $\eta$-, delay, and
weak congruence from Thm.~\ref{Thm:branching-completeness}. The key
to this derivation is the observation that, for certain classes of process
terms, these congruence relations coincide with branching congruence.
These classes of process terms are defined below.
\begin{definition}\label{Def:saturated}
We say that a term $P$ is:
\begin{itemize}
\item {\em $\eta$-saturated} iff for each of its derivatives $Q,~R$ and $S$
and $\xi \in A_\tau \cup \Vardef$ we have that:
\[
Q \mv{\xi} R \mv{\tau} S \mbox{ implies } Q \mv{\xi} S.
\]
\item {\em $d$-saturated} iff for each of its derivatives $Q,~R$ and $S$
and $\xi \in A_\tau \cup \Vardef$ we have that:
\[
Q \mv{\tau} R \mv{\xi} S \mbox{ implies } Q \mv{\xi} S.
\]
\item {\em $w$-saturated} iff it is both $\eta$- and $d$-saturated.
\end{itemize}
\end{definition}
The following theorem was first shown in \cite{GW90} for process graphs.
Here, we present its adaptation to open terms in the language $\OMPA$.
\begin{theorem}\label{Thm:saturated}
Let $\wild\in\set{\eta,d,w}$.
If $P$ and $Q$ are $\wild$-saturated and $P \bis{\wild}{c} Q$,
then $P \bracong Q$.
\end{theorem}
\begin{proof}
We only present the proof for weak congruence. The proofs for
$\eta$- and delay congruence are simple variations on this theme, and
the interested reader will have no difficulty in reconstructing them.
Note, first of all,
that any two $w$-saturated terms that are
weakly equivalent are also branching equivalent. This follows
because the relation
\begin{eqnarray*}
\Rel{B} & \deq & \set{ (S,T) \mid S \obseq T,~~\mbox{$S,T$ $w$-saturated} }
\end{eqnarray*}
is a branching bisimulation.
Now, assume that $P \obscong Q$ and that $P \mv{\xi} P'$.
Then, there exists a $Q'$ such that $Q \mvt{\xi} Q'$ and
$P' \obseq Q'$. As $Q$ is $w$-saturated, it follows that
$Q \mv{\xi} Q'$. Since $P'$ and $Q'$ are $w$-saturated and weakly equivalent,
we infer that $P' \braeq Q'$. Therefore, by symmetry, we finally obtain that
$P \bracong Q$, which was to be shown.
\end{proof}
\begin{proposition}\label{Propn:saturated}
Let $\wild\in\set{\eta,d,w}$. For each term $P$,
${\cal E}_\wild \proves P = P'$ for some $\wild$-saturated
term $P'$.
\end{proposition}
\begin{proof}
Again, we only present the details of the proof for $\wild = w$.
The proofs of $\eta$- and $d$-saturation are simple variations on this theme, and
the interested reader will have no difficulty in reconstructing them.
A term $P$ is {\em in head normal form} if it has the following
form, where $I,J$ are finite index sets:
\[
P \ACeq \sum_{i\in I} \alpha_i . P_i + \sum_{j\in J} x_j \enspace .
\]
By induction on the structure of a process term $T$, we show that
$T$ can be proven equal to a process term that is both $w$-saturated and
in head normal form, using the axiom system ${\cal E}_w$.
The cases $T \equiv x$ and $T\equiv 0$ are trivial.
\begin{itemize}
\item {\sc Case:} $T \equiv P+Q$. By the inductive hypothesis,
$P$ and $Q$ can be transformed into $w$-saturated terms $P'$ and
$Q'$ in head normal form, respectively. Then
$T$ is provably equal to
$P'+Q'$, which is a $w$-saturated term, and may be turned into
head normal form by possibly using A4.
\item {\sc Case:} $T \equiv a.P$. By the inductive hypothesis, $P$ can be
proven equal to a $w$-saturated term
\[
P'\ACeq \sum_{i\in I}b_i . P_i + \sum_{j\in J}\tau . Q_j +
\sum_{k \in K} x_k \enspace .
\]
By AT3, $T$ is provably equal to
\[
T'\ACeq a.P' + \sum_{j\in J}a.Q_j \enspace .
\]
We show that $T'$ is $w$-saturated.
Since $P'$ and its derivatives are
$w$-saturated, we only need to check the $w$-saturation condition
for $T'$ itself.
Note that the case $T'\mv{\tau}R\mv{\xi}S$ does not apply.
Assume that $T'\mv{\xi} R\mv{\tau} S$. Then $\xi=a$, and
$R$ is either $P'$ or $Q_j$ for some $j \in J$.
If $R\equiv P'$, then $S\equiv Q_{j'}$ for some $j'\in J$. Therefore
$T' \mv{a} S$ follows.
If $R\equiv Q_j$, then $P'\mv{\tau}R\mv{\tau}S$. Since
$P'$ is $w$-saturated, it follows that $P'\mv{\tau} S$.
Hence $S\equiv Q_{j'}$ for some $j' \in J$, and $T'\mv{a} S$ follows.
\item {\sc Case:} $T \equiv \tau. P$. By induction, $P$ is provably
equal to a $w$-saturated term
\[
P' \ACeq \sum_{i\in I}\alpha_i . P_i + \sum_{j\in J} x_j \enspace .
\]
By T2, $T$ is provably equal to $T'\equiv\tau.P' + P'$.
We show that $T'$ is $w$-saturated. Since $P'$ and its derivatives
are $w$-saturated, we only need to check the $w$-saturation
condition for transitions emanating from $T'$ itself.
We distinguish three possibilities.
Assume that $T'\mv{\tau}P'\mv{\xi}Q$. Then $T'\mv{\xi}Q$ follows
immediately.
Assume that $T'\mv{\tau}P_i\mv{\xi}Q$ for some $i\in I$ with
$\alpha_i=\tau$.
Then $P'\mv{\tau}P_i\mv{\xi}Q$, and, as $P'$ is
$w$-saturated, it follows that $P'\mv{\xi}Q$.
Hence $T'\mv{\xi}Q$, as desired.
Assume that $T'\mv{\alpha_i}P_i\mv{\tau}Q$ for some $i\in I$.
Then $P'\mv{\alpha_i}P_i\mv{\tau}Q$. As $P'$ is $w$-saturated, it
follows that $P'\mv{\alpha_i}Q$. Thus $T'\mv{\alpha_i}Q$, as desired.
\item {\sc Case:} $T \equiv a^*P$. By induction, $P$ is provably
equal to a $w$-saturated term
\[
P' \ACeq \sum_{i\in I}b_i . P_i + \sum_{j\in J} \tau. Q_j
+ \sum_{k\in K} x_k \enspace .
\]
Now,
\[
T \stackrel{\mbox{\tiny PT3}}{=} a^*(P' + \sum_{j\in J} a. Q_j)
\stackrel{\mbox{\tiny PA1}}{=} a.a^*(P' + \sum_{j\in J} a . Q_j)
+ P' + \sum_{j \in J}a.Q_j \deq_{\mbox{\tiny\rm AC}} T' \enspace .
\]
% By Lem.~\ref{Lem:derivable-equations},
% \[
% {\cal E}_w \proves T=a^*P'+\sum_{j\in J}a.Q_j
% \stackrel{\mbox{\tiny \rm PA1}}=a.a^* P'+P'+\sum_{j \in J}a.Q_j
% \enspace .
% \]
% By PT3, $T$ is provably equal to
% \[
% T' \ACeq a.a^*(P' + \sum_{j\in J} a . Q_j)
% + P' + \sum_{j \in J}a.Q_j \enspace .
% \]
We show that $T'$ is $w$-saturated.
All derivatives other than $T'$ itself and $S \equiv
a^*(P' + \sum_{j\in J}a . Q_j)$ are $w$-saturated by assumption,
so we only need deal with these two cases. First, we deal with $T'$.
\begin{list}{$\bullet$}{\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 4pt \itemsep 2pt \parsep 2pt}
\item Let $T' \mv{\xi} Q \mv{\tau} R$. There are three possibilities:
\begin{list}{{\bf --}}{\leftmargin 15pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 2pt \itemsep 2pt \parsep 0pt}
\item $\xi=a$ and $Q\equiv S$. Then $R\equiv Q_j$ for some $j\in J$,
and thus $T' \mv{a} R$.
\item $P' \mv{\xi} Q \mv{\tau} R$. In that case $P' \mv{\xi} R$
since $P'$ is $w$-saturated, and thus $T' \mv{\xi} R$ follows.
\item $\xi=a$ and $Q\equiv Q_j$ for some $j \in J$.
In that case $P'\mv{\tau}Q_j\mv{\tau}R$. Thus
$P'\mv{\tau} R$, since $P'$ is $w$-saturated. Hence $R\equiv Q_{j'}$ for
some $j'\in J$. Again $T' \mv{a} R$ follows.
\end{list}
\item Let $T' \mv{\tau} Q \mv{\xi} R$. Then $P' \mv{\tau} Q
\mv{\xi} R$. Thus $P' \mv{\xi} R$, since $P'$ is $w$-saturated, and
$T' \mv{\xi} R$ follows.
\end{list}
Next, we deal with $S$.
\begin{list}{$\bullet$}{\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 4pt \itemsep 2pt \parsep 2pt}
\item Let $S \mv{\xi} Q \mv{\tau} R$. There are three possibilities:
\begin{list}{{\bf --}}{\leftmargin 15pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 2pt \itemsep 2pt \parsep 0pt}
\item $\xi=a$ and $Q\equiv S$. Then $R\equiv Q_j$ for some $j \in J$, and $S \mv{a} R$.
\item $P' \mv{\xi} Q \mv{\tau} R$. In that case $S \mv{\xi} R$
since $P'$ is $w$-saturated.
\item $\xi=a$ and $Q\equiv Q_j$ for some $j \in J$.
In that case $P'\mv{\tau}Q_j\mv{\tau}R$; therefore
$P'\mv{\tau} R$, since $P'$ is $w$-saturated. Hence $R\equiv Q_{j'}$ for
some $j'\in J$. Again $S\mv{a} R$ follows.
\end{list}
\item Let $S \mv{\tau} Q \mv{\xi} R$. Then $P' \mv{\tau} Q
\mv{\xi} R$, and, since $P'$ is $w$-saturated, $S \mv{\xi} R$
follows.
\end{list}
\item {\sc Case:} $T \equiv \tau^*P$. Application of PT1 reduces this
case to the one $T \equiv \tau.P$.
\end{itemize}
This completes the inductive argument.
\end{proof}
\noindent
In light of Propn.~\ref{Propn:relative}, the results in
Thm.~\ref{Thm:saturated} and Propn.~\ref{Propn:saturated} effectively
reduce the completeness problem for $\eta$-, delay, and weak
congruence over $\OMPA$ to that for branching congruence.
\begin{corollary}\label{Cor:other-completeness}
Let $\wild\in\set{\eta,d,w}$. If
$P\bis{\wild}{c}Q$, then ${\cal E}_\wild \proves P = Q$.
\end{corollary}
\begin{proof}
Let $\wild\in\set{\eta,d,w}$. Suppose that $P \bis{\wild}{c} Q$.
Prove $P$ and $Q$ equal to $\wild$-saturated processes $P'$ and $Q'$,
respectively (Propn.~\ref{Propn:saturated}). By the soundness of the
axiom system ${\cal E}_\wild$ (Propn.~\ref{Propn:soundness}), $P'$ and $Q'$
are $\wild$-congruent. It follows that $P'$ and $Q'$ are branching
congruent (Thm.~\ref{Thm:saturated}).
Hence, by Thm.~\ref{Thm:branching-completeness},
${\cal E}_b\proves P' = Q'$.
The claim now follows because, by Propn.~\ref{Propn:relative},
the axioms for branching congruence are derivable from the theory
${\cal E}_\wild$.
\end{proof}
\subsection{Comparison of proof strategies}
The $\omega$-completeness results for branching, delay, and
$\eta$-congruence that we have just obtained, are all new.
The $\omega$-completeness of the axiomatization for weak congruence was
proven earlier in \cite{AI95}, under the assumption that the set of actions
$A$ be countably infinite. The proof presented in this paper applies to
any non-empty action set. While in this study we have obtained the
completeness result for weak congruence via
that for branching congruence, in {\sl op.~cit.}~a direct proof strategy was
employed, based on structural induction. It turns out that the direct
proof method yields a long and tedious proof, with many case distinctions.
The indirect proof via branching congruence, which we presented here,
is considerably shorter, and relies on a general relationship between the two
congruences. %Apparently, weak congruence can have a raw surface,
%which is approached more easily after it has been treated
%with a cream of branching congruence.
It should be noted, however, that delicate case analyses appear to be
inescapable components of completeness proofs for equational axiomatizations
of behavioural congruences over variations on Kleene algebras (cf., {\eg},
the proofs in \cite{FZ94,Fok94,AI95,Fok95,AG95}). In the approach followed
in this paper, the use of a detailed case analysis is limited to the proof
of Propn.~\ref{Propn:prove-nf}, which is the key to the completeness theorem
for branching congruence, and to the saturation procedures employed in the
proof of Propn.~\ref{Propn:saturated}. In both cases, the case analysis
is guided by operational, rather than purely syntactic, considerations.
A second, less vital distinction between our proof and that from
\cite{AI95}, is that there first completeness was proved, and then
a proof strategy from \cite{Gr90} was used to obtain $\omega$-completeness.
Here, we gave operational semantics to open terms,
instead of closed terms, and deduced completeness and $\omega$-completeness
at the same time. This method could have been employed in \cite{AI95}
just as well.
%%% End of the main body of the paper
%\bibliographystyle{siam}
%\bibliography{abbreviations,dbase}
\begin{thebibliography}{10}
\vspace{-1pt}
\bibitem{ABV94}
{\sc L.~Aceto, B.~Bloom and F.~Vaandrager}, {\em Turning {SOS} rules into
equations}, Information and Computation 111 (1994), pp.~1--52.
\vspace{-1pt}
\bibitem{AG95}
{\sc L.~Aceto and J.F.~Groote}, {\em A complete equational axiomatization for
{MPA} with string iteration}, Research Report RS--95--28, BRICS (Basic
Research in Computer Science, Centre of the Danish National Research
Foundation), Department of Mathematics and Computer Science, Aalborg
University, May 1995.
\newblock Available by anonymous ftp from {\tt ftp.daimi.aau.dk} in the
directory {\tt pub/BRICS/RS/95/28}.
\vspace{-1pt}
\bibitem{AI95}
{\sc L.~Aceto and A.~Ing\'{o}lfsd\'{o}ttir}, {\em A complete equational
axiomatization for prefix iteration with silent steps}, Research Report
RS--95--5, BRICS (Basic Research in Computer Science, Centre of the Danish
National Research Foundation), Department of Mathematics and Computer
Science, Aalborg University, Jan. 1995.
\newblock Available by anonymous ftp from {\tt ftp.daimi.aau.dk} in the
directory {\tt pub/BRICS/RS/95/5}.
\vspace{-1pt}
\bibitem{BBK87a}
{\sc J.~Baeten, J.~Bergstra and J.~Klop}, {\em On the consistency of
Koomen's fair abstraction rule}, Theoretical Comput. Sci.~51 (1987),
pp.~129--176.
\vspace{-1pt}
\bibitem{BG87}
{\sc J.~Baeten and R.~v. Glabbeek}, {\em Another look at abstraction in process
algebra}, in Proceedings $14^{th}$ ICALP, {\rm Karlsruhe}, T.~Ottmann, ed.,
vol.~267 of Lecture Notes in Computer Science, Springer-Verlag, July 1987,
pp.~84--94.%
\vspace{-1pt}
\bibitem{CONCUR90}
{\sc J.~Baeten and J.~Klop}, eds., {\em Proceedings CONCUR 90, {\rm
Amsterdam}}, vol.~458 of Lecture Notes in Computer Science, Springer-Verlag,
1990.
\vspace{-1pt}
\bibitem{Bas95}
{\sc T.~Basten}, {\em Branching bisimulation is an equivalence indeed!}
\newblock Unpublished manuscript.
\vspace{-1pt}
\bibitem{BBP94}
{\sc J.~Bergstra, I.~Bethke and A.~Ponse}, {\em Process algebra with iteration
and nesting}, Computer Journal 37 (1994), pp.~243--258.
\vspace{-1pt}
\bibitem{BK84}
{\sc J.~Bergstra and J.~Klop}, {\em The algebra of recursively defined
processes and the algebra of regular processes}, in Proceedings $11^{th}$
ICALP, {\rm Antwerpen}, J.~Paredaens, ed., vol.~172 of Lecture Notes in
Computer Science, Springer-Verlag, 1984, pp.~82--95.
%\vspace{-1pt}
%\bibitem{BK84b}
%\leavevmode\vrule height 2pt depth -1.6pt width 23pt, {\em Process algebra for
% synchronous communication}, Information and Computation, 60 (1984),
% pp.~109--137.
%\vspace{-1pt}
\bibitem{Bl95}
{\sc B.~Bloom}, {\em Structural operational semantics for weak bisimulations},
Theoretical Comput. Sci.~146 (1995), pp.~25--68.
\vspace{-1pt}
\bibitem{CEW58}
{\sc I.~Copi, C.~Elgot and J.~Wright}, {\em Realization of events by logical
nets}, Journal of the ACM 5 (1958), pp.~181--196.
\vspace{-1pt}
\bibitem{CDL95}
{\sc F.~Corradini, R.~De~Nicola and A.~Labella}, {\em Fully abstract models
for nondeterministic {Kleene} algebras (extended abstract)}, in Proceedings
CONCUR 95, {\rm Philadelphia, PA, USA}, I.~Lee and S.~Smolka, eds., vol.~962
of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp.~130--144.%
\vspace{-1pt}
\bibitem{DL94}
{\sc R.~De~Nicola and A.~Labella}, {\em A completeness theorem for
nondeterministic {Kleene} algebras}, in Proceedings of MFCS '94,
Ko\v{s}ice, Slovakia, I.~Pr\'{\i}vara, B.~Rovan and P.~Pu\v{z}i\v{c}ka, eds.,
vol.~841 of Lecture Notes in Computer Science, Springer-Verlag, 1994.
\vspace{-1pt}
\bibitem{DMV90}
{\sc R.~De~Nicola, U.~Montanari and F.~Vaandrager}, {\em Back and forth
bisimulations}, in Baeten and Klop \cite{CONCUR90}, pp.~152--165.
\vspace{-1pt}
\bibitem{Fok94}
{\sc W.~Fokkink}, {\em A complete equational axiomatization for prefix
iteration}, Inf. Process. Lett.~52 (1994), pp.~333--337.
\vspace{-1pt}
\bibitem{Fok95}
\leavevmode\vrule height 2pt depth -1.6pt width 23pt, {\em A complete
axiomatization for prefix iteration in branching bisimulation}, Logic Group
Preprint Series 126, Dept.~of Philosophy, Utrecht University, Jan. 1995.
\newblock To appear in {\em Fundamenta Informaticae}. Available by
ftp from {\tt ftp.phil.ruu.nl} as {\tt logic/PREPRINTS/preprint126.ps.Z}.
\vspace{-1pt}
\bibitem{FZ94}
{\sc W.~Fokkink and H.~Zantema}, {\em Basic process algebra with iteration:
Completeness of its equational axioms}, Computer Journal 37 (1994),
pp.~259--267.
\vspace{-1pt}
\bibitem{vG93}
{\sc R.~v. Glabbeek}, {\em A complete axiomatization for branching bisimulation
congruence of finite-state behaviours}, in Mathematical Foundations of
Computer Science 1993, {\rm Gdansk, Poland}, A.~Borzyszkowski and
S.~Soko{\l}owski, eds., vol.~711 of Lecture Notes in Computer Science,
Springer-Verlag, 1993, pp.~473--484.
\newblock Available by anonymous ftp from {\tt Boole.stanford.edu} as
{\tt pub/DVI/complete.dvi.gz}.
\vspace{-1pt}
\bibitem{GW89}
{\sc R.~v. Glabbeek and W.~Weijland}, {\em Branching time and abstraction in
bisimulation semantics (extended abstract)}, in Information Processing 89,
G.~Ritter, ed., North-Holland, 1989, pp.~613--618.
\newblock Full paper available as: %Report CS-R9120, CWI, Amsterdam, 1991.
\vspace{-1pt}
\bibitem{GW90}
\leavevmode\vrule height 2pt depth -1.6pt width 23pt, {\em Branching time and
abstraction in bisimulation semantics}, Technical Report TUM-I9052,
SFB-Bericht Nr.\ 342/29/90 A, Institut f\"{u}r Informatik, Technische
Universit\"{a}t M\"{u}nchen, Germany, 1990.
\newblock Extended abstract appeared as \cite{GW89}. To appear in {\em Journal
of the ACM}.
\vspace{-1pt}
\bibitem{Gr90}
{\sc J.F.~Groote}, {\em A new strategy for proving $\omega$--completeness with
applications in process algebra}, in Baeten and Klop \cite{CONCUR90},
pp.~314--331.
\vspace{-1pt}
\bibitem{He81}
{\sc M.~Hennessy}, {\em A term model for synchronous processes}, Information
and Control 51 (1981), pp.~58--75.
\vspace{-1pt}
\bibitem{He84}
\leavevmode\vrule height 2pt depth -1.6pt width 23pt, {\em Axiomatising finite
delay operators}, Acta Inf.~21 (1984), pp.~61--88.
\vspace{-1pt}
\bibitem{HM85}
{\sc M.~Hennessy and R.~Milner}, {\em Algebraic laws for nondeterminism and
concurrency}, Journal of the ACM 32 (1985), pp.~137--161.
\vspace{-1pt}
\bibitem{Ke76}
{\sc R.~Keller}, {\em Formal verification of parallel programs}, Comm. ACM 19
(1976), pp.~371--384.
\vspace{-1pt}
\bibitem{Kleene56}
{\sc S.~Kleene}, {\em Representation of events in nerve nets and finite
automata}, in Automata Studies, C.~Shannon and J.~McCarthy, eds., Princeton
University Press, 1956, pp.~3--41.
\vspace{-1pt}
\bibitem{Mi81}
{\sc R.~Milner}, {\em A modal characterisation of observable machine
behaviour},
in Proceedings CAAP 81, G.~Astesiano and C.~Bohm, eds., vol.~112 of Lecture
Notes in Computer Science, Springer-Verlag, 1981, pp.~25--34.
\vspace{-1pt}
\bibitem{Mi89}
\leavevmode\vrule height 2pt depth -1.6pt width 23pt, {\em Communication and
Concurrency}, Prentice-Hall International, Englewood Cliffs, 1989.
\vspace{-1pt}
\bibitem{Mi89a}
\leavevmode\vrule height 2pt depth -1.6pt width 23pt, {\em A complete
axiomatisation for observational congruence of finite-state behaviours},
Information and Computation 81 (1989), pp.~227--247.
\vspace{-1pt}
\bibitem{Pa81}
{\sc D.~Park}, {\em Concurrency and automata on infinite sequences}, in
$5^{th}$ GI Conference, {\rm Karlsruhe, Germany}, P.~Deussen, ed., vol.~104
of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp.~167--183.
\vspace{-1pt}
\bibitem{Pl81}
{\sc G.~Plotkin}, {\em A structural approach to operational semantics}, Report
DAIMI FN-19, Computer Science Department, Aarhus University, 1981.%
\vspace{-1pt}
\bibitem{Sew94}
{\sc P.~Sewell}, {\em Bisimulation is not finitely (first order) equationally
axiomatisable}, in Proceedings $9^{th}$ Annual Symposium on Logic in Computer
Science, {\rm Paris, France}, IEEE Computer Society Press, 1994, pp.~62--70.
\vspace{-1pt}
\bibitem{Taylor}
{\sc W.~Taylor}, {\em Equational logic}, Appendix 4 of the book
Universal Algebra by G. Gr\"atzer, Springer-Verlag, 1979, pp.~378--400.
\end{thebibliography}
\end{document}
%%%% Relative independence arguments by Wan %%%%
\iffalse
\begin{enumerate}
\item The reason why equation PT1 is not derivable from the theory
${\cal E}_w\setminus\set{\mbox{PT1}}$ is that PT1
is the only equation that can be used to
eliminate occurrences of the operation $\tau^*$ from terms.
This intuition is captured in the following interpretation $\rho$
of process terms in the natural numbers:
\[
\begin{array}{lcl}
\rho(x)&=&0\\
\rho(0)&=&0\\
\rho(\alpha.P)&=&\rho(P)\\
\rho(P+Q)&=&\max\{\rho(P),\rho(Q)\}\\
\rho(a^*P)&=&\rho(P)\\
\rho(\tau^*P)&=&\rho(P)+1
\end{array}
\]
It is not difficult to see that the interpretation $\rho$ is a model
for ${\cal E}_w\setminus\set{\mbox{PT1}}$. However,
$\rho(\tau^*P)=\rho(P)+1\not=\rho(P)=\rho(\tau.P)$.
\item If $P=Q$ is provable without PT2, and in all subterms $a^*R$ of $P$,
the term $R$ does not contain summands of the form $\tau.S$ nor
$\tau^*S$, then the same holds for $Q$.
This follows because it holds for the axioms in ${\cal E}_w$,
apart from PT2, and moreover no axiom contains a variable $x$ on one side
that does not also occur on the other side. Hence, PT2 cannot be
derivable from ${\cal E}_w\setminus\set{\mbox{PT2}}$.
\item If $P=Q$ is provable without PT3, and $P$ contains a subterm $a^*R$
where $R$ is free of *-operators,
then $Q$ contains a subterm $a^*S$ where $R$ and $S$ are weakly
equivalent. This follows because it holds for the other axioms, and
as above, no variables are lost in the axioms.
Hence, PT3 cannot be derivable
from ${\cal E}_w\setminus\set{\mbox{PT3}}$.
\end{enumerate}
\fi
%%%%% The rewriting stuff from Wan %%%
\noindent
We want to construct a subset of process terms of a special form,
which will be convenient in the proof of the completeness result
for branching congruence. This can be done quite easily by an inductive
definition. However, we opt for a more elegant, but somewhat more involved
method, taken from \cite{FZ95}, which is based on term rewriting.
\begin{figure}[htb]
\centering
$
\begin{array}{rcl}
x+0&\longrightarrow&x\\
\tau^*x&\longrightarrow&\tau.x+x\\
a^*x+y&\longrightarrow&a.a^*x+x+y\\
b^*(a^*x)&\longrightarrow&b^*(a.a^*x+x)\\
\end{array}
$
\caption{The rewrite system ${\cal R}_0$}
\label{tab.rew}
\end{figure}
Figure \ref{tab.rew} contains a rewrite system ${\cal R}_0$ for terms
in $\OMPA$, which eliminates redundant zeros and expressions $\tau^*x$,
and which reduces occurrences of prefix iteration in the context
of alternative composition and of prefix iteration.
The rewrite rules are to be interpreted modulo AC of the +.
It is easy to see that the normal forms of ${\cal R}_0$, i.e.\ the
process terms that cannot be
reduced by the rewrite rules in ${\cal R}_0$, have one of the following
two forms:
\[
\sum_i\alpha_i.P_i+\sum_j x_j~~~~~\mbox{\rm or}~~~~~
a^*(\sum_i\alpha_i.P_i+\sum_j x_j),
\]
where the $P_i$ are normal forms of ${\cal R}_0$.
(Recall that the empty sum represents 0.)
In the completeness proof it will be shown that if two
normal forms $P$ and $Q$ of ${\cal R}_0$ are branching equivalent, then
$\alpha.P=\alpha.Q$. In order to obtain completeness for the full
class of process terms, we will desire to know that each
process term is provably equal to a normal form.
Since the rewrite rules in ${\cal R}_0$ are all derivable from the axioms
(A4, PB1 and PA1), this fact follows if we know that ${\cal R}_0$
is terminating, which means that there are no infinite reductions.
\begin{proposition}
${\cal R}_0$ is terminating.
\end{proposition}
\begin{proof}
We apply the technique of dummy elimination from Ferreira and Zantema
\cite{FeZa94}. First, we give a brief description of this technique.
Suppose that a function symbol $f$ occurs only at the right-hand sides of
the rewrite rules in a rewrite system ${\cal R}$.
Dummy elimination enables to remove $f$ from rules in ${\cal R}$ as follows.
First, introduce a new constant $\Delta$. If a rule in ${\cal R}$ is
of the form $t\longrightarrow C[f(t_1,...,t_n)]$, where $C[]$ is some
context, then replace this rule by the following collection of rules:
\[
\begin{array}{rcl}
t&\longrightarrow&C[\Delta]\\
t&\longrightarrow&t_1\\
&\vdots\\
t&\longrightarrow&t_n.
\end{array}
\]
Apply this procedure in order to remove all occurrences of $f$ in ${\cal R}$.
Let $E({\cal R})$ denote the resulting rewrite system.
The main theorem from \cite{FeZa94} says that
termination of $E({\cal R})$ implies termination of ${\cal R}$.
Dummy elimination can be applied also if ${\cal R}$
contains infinitely many rules.
In Ferreira \cite{Fer95}, dummy elimination has been extended to the
setting of rewriting modulo associativity and commutativity of an operator.
\begin{figure}[htb]
\centering
$
\begin{array}{rcl}
x+0&\longrightarrow&x\\
\tau^*x&\longrightarrow&\tau.x+x\\
a^*x+y&\longrightarrow&\Delta+x+y\\
a^*x+y&\longrightarrow&a^*x\\
b^*(a^*x)&\longrightarrow&b^*(\Delta+x)\\
b^*(a^*x)&\longrightarrow&a^*x\\
\end{array}
$
\caption{${\cal R}_0$ after dummy elimination}
\label{tab.dummy}
\end{figure}
In the case of the rewrite system ${\cal R}_0$, dummy elimination
can be applied to remove the prefixing operator $a.\_$ for $a\in A$.
The rewrite system which results after dummy elimination is presented in
Figure \ref{tab.dummy}. Define a weight function as follows.
\[
\begin{array}{rcl}
w(\Delta)&=&0\\
w(0)&=&1\\
w(P+Q)&=&w(P)+w(Q)\\
w(\alpha.P)&=&w(P)+1\\
w(\alpha^*P)&=&2w(P)+2.
\end{array}
\]
The weight of terms strictly decreases under application of the rewrite
rules. Note that terms which are equal modulo AC of the + have
the same weight. Hence, the rewrite system in Table \ref{tab.dummy} is
terminating modulo AC of the +. So ${\cal R}_0$ is also terminating
modulo AC of the +.
\end{proof}