\documentclass[10pt,twocolumn]{article} % Fontsize 11 point
\usepackage{amssymb}
\usepackage{url}
\usepackage{times}

\setlength{\textwidth}{6.875in} \setlength{\columnsep}{0.375in}
\setlength{\oddsidemargin}{-.1875in}
\setlength{\textheight}{8.875in} \setlength{\topmargin}{0in}
\setlength{\headheight}{0in} \setlength{\headsep}{0in}
\setlength{\parindent}{12pt} \makeatletter
\newcommand\sublarge{\@setfontsize\sublarge\@xipt{13}}
\def\@seccntformat#1{\csname the#1\endcsname.~~}
\def\section{\@startsection {section}{1}{0pt}{-3.25ex plus -1ex minus
   -.2ex}{1.5ex plus .2ex}{\large\bf}}
\def\subsection{\@startsection {subsection}{2}{0pt}{-2ex plus -1ex minus
   -.2ex}{1.5ex plus .2ex minus .3ex}{\sublarge\bf}}
\long\def\@makecaption#1#2{
   \setbox\@tempboxa\hbox{\sf\bf #1. #2}
   \ifdim \wd\@tempboxa >\hsize   % IF longer than one line:
       \sf\bf #1. #2\par          %   THEN set as ordinary paragraph.
     \else                        %   ELSE  center.
       \hbox to\hsize{\hfil\box\@tempboxa\hfil}
   \fi
      \vskip 8pt }
\makeatother \frenchspacing

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

\newenvironment{definition}{\begin{defi} \rm }{\end{defi}}
\newenvironment{theorem}{\begin{theo} \rm }{\end{theo}}
\newenvironment{proposition}{\begin{prop} \rm }{\end{prop}}
\newenvironment{lemma}{\begin{lemm} \rm }{\end{lemm}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill$\Box$\end{trivlist}}

\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 12pt
   \labelwidth\leftmargini\advance\labelwidth-\labelsep}}{\end{list}}

\newcommand{\mc}[1]{\mathcal{#1}}
\newcommand{\nil}{\mathbf{0}}
\newcommand{\mv}[1]{\mathrel{\stackrel{#1}{\rightarrow}}}
\newcommand{\bis}{\mathrel{             % bisimulation
    \raisebox{.2ex}{$\underline{\makebox[.8em]{$\leftrightarrow$}}$}}}
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}     % no vertical space

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

\title{{\Large\bf Ready to Preorder: The Case of Weak Process Semantics}\thanks{This work is
partially supported by the Dutch Bsik project BRICKS.}}
   \author{Taolue Chen\\
 \small \sl CWI\\[-3pt]
 \small \sl PO Box 94079, 1090 GB Amsterdam, NL\\[-3pt]
 \small \tt chen@cwi.nl
   \and    Wan Fokkink\\
 \small \sl Vrije Universiteit\\[-3pt]
 \small \sl De Boelelaan 1081a, 1081 HV Amsterdam, NL\\[-3pt]
 \small \tt wanf@cs.vu.nl
 \and    Rob van Glabbeek\\
 \small National ICT Australia, Locked Bag 6016, Sydney, NSW
 1466, Australia  \\ [-3pt]
 \small The University of New South Wales, School of
 \small Computer Science and Engineering,\\[-3pt]
 \small Sydney, NSW 2052, Australia\\[-3pt]
 \small \tt rvg@cs.stanford.edu
\vspace{1ex} }
   \date{}
   \maketitle
\thispagestyle{empty}

{\centering\bf Abstract\\[1ex]}\noindent
  {\em Recently, Aceto, Fokkink \& Ing{\'o}lfsd{\'o}ttir proposed an
algorithm to turn any sound and ground-complete axiomatisation of
any preorder listed in the linear time -- branching time spectrum
at least as coarse as the ready simulation preorder, into a sound
and ground-complete axiomatisation of the corresponding
equivalence---its kernel. Moreover, if the former axiomatisation
is $\omega$-complete, so is the latter. Subsequently, de Frutos
Escrig, Gregorio Rodr\'{\i}guez \& Palomino generalised this
result, so that the algorithm is applicable to any preorder at
least as coarse as the ready simulation preorder, provided it is
initials preserving. The current paper shows that the same
algorithm applies equally well to weak semantics: the proviso of
initials preserving can be replaced by other conditions, such as
weak initials preserving and satisfying the second $\tau$-law.
This makes it applicable to all 87 preorders surveyed in ``the
linear time -- branching time spectrum II" that are at least as
coarse as the ready simulation preorder. We also extend the scope
of the algorithm to infinite processes, by adding recursion
constants. As an application of both extensions, we provide a
ground-complete axiomatisation of the CSP failures equivalence for
BCCS processes with divergence.}

\section{Introduction}

The lack of consensus on what constitutes an appropriate notion of
observable behaviour for reactive systems has led to a large
number of proposals for behavioural equivalences and preorders for
concurrent processes. These have been surveyed in the \emph{linear
time-branching time spectrum}, for concrete semantics
\cite{Gla01}, and for weak semantics that take into account the
internal action $\tau$ \cite{Gla93}. Typically, a given semantical
notion induces both a preorder and an equivalence, where the
equivalence is the kernel of the corresponding preorder, meaning
that two processes are considered equivalent if, and only if, each
is a refinement of the other with respect to the preorder.

For equational reasoning about processes expressed in some process
algebra, an axiomatisation of the semantics under consideration
(both for the preorder and the equivalence) is required. This
axiomatisation should be \emph{sound}, and preferably also
\emph{ground-complete}, for the process algebra modulo the
semantics at hand, meaning that all equivalent closed terms can be
equated. Ideally, such an axiomatisation is also
\emph{$\omega$-complete}, meaning that whenever all closed
instances of an equation can be derived from it, then so can the
equation itself.  \cite{AFIL05,CFLN07,Gro90} offer positive and
negative results on the existence of $\omega$-complete, sound and
ground-complete finite axiomatisations for several concrete
behavioural equivalences and preorders in the spectrum from
\cite{Gla01}, over BCCSP\@.  This process algebra contains only
the basic operators from CCS and CSP, but is sufficiently powerful
to express all finite synchronisation trees.

Such positive and negative axiomatisability results were always
proved separately for a preorder and the corresponding
equivalence. Aceto, Fokkink \& Ing{\'o}lfsd{\'o}ttir \cite{AFI07}
showed that for BCCSP such double effort can be avoided, by
presenting an algorithm to turn a sound and ground-complete
axiomatisation of any preorder in the linear time -- branching
time spectrum at least as coarse as the ready simulation preorder,
into a sound and ground-complete axiomatisation of the
corresponding equivalence.\footnote{Another way to avoid the
double effort is by deriving axiomatisations of preorders from
those of the corresponding equivalences. This line of research is
explored in \cite{FG08}.}  Moreover, if the former axiomatisation
is $\omega$-complete, so is the latter. The requirement that the
preorder is at least as coarse as ready simulation is essential;
in \cite{CF07} it was shown that for impossible futures semantics
(which does not satisfy this requirement), there is a finite
axiomatisation for the preorder, but not for the equivalence.

A serious drawback of the work reported in \cite{AFI07} is that
their algorithm requires several properties to hold for the
preorders to which it is applied, which have to be checked for
each preorder separately. Especially their variable cancellation
property is usually rather hard to prove, see \cite{AFI07b}.
Subsequently, de Frutos Escrig, Gregorio Rodr\'{\i}guez \&
Palomino \cite{FGP08,FGP08b} improved upon this result, so that
the algorithm is applicable not only to those preorders
specifically mentioned in ``the linear time -- branching time
spectrum" but to any preorder at least as coarse as the ready
simulation preorder, provided it is \emph{initials preserving},
meaning that a preorder relation ($p \sqsubseteq q$) implies
inclusion of initial action sets ($I(p) \subseteq I(q)$). This
condition is needed to guarantee soundness of the generated
axiomatisation.

The current paper stems from an effort to apply the algorithm to
weak semantics, which take into account internal activity $\tau$.
The results in \cite{FGP08,FGP08b} do not suffice in this setting,
because weak semantics tend to violate the initials preserving
condition. So a new round of generalisation is needed. To this
end, we show that in the setting of BCCS (BCCSP extended with
$\tau$), the algorithm originally proposed in \cite{AFI07} applies
equally well to weak semantics; the proviso of initials preserving
can be replaced by other conditions. We give three sufficient
conditions on the preorder $\sqsubseteq$ and its corresponding
equivalence $\equiv$: either (1) $p \equiv \tau p$ for all closed
terms $p$; or (2) $p\equiv \tau p$ for all $p$ with $I(p) \neq
\emptyset$, and $p \sqsubseteq q$ with $I(p) \neq \emptyset$
implies $I(q) \neq \emptyset$; or (3) $\tau p \equiv \tau p + p$
for all closed terms $p$, and $\sqsubseteq$ is \emph{weak}
initials preserving.

This makes the algorithm applicable to all 87 preorders surveyed
in ``the linear time -- branching time spectrum II" \cite{Gla93}
that are coarser than the (strong) ready simulation preorder. That
is, each of these preorders satisfies either the original initials
preserving condition from \cite{FGP08,FGP08b}, or one of our three
new conditions.

Moreover, we extend the scope of the algorithm to \emph{infinite}
processes, by adding recursion constants to BCCS. As an
application of both extensions, we provide a ground-complete
axiomatisation of the CSP failures equivalence, also known as
must-testing equivalence, for BCCS processes with divergence.

\section{Preliminaries} \label{sec2}

BCCS is a basic process algebra for expressing finite process
behaviour. Its signature consists of the constant $\nil$, the
binary operator $\_+\_$\,, and unary prefix operators $\tau\_$ and
$a\_$\,, where $a$ is taken from a nonempty set $A$ of
\emph{visible actions}, called the \emph{alphabet}.  We assume
$\tau\!\notin\! A$, $\tau$ being the \emph{hidden action}, and
write $A_\tau$ for $A\cup\{\tau\}$, ranged over by $\alpha,\beta$.
\[ t::= 0 \mid \alpha t \mid t+t \mid x\]
Closed ${\rm BCCS}$ terms, ranged over by $p,q,r$, represent
finite process behaviours, where $\nil$ does not exhibit any
behaviour, $p+q$ offers a choice between the behaviours of $p$ and
$q$, and $\alpha p$ executes action $\alpha$ to transform into
$p$.  This intuition is captured by the transition rules below.
They give rise to $A_\tau$-labelled transitions between closed
BCCS terms.
\[
  \frac{~}{\alpha x\mv{\alpha}x}
\qquad
  \frac{x\mv{\alpha}x'}{x+y\mv \alpha x'}
\qquad
  \frac{y\mv{\alpha}y'}{x+y\mv \alpha y'}
\]
We assume a countably infinite set $V$ of variables; $w,x,y,z$
denote elements of $V$. Open BCCS terms, denoted by $t,u,v$, may
contain variables from $V$.  A (closed) substitution, typically
denoted by $\sigma$, maps variables in $V$ to (closed) terms. For
open terms $t$ and $u$, and a preorder $\sqsubseteq$ (or
equivalence $\equiv$) on closed terms, we define $t\sqsubseteq u$
(or $t\equiv u$) if $\sigma(t)\sqsubseteq\sigma(u)$ (resp.\
$\sigma(t)\equiv\sigma(u)$) for all closed substitutions $\sigma$.
A preorder $\sqsubseteq$ is called a \emph{precongruence} (for
BCCS) if $p \sqsubseteq q$ and $p' \sqsubseteq q'$ implies that
$p+p' \sqsubseteq q+q'$ and $\alpha p \sqsubseteq \alpha q$ for
$\alpha \in A_\tau$.  The \emph{kernel} of a preorder
$\sqsubseteq$ is $\sqsubseteq \cap \sqsubseteq^{-1}$.

An \emph{axiomatisation} is a collection of equations $t \approx
u$ or of inequations $t \preccurlyeq u$. The (in)equations in an
axiomatisation $E$ are referred to as \emph{axioms}.  If $E$ is an
equational axiomatisation, we write $E\vdash t\approx u$ if the
equation $t\approx u$ is derivable from the axioms in $E$ using
the rules of equational logic (reflexivity, symmetry,
transitivity, substitution, and closure under BCCS contexts). For
the derivation of an inequation $t\preccurlyeq u$ from an
inequational axiomatisation $E$, denoted by $E\vdash t\preccurlyeq
u$, the rule for symmetry is omitted. We will also allow equations
$t\approx u$ in inequational axiomatisations, as an abbreviation
of $t\preccurlyeq u$ and $u\preccurlyeq t$.

An axiomatisation $E$ is \emph{sound} modulo a precongruence
$\sqsubseteq$ (or congruence $\equiv$) if for all terms $t,u$,
from $E\vdash t\preccurlyeq u$ (or $E\vdash t\approx u$) it
follows that $t\sqsubseteq u$ (or $t\equiv u$). $E$ is
\emph{ground-complete} for $\sqsubseteq$ (or $\equiv$) if for all
closed terms $p,q$, $p\sqsubseteq q$ (or $p\equiv q$) implies
$E\vdash p\preccurlyeq q$ (or $E\vdash p\approx q$). And $E$ is
\emph{$\omega$-complete} if for all terms $t,u$ with
$E\vdash\sigma(t)\preccurlyeq\sigma(u)$ (or
$E\vdash\sigma(t)\approx\sigma(u)$) for all closed substitutions
$\sigma$, we have $E\vdash t\preccurlyeq u$ (or $E\vdash t\approx
u$).

Bisimilarity is the largest equivalence relation $\bis$ such that
$p\bis q$ and $p\mv{\alpha}p'$ implies $\exists q':q\mv{\alpha}q'$
and $p'\bis q'$. It is completely axiomatised by the following
axioms:
\[
\begin{array}{c@{\qquad}l}
x+y  \approx  y+x          &({\rm A}1)\\
(x+y)+z  \approx  x+(y+z)  &({\rm A}2)\\
x+x  \approx  x            &({\rm A}3)\\
 x+\nil  \approx  x         & ({\rm A}4)\\
\end{array}
\]
Summation $\sum_{i\in\{1,\ldots,n\}}t_i$ denotes $t_1+\cdots+t_n$,
where summation over the empty set denotes $\nil$. Binary choice
$\_+\_$ and summation bind weaker than $\alpha\_$\,. For each
closed BCCS term $p$ there exists a finite set $\{\alpha_i p_i\mid
i\!\in\! I\}$ of closed terms such that $p\bis \sum_{i\in I}
\alpha_i p_i$ and hence $\mbox{A1--4}\vdash p\approx \sum_{i\in I}
\alpha_i p_i$. The $\alpha_i p_i$ are called the \emph{summands}
of $p$.

We write $p\Rightarrow q$ if there is a (possibly empty) sequence
of $\tau$-transitions $p\mv{\tau}\cdots\mv{\tau}q$; furthermore
$p\mv{\alpha}$ denotes that there is a term $q$ with
$p\mv{\alpha}q$, and likewise $p\Rightarrow\mv{a}$ denotes that
there are a terms $q,r$ with $p\Rightarrow q \mv{\alpha} r$.

\begin{defi}[Initial actions]\label{def-initials}\rm
For any closed term $p$, the set $I(p)$ of \emph{strongly initial
actions} is $I(p)=\{\alpha\!\in\! A_\tau \mid$
\plat{$p\mv{\alpha}\}$}, whereas the set $\mc{I}_\tau(p)$ of
\emph{weakly initial actions} is \plat{$\mc{I}_\tau(p)=\{\alpha\in
A_\tau\mid p\Rightarrow \mv{\alpha}\}$}.

A preorder $\sqsubseteq$ is \emph{(strong) initials preserving} if
$p\sqsubseteq q$ implies $I(p)\subseteq I(q)$ for all $p$ and $q$;
it is \emph{weak initials preserving} if $p\sqsubseteq q$ implies
$\mc{I}_\tau(p)\subseteq \mc{I}_\tau(q)$. With $\mc{I}(p)$ we
denote $\mc{I}_\tau(p) \cap A$, the weakly initial \emph{visible}
actions of $p$.
\end{defi}


\section{The algorithm for producing equational axiomatisations}

In Aceto, Fokkink \& Ing{\'o}lfsd{\'o}ttir \cite{AFI07} an
algorithm is presented which takes as input a sound and
ground-complete inequational axiomatisation $E$ for BCCS modulo a
precongruence in the linear time -- branching time spectrum that
contains the ready simulation preorder, and generates as output an
equational axiomatisation $\mc{A}(E)$ which is sound and
ground-complete for BCCS modulo the corresponding congruence.
Moreover, if the original axiomatisation $E$ is $\omega$-complete,
so is the resulting axiomatisation. The axiomatisation $\mc{A}(E)$
generated by the algorithm from $E$ contains the axioms A1--4 as
well
as the axioms:\\[1em]
(RS$_\equiv$):\hfill $\alpha(\beta x + z) + \alpha (\beta x +
\beta y + z) \approx
 \alpha (\beta x + \beta y + z)$\\[1em] for $\alpha,\beta\in A_\tau$,
that are valid in ready simulation semantics, together with the
following equations, for each inequational axiom $t \preccurlyeq
u$ in $E$:
\begin{enumerate}
\item[(1)] $ t + u \approx u$; and \item[(2)] $\alpha(t + x) +
\alpha(u + x) \approx \alpha(u + x)$ (for each $\alpha\in A_\tau$,
and some variable $x$ that does not occur in $t + u$).
\end{enumerate}
Instead of explicitly adding the axioms RS$_\equiv$ one can
equivalently add the axioms\\[1em](RS):\hfill
$\beta x \preccurlyeq \beta x + \beta y$\hfill
for $\beta\in A_\tau$\\[1em]
to $E$ prior to invoking steps (1) and (2) above. Moreover, as
observed in \cite{FGP08}, the conversion from $E$ to $\mc{A}(E)$
can be factored into two steps:
\begin{itemise}
\item Given an inequational axiomatisation $E$, its
  \emph{BCCS-context closure} $\overline{E}$ is
  $$E \cup \{\alpha(t+x)\preccurlyeq \alpha(u+x) \mid \alpha\in A_\tau
  \wedge t \preccurlyeq u \in E\} \cup \{\mbox{RS}\}$$
  where $x$ is a variable not occurring in $E$.
\item Now $\mc{A}(E) = \{t+u\approx u \mid t \preccurlyeq u \in
\overline
  E\} \cup \mbox{(A1--4)}$.
\end{itemise}
In \cite{AFI07} the correctness of this algorithm was shown for
all precongruences listed in the linear time -- branching time
spectrum of \cite{Gla01} that are included between trace inclusion
and the ready simulation preorder. The proof contained a few
arguments that had to be checked for each of these preorders
separately. Subsequently, in de Frutos Escrig, Gregorio \&
Palomino \cite{FGP08} the following more general result was
obtained:

\begin{theorem}\label{thm-dFGP}
Let $\sqsubseteq$ be an initials preserving precongruence that
contains the ready simulation preorder $\sqsubseteq_{\rm RS}$, and
let $E$ be a sound and ground-complete axiomatisation of
$\sqsubseteq$. Then $\mc{A}(E)$ is a sound and ground-complete
axiomatisation of the kernel of $\sqsubseteq$. Moreover, if $E$ is
$\omega$-complete, then so is $\mc{A}(E)$.
\end{theorem}
As all preorders in the linear time -- branching time spectrum of
\cite{Gla01} between trace inclusion and ready simulation are
initials preserving, the above theorem strengthens the result of
\cite{AFI07}.

\section{Correctness proof of the algorithm}
\label{sec:proof}

Below we recreate the proof of Theorem~\ref{thm-dFGP}.
Lemma~\ref{context closure} and
Proposition~\ref{prop-completeness} constitute the completeness
argument, and are taken directly from \cite{FGP08}.  However, the
proofs below are significantly simpler---in the case of
Lemma~\ref{context closure} employing ideas from the completeness
proof in \cite{AFI07}. The essence of Lemma~\ref{lem-soundness}
and its proof come from \cite{FGP08} as well; this is the
soundness argument. Our rewording of Lemma~\ref{lem-soundness}
allows it to be reused in Sections~\ref{sec:weak} and
~\ref{sec-infinite}.

\begin{lemma}\label{context closure}
Let $E$ be an inequational axiomatisation. Then for any
$t\preccurlyeq u \in E$ and any context $\mc{C}[\cdot]$ we have
$\mc{A}(E)\vdash \mc{C}(t) + \mc{C}(u) \approx \mc{C}(u)$.
\end{lemma}

\begin{proof} By structural induction on the context $\mc{C}[\cdot]$.

In case of the trivial context $\mc{C}[\cdot]= \cdot\,$ we have to
show $\mc{A}(E)\vdash t+u\approx u$, which follows immediately
from step (1) in the construction of $\mc{A}(E)$.

For a context $\alpha (\,\cdot +v)$ we have to show
$\mc{A}(E)\vdash \alpha(t+v) + \alpha(u+v) \approx \alpha(u+v)$,
which follows from step (2) in the construction of $\mc{A}(E)$,
substituting the term $v$ for the variable $x$.

Now let the result be obtained for a context $\mc{D}[\cdot]$ and
let $\mc{C}[\cdot]$ be of the form $\mc{D}[\cdot] + v$, where $v$
is an arbitrary term, possibly $\nil$. We have to show that
$\mc{A}(E)\vdash \mc{D}(t)+v + \mc{D}(u)+v \approx \mc{D}(u)+v$.
This follows immediately from the induction hypothesis.

Finally, let the result be obtained for a context
$\beta\mc{D}[\cdot]$ and let $\mc{C}[\cdot]$ be of the form
$\alpha (\beta \mc{D}[\cdot]+v)$. We have to obtain
$$\mc{A}(E)\vdash \alpha(\beta\mc{D}(t)+v) + \alpha(\beta\mc{D}(u)+v)
 \approx \alpha(\beta\mc{D}(u)+v).$$
By the induction hypothesis we have $\mc{A}(E)\vdash
\beta\mc{D}(t) + \beta\mc{D}(u) \approx
 \beta\mc{D}(u)$, so it suffices to obtain
\[
\begin{array}{ll}
 \mc{A}(E)\vdash & \alpha(\beta\mc{D}(t)+v) +
 \alpha(\beta\mc{D}(t)+\beta\mc{D}(u)+v)\\
 & \approx \alpha(\beta\mc{D}(t)+\beta\mc{D}(u)+v).
 \end{array}\]
This is an instance of the axiom RS$_\equiv$.  \end{proof}

\begin{proposition}\label{prop-completeness}
Let $E$ be an inequational axiomatisation. Then whenever $E\vdash
t \preccurlyeq u$ we also have $\mc{A}(E)\vdash t+u \approx u$.
\end{proposition}

\begin{proof}
If $E\vdash t \preccurlyeq u$ then there is a chain of terms
$t_0,\ldots,t_n$ for $n\geq 0$ with $t_0=t$ and $t_n=u$ such that
for $0\leq i< n$ the inequation $t_i \preccurlyeq t_{i+1}$ is
provable from $E$ by one application of an axiom. We now prove the
claim by induction on $n$. The case $n=0$ is an instance of axiom
A3, and the case $n=1$ is an immediate consequence of
Lemma~\ref{context closure}, by applying substitution.

Now for the general case, let $v$ be $t_i$ for some $0<i<n$. By
induction we have $\mc{A}(E)\vdash t+v \approx v$ and
$\mc{A}(E)\vdash v+u \approx u$. Applying once again A3 this
yields $\mc{A}(E)\vdash t+u \approx t+v+u \approx v+u \approx u$.
 \end{proof}

\begin{lemma}~\label{lem-soundness}
Let $\sqsubseteq$ be a precongruence containing $\sqsubseteq_{\it
RS}$ and $\equiv$ be its kernel. Let $p,q$ be closed terms with $p
\sqsubseteq q$ and $I(p)\subseteq I(q)$. Then $p + q \equiv q$.
\end{lemma}

\begin{proof}
As $p \sqsubseteq q$ and $\sqsubseteq$ is a precongruence for
choice, we have $p+q \sqsubseteq q+q \sqsubseteq q$. To show that
$q\sqsubseteq p+q$, let $p \bis \sum_{i\in I}\alpha_i p_i$ and $q
\bis \sum_{j\in J}\beta_jq_j$. It is well known \cite{Gla01} that
$p\bis q$ implies $I(p)=I(q)$ as well as $p \sqsubseteq_{\it RS}
q$ and hence $p\sqsubseteq q$. Writing $p|_\beta$ for
$\sum_{\alpha_i=\beta}\!\alpha_i p_i$, the collection of
$\beta$-summands of $p$, and likewise
\plat{$q|_\beta=\sum_{\beta_j :=\beta}\!\beta_jq_j$}, we have
\plat{$p \bis \sum_{\beta\in I(p)}p|_\beta$} and \plat{$q \bis
\sum_{\beta\in I(q)}q|_\beta$}. Using that $I(p)\subseteq I(q)$,
and that $\sqsubseteq$ is a precongruence for the choice operator
$+$, it suffices to show that $q|_\beta \sqsubseteq p|_\beta +
q|_\beta$ for all $\beta \in A_\tau$. This is an immediate
consequence of the axiom RS, which is sound for $\sqsubseteq_{\it
RS}$ and hence for $\sqsubseteq$.   \end{proof}

\noindent\textbf{Proof of Theorem~\ref{thm-dFGP}:} As
$\sqsubseteq$ is a precongruence contained in the ready simulation
preorder, all inequations in the BCCS-context closure
$\overline{E}$ of $E$ are sound w.r.t.\ $\sqsubseteq$. Considering
that the soundness of an (in)equation is tantamount to the
soundness of its closed substitution instances, the soundness of
$\mc{A}(E)$ now follows from Lemma~\ref{lem-soundness}.

Ground-completeness and $\omega$-completeness follow directly from
Proposition~\ref{prop-completeness}: If $t \equiv u$, that is $t
\sqsubseteq u$ and $u \sqsubseteq t$, we have $E \vdash t
\preccurlyeq u$ and $E \vdash u \preccurlyeq t$ by the
completeness of $E$.  So Proposition~\ref{prop-completeness}
yields $\mc{A}(E) \vdash t \approx t+u \approx u$.\hfill$\Box$


\section{Applying the algorithm to weak semantics}
\label{sec:weak}

The results of \cite{AFI07,FGP08} were obtained for the language
BCCSP, containing the basic operators of CCS and CSP. This
language is obtained from BCCS as presented above by omitting the
unary operator $\tau$. Naturally, as shown above, these results
generalise smoothly to BCCS by treating $\tau$ just like any
visible action from $A$. Preorders or equivalences that do so are
called \emph{strong}. The main purpose of the present paper is to
apply the same ideas to \emph{weak} preorders: those that in some
way abstract from internal activity, by treating $\tau$
differently from visible actions.

When reading Theorem~\ref{thm-dFGP} in the context of weak process
semantics, it helps to remember that $\sqsubseteq_{\it RS}$ is the
\emph{strong} ready simulation preorder, and ``initials
preserving'' refers to preservation of the \emph{strongly} initial
actions. Theorem~\ref{thm-dFGP} directly applies to the rooted
variants of the $\eta$-simulation surveyed in \cite{Gla93}, for
these preorders are coarser than the strong ready simulation
preorder and strong initials preserving.  However, most weak
semantics are not strong initials preserving (for instance,
typically $\tau x\preccurlyeq x$ is sound), and consequently
Theorem~\ref{thm-dFGP} fails to apply to them.

The precondition of being initials preserving is in fact nowhere
used in the completeness proof in \cite{FGP08}, or its recreation
in Section~\ref{sec:proof}. Hence, this condition applies to the
soundness claim only.  Therefore, in order to apply the algorithm
to weak semantics, all we need is to find another way of
guaranteeing the soundness of the generated axioms.

Given that we deal with preorders containing the ready simulation
preorder, the axiom RS$_\equiv$ will always be sound. Moreover,
the axioms generated by step (2) in the construction of
$\mc{A}(E)$ are guaranteed to be sound by
Lemma~\ref{lem-soundness}, for we have $\alpha(t+x) \sqsubseteq
\alpha(u+x)$ and $I(\alpha(t+x)) = I(\alpha(u+x)) = \{\alpha\}$.
One way to guarantee soundness of the remaining axioms, is to
check this for each of them explicitly:

\begin{theorem}\label{thm-correctness}
Let $\sqsubseteq$ be a precongruence that contains the ready
simulation preorder $\sqsubseteq_{\rm RS}$, and let $E$ be a sound
and ground-complete axiomatisation of $\sqsubseteq$, such that for
each axiom $t \preccurlyeq u$ in $E$ the law $t+u \approx u$ is
sound as well. Then $\mc{A}(E)$ is a sound and ground-complete
axiomatisation of the kernel of $\sqsubseteq$.  Moreover, if $E$
is $\omega$-complete, then so is $\mc{A}(E)$.\hfill$\Box$
\end{theorem}
Note that for the axioms stemming from $t\preccurlyeq u$ with
$I(\sigma(t)) \subseteq I(\sigma(u))$ for any closed substitution
$\sigma$, no check is needed, by Lemma~\ref{lem-soundness}. Next
we present three other conditions that guarantee soundness of
$\mc{A}(E)$.

\begin{theorem}\label{thm-correctness1}
Let $\sqsubseteq$ be a precongruence that contains the strong ready
simulation preorder $\sqsubseteq_{\rm RS}$, such that $p\equiv
\tau p$, with $\equiv$ the kernel of $\sqsubseteq$, for all
processes $p$. Let $E$ be a sound and ground-complete
axiomatisation of $\sqsubseteq$. Then $\mc{A}(E)$ is a sound and
ground-complete axiomatisation of $\equiv$.
Moreover, if $E$ is $\omega$-complete, then so is $\mc{A}(E)$.
\end{theorem}

\begin{proof}
It suffices to show that $p\sqsubseteq q$ implies $p+q \equiv q$.
So assume $p \sqsubseteq q$. Let $p':=\tau p$ and $q':=\tau q$.
By assumption we have $p\equiv p'$ and $q\equiv q'$, and therefore
$p' \sqsubseteq q'$.
As $I(p')=I(q')=\{\tau\}$, Lemma~\ref{lem-soundness} yields
$p'+q'\equiv q'$, which implies $p+q \equiv q$.
\end{proof}

\begin{theorem}\label{thm-correctness2}
Let $\sqsubseteq$ be a precongruence that contains the strong ready
simulation preorder $\sqsubseteq_{\rm RS}$, such that $p \equiv
\tau p$, with $\equiv$ the kernel of $\sqsubseteq$, for all
processes $p$ with $I(p)\neq\emptyset$, and such that $p
\sqsubseteq q$ implies that if $I(p)\neq\emptyset$ then
$I(q)\neq\emptyset$. Let $E$ be a sound and ground-complete
axiomatisation of $\sqsubseteq$.  Then $\mc{A}(E)$ is a sound and
ground-complete axiomatisation of $\equiv$.  Moreover, if $E$ is
$\omega$-complete, then so is $\mc{A}(E)$.
\end{theorem}

\begin{proof}
Again it suffices to show that $p\sqsubseteq q$ implies $p+q
\equiv q$. So assume $p \sqsubseteq q$. If $I(p)=\emptyset$ then
trivially $I(p)\subseteq I(q)$ and the result follows from
Lemma~\ref{lem-soundness}. Otherwise, we have $p\equiv\tau p$ and
$q\equiv\tau q$ and the result follows as in the previous proof.
 \end{proof} Let T2 be the second $\tau$-law of CCS
\cite{Mi89}: \quad $\tau x \approx \tau x + x$.

\begin{theorem}\label{thm-correctness3}
Let $\sqsubseteq$ be a weak initials preserving precongruence that
contains the strong ready simulation preorder $\sqsubseteq_{\rm
RS}$ and satisfies \mbox{\rm T2}, and let $E$ be a sound and
ground-complete axiomatisation of $\sqsubseteq$.  Then $\mc{A}(E)$
is a sound and ground-complete axiomatisation of the kernel of
$\sqsubseteq$. Moreover, if $E$ is $\omega$-complete, then so is
$\mc{A}(E)$.
\end{theorem}

\begin{proof}
A straightforward induction on the length of a path $p \Rightarrow
p'$, using the soundness of T2, yields that if \plat{$p
\Rightarrow p' \mv{\alpha} p''$} then $p \equiv p+\alpha p''$,
where $\equiv$ is the kernel of $\sqsubseteq$. Hence for any
closed term $p$ there is a closed term $p'$ such that $p\equiv p'$
and $\mc{I}_\tau(p)=I(p')$. Using this, the soundness claim
follows from Lemma~\ref{lem-soundness}, reasoning as in the proof
of Theorem~\ref{thm-correctness1}.  \end{proof} Note that
$\mc{I}_\tau(p) = \mc{I}(p) \cup \{\tau \mid p \mv{\tau}\}$ (see
Definition~\ref{def-initials}). Thus, the precondition of
Theorem~\ref{thm-correctness3} is that $p \sqsubseteq q$ implies
that $\mc{I}(p) \subseteq \mc{I}(q)$ and that if $p\mv{\tau}$ then
$q\mv{\tau}$.

So far, Theorem~\ref{thm-correctness} applies to the widest
selection of preorders, but it comes with the need to check the
soundness of some of the generated axioms separately.  We can go
even further in this direction by observing that also the
precondition of containing the ready simulation preorder is not
used anywhere in the completeness proof:

\begin{theorem}\label{thm-completeness}
Let $\sqsubseteq$ be any precongruence, and let $E$ be a
ground-complete axiomatisation of $\sqsubseteq$. Then $\mc{A}(E)$
is a ground-complete axiomatisation of the kernel of
$\sqsubseteq$. Moreover, if $E$ is $\omega$-complete, then so is
$\mc{A}(E)$.\hfill$\Box$
\end{theorem}
Note that this theorem makes no statement on the soundness of
$\mc{A}(E)$. Hence an application of this theorem to achieve a
sound and ground-complete axiomatisation involves checking
the soundness of all axioms generated by both step (1) and step
(2) of the algorithm explicitly, as well as the soundness of the
axioms A1--4 and RS$_\equiv$. As A1--4 and RS$_\equiv$ constitute
a sound and ground-complete axiomatisation of strong ready
simulation equivalence, checking the soundness of these axioms is
naturally done by checking that the kernel of $\sqsubseteq$
contains strong ready simulation equivalence. As we shall
illustrate in the next section, this is a meaningful improvement
over the precondition of Theorem~\ref{thm-correctness} that
$\sqsubseteq$ contains the strong ready simulation preorder. The
price to be paid for this improvement is that also the soundness
of the axioms generated by step (2) of the algorithm has to be
checked separately. This is because the proof of
Lemma~\ref{lem-soundness} uses that $\sqsubseteq$ contains the
strong ready simulation preorder.

In \cite{Gla93} 155 weak preorders are reviewed. Most of them fail
to be congruences for the choice operator of BCCS\@.
Axiomatisations are typically proposed for the \emph{congruence
closures} of these preorders: the coarsest congruence contained in
them. All preorders $\sqsubseteq$ in \cite{Gla93} and their
congruence closures satisfy the property that if $p \sqsubseteq q$
then $\mc{I}(p) \subseteq \mc{I}(q)$. \footnote{In fact, most
  preorders in \cite{Gla93} are actually pairs of
  preorders, as for every semantics a \emph{may} and a \emph{must}
  preorder are proposed. Inspired by \cite{DH84}, there are two
  differences between the may and the must preorders.  One is a
  different treatment of \emph{divergence}---this has no effect when
  restricting attention to BCCS processes. The other is that the
  preorders are oriented in opposite directions. This entire paper, as
  well as \cite{AFI07,FGP08}, has been written from the perspective of
  the may preorders. When dealing with must preorders $\sqsubseteq$ we
  have that if $p \sqsubseteq q$ then $\mc{I}(p) \supseteq \mc{I}(q)$.
  Moreover, none of these preorders contains $\sqsubseteq_{\it RS}$---at
  best their inverses have this property. Consequently, for preorders
  oriented in the must direction, the algorithm is to be applied in
  the reverse direction, where an inequational axiom $t \preccurlyeq
  u$ gives rise to equational axioms like $t \approx t+u$.}

Of the 155 preorders surveyed in \cite{Gla93}, 87 contain the
strong ready simulation preorder. We can partition this collection
into four classes.

6 preorders are variants of trace inclusion and the simulation
preorder. They are precongruences for BCCS and satisfy the axiom
$x \approx \tau x$. Consequently, they fall in the scope of
Theorem~\ref{thm-correctness1}.

16 preorders are variants of completed trace inclusion or the
completed simulation preorder. Each of their congruence closures
$\sqsubseteq$ has the property that $p \sqsubseteq q$ implies that
if $I(p)\neq\emptyset$ then $I(q)\neq\emptyset$. Moreover, the
kernels $\equiv$ of $\sqsubseteq$ have the property that $p \equiv
\tau p$ for all processes $p$ with $I(p)\neq\emptyset$.
Consequently, these congruence closures fall in the scope of
Theorem~\ref{thm-correctness2}.

22 are variants of the $\eta$-simulation or the $\eta$-ready
simulation.  Their congruence closures are strong initials
preserving, and hence fall under the scope of
Theorem~\ref{thm-dFGP}.

The congruence closures $\sqsubseteq$ of the remaining 43
preorders satisfy the property that $p \sqsubseteq q$ implies that
if $p \mv{\tau}$ then $q\mv{\tau}$, and hence $\mc{I}_\tau(p)
\subseteq \mc{I}_\tau(q)$. These precongruences therefore fall in
the scope of Theorem~\ref{thm-correctness3}.

Thus, the algorithm of \cite{AFI07} applies to all congruence
closures of preorders in \cite{Gla93} coarser than the ready
simulation preorder.

\section{Applications}\label{sec-applications}  \label{sec6}

In De Nicola \& Hennessy \cite{DH84} three testing preorders are
defined, and for each of them a sound and ground-complete
axiomatisation over BCCS is provided. In fact the axiomatisations
apply to all of CCS, enriched with a special constant $\Omega$,
and the semantics of processes involves, besides $A_\tau$-labelled
transitions, a \emph{convergence} predicate. However, the
completeness proofs remain valid when restricting attention to the
sublanguage BCCS, and there the convergence predicate plays no
r\^ole (for all processes are convergent). The \emph{combined may-
and must-testing
  preorder} is axiomatised by the laws A1--4 together with the axioms
$$\begin{array}{c@{\qquad}l}
\alpha x + \alpha y \approx \alpha (\tau x + \tau y) & \mbox{(N1)}\\
x + \tau y \preccurlyeq \tau(x+y)                    & \mbox{(N2)}\\
\alpha x + \tau(\alpha y + z) \approx \tau(\alpha x + \alpha y + z) & \mbox{(N3)}\\
\tau x \preccurlyeq x                                & \mbox{(N4)}\\
\end{array}$$
where $\alpha$ ranges over $A_\tau$. The \emph{must preorder} has
the additional axiom $$\tau x + \tau y \preccurlyeq x \qquad
\mbox{(E1)}$$ and the \emph{may preorder} has the additional axiom
$$\mbox{}\;\, x \preccurlyeq \tau x  + \tau y \qquad
\mbox{(F1)}.$$ Note that T2 follows from N2 and N4. We will now
apply the algorithm to obtain sound and ground-complete
axiomatisations of the three associated testing equivalences.

Beforehand, we mention a trivial simplification in applying the
algorithm: if the inequational axiomatisation features an equation
$t\approx u$, formally speaking this is an abbreviation for the
two axioms $t \preccurlyeq u$ and $u \preccurlyeq t$. Thus, step
(1) of the algorithm generates the equations $t+u \approx u$ and
$u+t \approx t$. Together, these are equivalent to the original
equation $t \approx u$. Moreover, in the presence of $t \approx u$
the two axioms generated by step (2) of the algorithm are
redundant. Thus, we can simplify the algorithm by leaving
equations untouched.

\paragraph{The may preorder.}
The may preorder of \cite{DH84} coincides with weak trace
inclusion, which is coarser than the ready simulation preorder. As
remarked in \cite{DH84}, it is not hard to see that the
axiomatisation above can be simplified to A1--4 together with
$$\begin{array}{c}
\tau x \approx x                               \\
\alpha x + \alpha y \approx \alpha (x+y)       \\
x \preccurlyeq x+y
\end{array}$$
Applying Theorem~\ref{thm-correctness1} yields a sound and
ground-complete axiomatisation of
may\hspace{-.7pt}-\hspace{-.7pt}testing equivalence,
which coincides with weak trace equivalence. It consists of A1--4,
RS$_\equiv$ and
$$\begin{array}{c}
\tau x \approx x                               \\
\alpha x + \alpha y \approx \alpha (x+y)       \\
x + x + y \approx x + y                        \\
\alpha(x+z) + \alpha(x+y+z) \approx \alpha(x+y+z)
\end{array}$$
As RS$_\equiv$ is an instance of the last axiom above, that last
axioms follows from the second, and the third from A3, this
axiomatisation can be simplified to A1--4 together with
$$\begin{array}{c}
\tau x \approx x                               \\
\alpha x + \alpha y \approx \alpha (x+y)       \\
\end{array}$$

\paragraph{The must preorder.}
On BCCS, the must preorder of \cite{DH84} coincides with the
failures preorder of CSP \cite{BHR84}. Its inverse contains the
ready simulation preorder and is weak initials preserving. Hence
we can apply Theorem~\ref{thm-correctness3} to obtain a sound and
ground-complete axiomatisation of must-testing equivalence. First
we note that N4 is a simple consequence of E1 and thus can be
omitted. Now Theorem~\ref{thm-correctness3} yields the axioms
A1--4, RS$_\equiv$ and
$$\begin{array}{@{}c@{~~\quad}l@{}}
\alpha x + \alpha y \approx \alpha (\tau x + \tau y) & \mbox{(N1)}\\
x + \tau y \approx x + \tau y + \tau(x+y)            & \mbox{(N2$_1$)}\\
\alpha(x \!+\! \tau y \!+\! z) \approx \alpha(x \!+\! \tau y \!+\!z) +
\alpha(\tau(x\!+\!y)\!+\!z)
                                                     & \mbox{(N2$_2$)}\\
\alpha x + \tau(\alpha y + z) \approx \tau(\alpha x + \alpha y +
z)
                                                     & \mbox{(N3)}\\
\tau x + \tau y \approx \tau x + \tau y + x          & \mbox{(E1$_1$)}\\
\alpha(\tau x + \tau y +z) \approx \alpha(\tau x + \tau y + z) +
\alpha(x+z)
                                                     & \mbox{(E1$_2$)}\\
\end{array}$$
This axiomatisation can be simplified to A1--4 together with
$$\begin{array}{c@{\qquad}l}
\alpha x + \alpha y \approx \alpha (\tau x + \tau y) & \mbox{(N1)}\\
x + \tau y \approx \tau y + \tau(x+y)                & \mbox{(N2$^*$)}\\
\alpha x + \tau(\alpha y+z) \approx \tau(\alpha x +\alpha y +z) &
\mbox{(N3)}
\end{array}$$
Namely, E1$_1$ implies T2 which allows us to reformulate N2$_1$ as
N2$^*$. The latter axiom implies T2 (by taking $y=x$) and hence
also N2$_1$ and E1$_1$.  It remains to derive N2$_2$, E2$_2$ and
RS$_\equiv$.  In all three cases, by N1 it suffices to derive the
instance where $\alpha=\tau$.  Substituting $\tau y$ for $y$ in
N2$^*$ and applying $\tau \tau y \approx \tau y$ (which follows
from N1) and T2 gives $\tau(x+\tau y) \approx x+\tau y$. Now it is
straightforward to derive N2$_2^\tau$, E2$_2^\tau$ and
RS$_\equiv^\tau$.

This axiomatisation has been mentioned in \cite{Gla86}, just like
the axiomatisation of weak trace equivalence mentioned above.
However, we have not found an actual proof of its
ground-completeness (or the ground-completeness of any other
axiomatisation of must-testing equivalence over BCCS) in the
literature.

\paragraph{The combined may and must preorder.}
The combined may- and must-testing preorder is the intersection of the
may- and the must-testing preorders.  It is known that on BCCS the
combined preorder has the same kernel as the must preorder, so that we
can reuse the axiomatisation above.  Nevertheless, obtaining a sound
and complete axiomatisation of this kernel by means of the algorithm
provides a useful illustration of some of the issues that play a
r\^ole in this process. On BCCS, the combined preorder is contained
in weak trace equivalence, and hence contains neither the strong
ready simulation preorder, nor its inverse. Therefore,
Theorems~\ref{thm-correctness}--\ref{thm-correctness3} are not
applicable to it. However, its kernel does contain strong ready
simulation equivalence, and with help of
Theorem~\ref{thm-completeness} we can obtain a sound and
ground-complete axiomatisation of it. The algorithm yields the
axioms A1--4, RS$_\equiv$ and
$$\begin{array}{@{}c@{~~\quad}l@{}}
\alpha x + \alpha y \approx \alpha (\tau x + \tau y) & \mbox{(N1)}\\
x + \tau y \approx x + \tau y + \tau(x+y)            & \mbox{(N2$_1$)}\\
\alpha(x \!+\! \tau y \!+\! z) \approx \alpha(x \!+\! \tau y \!+\!z) +
\alpha(\tau(x\!+\!y)\!+\!z)
                                                     & \mbox{(N2$_2$)}\\
\alpha x + \tau(\alpha y + z) \approx \tau(\alpha x + \alpha y +
z)
                                                     & \mbox{(N3)}\\
\tau x \approx \tau x + x                            & \mbox{(N4$_1$)}\\
\alpha(\tau x +z) \approx \alpha(\tau x + z) + \alpha(x+z)
                                                     & \mbox{(N4$_2$)}\\
\end{array}$$
The soundness of these axioms follows from the fact that they are
derivable both from the axioms for the may preorder and from the
axioms for the must preorder.

As expected, the axiomatisation above is easily seen to be equivalent
to the axiomatisation of must-testing equivalence.

\section{A generalisation to infinite processes}
\label{sec-infinite}

The results in \cite{AFI07,FGP08} were obtained for finite
processes only: processes that can be expressed in BCCSP\@.
Hereby we extend these results to infinite processes that can be
expressed by adding constants to BCCS\@. This is an easy way of
dealing with recursion---an alternative to introducing recursion
as a syntactic construct and requiring congruence properties for
it. An infinite process can be defined by introducing one or more
constants $C$ together with axioms like $C\approx abC$; in this
example, $C$ represents a process that performs an infinite
alternating sequence of $a$ and $b$ actions.

In order to obtain completeness of the axiomatisations
$\mc{A}(E)$, any extension of BCCS with constants will do.
Lemma~\ref{context closure}, Proposition~\ref{prop-completeness}
and Theorem~\ref{thm-completeness} remain valid in this setting.
The only place where structural induction is used is in the proof
of Lemma~\ref{context closure}, and there constants do not bother
us, as they cannot occur on a path from the root of a context,
seen as a parse tree, to the hole.

In order to obtain soundness, we furthermore assume that for any
constant $C$ in the language there is a closed term $\sum_{i\in
I}\alpha_i p_i$ in our extension of BCCS with constants---so $I$
is finite---such that $C \bis \sum_{i\in I}\alpha_i p_i$.  It then
follows that any closed term is bisimulation equivalent to a
closed term of the form $\sum_{i\in I} \alpha_ip_i$.  With this
assumption, all our results generalise to BCCS augmented with
constants.

The proof of Lemma~\ref{lem-soundness} goes through unaltered. The
only proof that needs to be adapted is the one of
Theorem~\ref{thm-correctness3}.

\begin{lemma}\label{weak initials}
Let $\equiv$ be a congruence containing $\bis$ that satisfies
\mbox{\rm T2}. If \plat{$p \Rightarrow p'\mv{\alpha} p''$} then $p
\equiv p+\alpha p''$.
\end{lemma}
\begin{proof}
By induction on the length of the path $p \Rightarrow p'$.
\\
In the base case $p = p' \bis \sum_{i\in I}\alpha_i p_i$, and by
definition of $\bis$ there must be an $i\in I$ with $\alpha_i
=\alpha$ and $p_i\bis{p''}$. It follows that $p \bis p+\alpha p''$
and hence $p \equiv p+\alpha p''$.
\\
Now assume $p \mv{\tau} p' \Rightarrow\mv{\alpha} p''$.  By
induction, $p'\equiv p'+\alpha p''$. T2 yields $p \equiv p+\alpha
p''$.  \end{proof}

\noindent \textbf{Proof of Theorem~\ref{thm-correctness3}:}
Suppose $p\sqsubseteq q$. We have to show that $p+q \equiv q$,
where $\equiv$ is the kernel of $\sqsubseteq$. By the assumption
above, $p \bis \sum_{i\in I}\alpha_i p_i$ for a finite index set
$I$ and closed terms $\alpha_i p_i$ in our extension of BCCS with
constants.  We have $\{\alpha_i \mid i\!\in\! I\} = I(p) \subseteq
\mc{I}_\tau(p) \subseteq \mc{I}_\tau(q)$, so for every $i\in I$
there is a term $q_i$ such that \plat{$q\Rightarrow\mv{\alpha_i}q_i$}.
Let\linebreak $q' := q +\sum_{i\in I} \alpha_i q_i$.  Applying
Lemma~\ref{weak initials} once for every $i\in I$ we obtain $q\equiv
q'$. Now $I(p)\subseteq I(q)$, so Lemma~\ref{lem-soundness} yields
$p+q'\equiv q'$, which implies $p+q \equiv q$.\hfill$\Box$

\section{Applications (continued)}

\paragraph{Adding divergence.}
In \cite{DH84} a special constant $\Omega$ denoting
\emph{divergence} is considered, and the three ground-complete
axiomatisations of the preorders mentioned in
Section~\ref{sec-applications} extend to the presence of
divergence by means of the extra axiom
$$\Omega \preccurlyeq x.\qquad\qquad(\rm \Omega)$$
Although $\Omega$ is defined in terms of a convergence predicate,
in all three testing preorders it is equivalent to a process
engaging in an infinite $\tau$-loop only. We could therefore
equivalently think of $\Omega$ as the process generated by adding
the transition rule $\Omega \mv{\tau} \Omega$ to BCCS. This way we
obtain $\Omega \bis \tau \Omega$, thereby fulfilling the soundness
requirement of Section~\ref{sec-infinite}.
Note that $I_\tau(\Omega) = \mc{I}_\tau(\Omega) = \{\tau\}$.

Invoking Theorem~\ref{thm-correctness1} we obtain a
ground-complete axiomatisation for may-testing equivalence by
adding the extra axioms
\vspace{-1ex}
$$\begin{array}{c@{\qquad}l}
\Omega + x \approx x \\
\alpha(\Omega+z) + \alpha(x+z) \approx \alpha(x+z)\\
\end{array}$$
to the ones mentioned in Section~\ref{sec-applications}. The
second one is derivable from the first and $\alpha x + \alpha y
\approx \alpha (x+y)$. Using A4, the first one is equivalent to
$\Omega\approx \nil$.

As the must preorder $\sqsubseteq$ satisfies $\Omega \sqsubseteq
a0$ for some $a\neq\tau$, it is not weak initials preserving (in
either direction) and we may not apply
Theorem~\ref{thm-correctness3}, as we did in Section~\ref{sec6}.
In order to obtain a sound and ground-complete axiomatisation of
must-testing equivalence, we therefore resort to
Theorem~\ref{thm-correctness}. Applying the algorithm to the
ground-complete axiomatisation of the must preorder yields the
extra axioms
$$\begin{array}{c@{\qquad}l}
\Omega \approx \Omega +x  & \mbox{($\rm \Omega_1$)}\\
\alpha(\Omega+z) \approx \alpha(\Omega+z) + \alpha(x+z)
&\mbox{($\rm\Omega_2$)}
\end{array}$$
Theorem~\ref{thm-correctness} requires us to explicitly check the
soundness of N2$_1$, E1$_1$ and $\rm\Omega_1$. We may not use the
soundness of N2$_1$ and E1$_1$ obtained in
Section~\ref{sec-applications}, as it could have been invalidated
by the addition of $\Omega$ to the language. The soundness of
N2$_1$ follows from Lemma~\ref{lem-soundness}, applying the remark
right after Theorem~\ref{thm-correctness}. The soundness of E1$_1$
follows because it is derivable from T2, which is derivable from
N2 and N4. The soundness of $\rm\Omega_1$ follows because it is
derivable from $\rm\Omega$, T2 and E1, as shown in \cite{DH84}.

E2 and T2 yield $\Omega \approx \Omega + \tau \Omega \approx \tau
\Omega$. With N1 the axiom $\rm\Omega_2$ follows from its instance
where $\alpha=\tau$, which follows from E2 and
$\tau\Omega=\Omega$. Hence a sound and ground-complete
axiomatisation of must-testing equivalence, also known as the
failures equivalence of CSP, consists of (N1), (N2$^*$), (N3) and
$\rm\Omega_1$.

Applying the algorithm to the combined may and must preorder again
yields the extra axioms $\rm\Omega_1$ and $\rm\Omega_2$, and using
Theorem~\ref{thm-completeness} we cannot assume soundness without
establishing this separately. In the presence of $\Omega$ the
kernels of the must preorder and the combined preorder do not
coincide, and this time $\rm\Omega_1$ turns out not to be sound.
This is an example where we cannot apply the algorithm to obtain a
sound and ground-compete axiomatisation. We conjecture that such an
axiomatisation exists nonetheless, namely consisting of
N1, N2$^*$, N3 and
$$\begin{array}{c@{\qquad}l}
\Omega + \tau x \approx \Omega + x & \mbox{(D1)}\\
\Omega + \alpha x \approx \Omega + \alpha(\Omega+x) & \mbox{(D3)}\\
\end{array}$$
In \cite{DH84} the axioms D1 and D3 have been derived from \mbox{N1--4},
thereby establishing their soundness.

\section{Concluding remark}

In \cite{FGP08}, de Frutos Escrig, Gregorio Rodr\'{\i}guez \&
Palomino also present a simplification of the algorithm of
\cite{AFI07} for a large class of applications. The simplification
consists in skipping
step (2) in favour of a \emph{constrained similarity axiom}\\[1em]
(NS$_\equiv$):\hfill $N(x,y) \Rightarrow \alpha x + \alpha(x+y)
\approx \alpha(x+y)$ \hfill for $\alpha\!\in\! A_\tau$\\[1em] Here
$N(x,y)$ is a congruence relation on processes such that $N(p,q)$
is implied by $I(p)=I(q)$. The constrained similarity axiom is a
conditional equation, but it can in several cases be recast in
equational terms. In the special case where $N(p,q)$ holds iff
$I(p)=I(q)$, NS$_\equiv$ is equivalent to RS$_\equiv$. They show
that the simplified algorithm applies to preorders $\sqsubseteq$
satisfying\\[1em](NS):\hfill
$N(x,y) \Rightarrow x \preceq x+y$\hfill\mbox{}\\[1em]
and such that $p\sqsubseteq q$ implies $N(p,q)$. In case $N(p,q)
\Leftrightarrow I(p)=I(q)$ we have that NS is equivalent to RS.

In applying this algorithm to $\tau$-free preorders in the linear
time -- branching time spectrum, they use three different
constraints $N$, whose ranges of application match those of our
Theorems~\ref{thm-correctness1},~\ref{thm-correctness2}
and~\ref{thm-correctness3}. Yet, we have not been able to apply
the simplified algorithm to weak preorders, due to the fact that
we would need an asymmetric precongruence $N$, whereas symmetry is
used crucially in the proofs in \cite{FGP08}. The same applies to
the generalisations of the constrained similarity approach
investigated in \cite{FGP08b}.

\begin{thebibliography}{11}

\bibitem{AFI07}
{ L.~Aceto, W.~Fokkink \& A.~Ing{\'o}lfsd{\'o}ttir} (2007):
\newblock {\em Ready to preorder: Get your {BCCSP} axiomatization for free!}
\newblock In {\sl Proc. CALCO'07}, LNCS 4624, Springer, pp.\ 65--79.

\bibitem{AFI07b} L. Aceto, W. Fokkink \& A.~Ing{\'o}lfsd{\'o}ttir (2007):
\newblock {\em A cancellation theorem for BCCSP}. Submitted. Available at
\url{http://www.ru.is/faculty/luca/reports.html}.

\bibitem{AFIL05} L. Aceto, W. Fokkink, A.~Ing{\'o}lfsd{\'o}ttir \& B. Luttik (2005): {\em Finite
equational bases in process algebra: Results and open questions.}
In {\sl Processes, Terms and Cycles}, LNCS 3838, Springer, pp.\ 338--367.

\bibitem{BHR84}
{ S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {\sl Journal of the ACM} 31(3), pp.\ 560--599.

\bibitem{CF07} T. Chen \& W. Fokkink (2008):
\newblock {\em On the axiomatizability of impossible futures: preorder versus equivalence.}
\newblock In {\sl Proc. LICS'08}, IEEE Press, pp.\ 156--165.

\bibitem{CFLN07}
T. Chen, W. Fokkink, B. Luttik \& S. Nain (2008):
\newblock {\em On finite alphabets and infinite bases.}
\newblock {\sl Information and Computation} 206(5), pp.\ 492--519.

\bibitem{FG08}
{ D.~de~Frutos Escrig \& C.~Gregorio Rodr\'{\i}guez} (2008):
\newblock {\em (Bi)simulations up-to characterise process semantics.}
\newblock To appear in {\sl Information and Computation}.

\bibitem{FGP08}
{ D.~de~Frutos Escrig, C.~Gregorio Rodr\'{\i}guez \& M.~Palomino}
(2008):
\newblock {\em Ready to preorder: an algebraic and general proof.}
\newblock Submitted. Available at \url{http://maude.sip.ucm.es/~miguelpt/}.
\\
An abstract appeared in {\sl Proc. NWPT'07}.

\bibitem{FGP08b}
{ D.~de~Frutos Escrig, C.~Gregorio Rodr\'{\i}guez \& M.~Palomino}
(2008):
\newblock {\em Coinductive characterisations reveal nice relations between preorders and equivalences.}
\newblock In {\sl Proc. FICS'08}, {\sl ENTCS} 212, pp.\ 149--162.

\bibitem{DH84}
{ R.~De~Nicola \& M.~Hennessy} (1984):
\newblock {\em Testing equivalences for processes.}
\newblock {\sl Theoretical Computer Science} 34, pp.\ 83--133.

\bibitem{Gla93}
{ R.J.~van Glabbeek} (1993):
\newblock {\em The linear time -- branching time spectrum {II}; the semantics of sequential systems with silent moves.}
\newblock In {\sl {\rm Proc.} CONCUR'93}, {\sl \rm LNCS} 715, Springer, pp.\ 66--81.

\bibitem{Gla86}
{ R.J.~van Glabbeek} (1997):
\newblock {\em Notes on the methodology of {CCS} and {CSP}.}
\newblock {\sl Theoretical Computer Science} 177(2), pp.\ 329--349.

\bibitem{Gla01}
{ R.J.~van Glabbeek} (2001):
\newblock {\em The linear time -- branching time spectrum {I}; the semantics of concrete, sequential processes.}
\newblock In J.A. Bergstra, A.~Ponse \& S.A. Smolka, editors: {\sl Handbook of Process Algebra}, chapter~1, Elsevier, pp.\ 3--99.

\bibitem{Gro90}
J.F. Groote (1990):
\newblock {\em A new strategy for proving $\omega$-completeness with
  applications in process algebra.}
\newblock In {\sl Proc. CONCUR'90}, LNCS 458, Springer, pp.\ 314--331.

\bibitem{Mi89}
{ R.~Milner} (1989):
\newblock {\em Communication and Concurrency}.
\newblock Prentice Hall, Englewood Cliffs.

\end{thebibliography}

\end{document}
