\documentclass[runningheads]{llncs}
\bibliographystyle{plain}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% References %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Prop.~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Cor.~\ref{cor-#1}}
\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
\newcommand{\sect}[1]{Sect.~\ref{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}
\newenvironment{itemise2}{\begin{list}{{\bf --}}{\leftmargin 15pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 2pt \itemsep 1pt \parsep 1pt}}{\end{list}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}} % disjoint union
\newcommand{\IT}{\mbox{\sf T\hspace{-5.5pt}T}} % openface T (terms)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}} % no vertical space
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}} % transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt} % no transition
\stackrel{#1\ }{\longrightarrow}}
\newcommand{\dto}{\Longrightarrow} % silent transitions
\newcommand{\bis}[1]{\;\raisebox{.3ex}{$\underline % bisimulation
{\makebox[.7em]{$\leftrightarrow$}}$}\,_{#1}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt} % no bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}\,$}}
\newcommand{\var}{{\it var}} % variables in a term
\newcommand{\opt}[1]{\mbox{\tiny(}#1\mbox{\tiny)}} % optional action
\newcommand{\leftmerge}{\|\hspace{-1.06ex}\raisebox{-1.17ex}{$-$}}% left merge
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Abbreviations %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\bbbn} % natural numbers
\newcommand{\GL}{\mathcal{L}} % a GSOS language
\newcommand{\rel}{\mathcal{R}} % a bisimulation
\newcommand{\names}{\mathcal{N}} % action names in CCS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{On Cool Congruence Formats\\ for Weak Bisimulations\\
\normalsize (extended abstract)}
\titlerunning{On Cool Congruence Formats for Weak Bisimulations}
\author{Rob van Glabbeek}
\institute{National ICT Australia\\
and School of Computer Science and Engineering\\
The University of New South Wales\\
\email{rvg@cs.stanford.edu}}
\begin{document}
\maketitle
\begin{abstract}
In TCS 146, Bard Bloom presented rule formats for four main notions of
bisimulation with silent moves. He proved that weak bisimulation
equivalence is a congruence for any process algebra defined by
\emph{WB cool rules}, and established similar results for rooted weak
bisimulation (Milner's ``observational congruence''), branching
bisimulation and rooted branching bisimulation. This study
reformulates Bloom's results in a more accessible form and contributes
analogues for (rooted) $\eta$-bisimulation and (rooted) delay
bisimulation. Moreover, finite equational axiomatisations of rooted
weak bisimulation equivalence are provided that are sound and complete
for finite processes in any RWB cool process algebra. These require
the introduction of auxiliary operators with lookahead. Finally, a
challenge is presented for which Bloom's formats fall short and
further improvement is called for.
\end{abstract}
\section*{Introduction}
\emph{Structural Operational Semantics} \cite{Mi90ccs,Pl04} is one of
the main methods for defining the meaning of operators in system
description languages like CCS \cite{Mi90ccs}. A system behaviour, or
\emph{process}, is represented by a closed term built from a
collection of operators, and the behaviour of a process is given by
its collection of (outgoing) transitions, each specifying the action
the process performs by taking this transition, and the process that
results after doing so. For each $n$-ary operator $f$ in the language,
a number of \emph{transition rules} are specified that generate the
transitions of a term $f(p_1,\ldots,p_n)$ from the transitions (or the
absence thereof) of its arguments $p_1,\ldots,p_n$.
For purposes of representation and verification, several behavioural
equivalence relations have been defined on processes, of which the
most well-known is \emph{strong bisimulation equivalence}
\cite{Mi90ccs}, and its variants \emph{weak} and \emph{branching}
bisimulation equivalence \cite{Mi90ccs,GW96}, that feature abstraction
from internal actions. In order to allow compositional system
verification, such equivalence relations need to be \emph{congruences}
for the operators under consideration, meaning that the equivalence
class of an $n$-ary operator $f$ applied to arguments $p_1,\ldots,p_n$
is completely determined by the equivalence classes of these
arguments. Although strong bisimulation equivalence is a congruence
for the operators of CCS and many other languages found in the
literature, weak bisimulation equivalence fails to be a congruence for
the \emph{choice} or \emph{alternative composition} operator $+$ of
CCS\@. To bypass this problem one uses the coarsest congruence
relation for $+$ that is finer than weak bisimulation equivalence,
characterised as \emph{rooted weak bisimulation equivalence}
\cite{Mi90ccs,BK85}, which turns out to be a minor variation of weak
bisimulation equivalence, and a congruence for all of CCS and many
other languages. Analogously, \emph{rooted branching bisimulation} is
the coarsest congruence for CCS and many other languages that is finer
than branching bisimulation equivalence \cite{GW96}.
\advance\textheight 1pt
\advance\textheight -1pt
In order to streamline the process of proving that a certain
equivalence is a congruence for certain operators, and to guide
sensible language definitions, syntactic criteria (\emph{rule
formats}) for the transition rules in structural operational semantics
have been developed, ensuring that the equivalence is a congruence for
any operator specified by rules that meet these criteria. One of
these is the \emph{GSOS format} of {\sc Bloom, Istrail \& Meyer}
\cite{BIM95}, generalising an earlier format by {\sc De Simone}
\cite{dS85}. When adhering to this format, all processes are
computably finitely branching, and strong bisimulation equivalence is
a congruence \cite{BIM95}. {\sc Bloom} \cite{Bl95} defines congruence
formats for (rooted) weak and branching bisimulation equivalence by
imposing additional restrictions on the GSOS format. As is customary
in this field, finer equivalences have wider formats, so Bloom's
\emph{BB cool} GSOS format, which guarantees that branching
bisimulation equivalence is a congruence, is more general than his
\emph{WB cool} GSOS format, which suits weak bisimulation equivalence;
also his \emph{RWB cool} GSOS format, suiting rooted weak
bisimulation, is more general than the WB cool GSOS format, and his
\emph{RBB cool} GSOS format, guaranteeing that rooted branching
bisimulation equivalence is a congruence, is the finest of all. The
prime motivating example for these formats is the structural
operational semantics of CCS \cite{Mi90ccs}. All CCS operators are
RWB cool, and the CCS operators other than the + are even WB cool.
Bloom's formats involve a fast bookkeeping effort of names of
variables, used to precisely formulate the \emph{bifurcation rules}
that his formats require. To make his work more accessible, Bloom also
presents simpler but less general versions of his formats, obtained by
imposing an additional syntactic restriction. This restriction makes
it possible to simplify the bifurcation rules to \mbox{\emph{patience
rules}}, which do not require such an extensive bookkeeping. {\sc
Fokkink} \cite{Fok00b} generalises Bloom's \mbox{\emph{simply RBB cool}}
format to a format he calls \emph{RBB safe}, and writes ``The
definition of bifurcation rules is deplorably complicated, and we do
not know of any examples from the literature that are RBB cool but not
simply RBB cool. Therefore, we refrain from this generalisation
here.'' {\sc Ulidowski} \cite{Ul92,UP02,UY00} studies congruence
formats for variations of the semantic equivalences mentioned above
with a different treatment of divergence. Ulidowski's formats form
the counterparts of Bloom's simply cool formats only.
The main aim of the present study is to simplify and further clarify
Bloom's work, so as to make it more accessible for the development of
applications, variations and extensions. In passing, analogous
results are obtained for two equivalences, and their rooted variants,
that bridge the gap between weak and branching bisimulation.
Moreover, the method of {\sc Aceto, Bloom \& Vaandrager} \cite{ABV94}\linebreak
to extract from any GSOS language a finite equational axiomatisation
that is sound and complete for strong bisimulation equivalence on
finite processes, is adapted to rooted weak bisimulation equivalence.
In the construction fresh function symbols may need be added whose
transition rules have \emph{lookahead} and thereby fall outside the
GSOS format.
One of the simplifications of Bloom's formats presented here stems
from the observation that the operators in any of the cool formats can
be partitioned in \emph{principal operators} and \emph{abbreviations},
such that the abbreviations can be regarded as syntactic sugar, adding
nothing that could not be expressed with principal operators. For any
abbreviation $f$ there exists a principal operator $f^\star$ that
typically takes more arguments. For instance, $f(x_1,x_2)$ could be an
abbreviation of $f^\star(x_1,x_1,x_2)$. The rules for the
abbreviations are completely determined by the rules for the principal
operators, and for principal operators patience rules suffice, i.e.\
one does not need the full generality of bifurcation rules. Moreover,
the simply cool formats can be characterised by the requirement that
all operators are principal. These observations make it possible to
define the cool formats of Bloom without mentioning bifurcation rules
altogether. It also enables a drastic simplification of the congruence
proofs, namely by establishing the congruence results for the simply
cool formats first, and reducing the general case to the simple case
by means of some general insights in abbreviation expansion.
Even though any operation that fits the cool formats can also be
defined using merely the simply cool formats, in practice it may be
handy to work with the full generality of the cool formats. The unary
copying operator $\sf cp$ of \cite{BIM95} (page 257) for instance does
not fit the cool formats directly, but can be made to fit by adding an
auxiliary binary copying operator to the language, of which the unary
one is an abbreviation. Dumping the abbreviation from the language
would appear unnatural here, as the unary operator motivates the rules
for both itself and its binary expansion, the latter being needed
merely to make it work.
Another simplification contributed here is in the description of the
RWB cool format. Bloom requires for every operational rule with
target $t$ the existence of two terms $t_1$ and $t_2$, and seven types
of derived operational rules. I show that without limitation of
generality it is always possible to choose $t_2=t$, thereby making
four of those seven types of rules redundant. Thus, the same format is
obtained by requiring only $t_1$ and two types of derived rules (the
third being a patience rule, that was already required for its own sake).
After defining the basic concepts in Section 1, I present the simply
cool congruence formats in Section~\ref{simply cool}.
Section~\ref{cool} presents the theory of abbreviations that lifts the
results from the simple to the general formats, and \sect{rooted}
deals with the rooted congruence formats. Section~\ref{Bloom} compares
my definitions of the cool formats with the ones of Bloom.
Section~\ref{sec-equations} recapitulates the method of \cite{ABV94}
to provide finite equational axiomatisations of strong bisimulation
equivalence that are sound and complete for finite processes on an
augmentation of any given GSOS language, and
Sect.~\ref{sec-cool-equations} extends this work to the rooted weak
equivalences. Finally, \sect{challenge} presents a fairly intuitive
GSOS language for which the existing congruence formats fall short and
further improvement is called for.
\paragraph{Acknowledgement.} My thanks to Simone Tini for inspiration.
\section{Preliminaries}
In this paper $V=\{x_1, x_2, \dots \}$ and $Act$ are two sets of {\em
variables} and {\em actions}.
\begin{definition}\rm\label{df-signature}
A {\em signature} is a collection $\Sigma$ of {\em function symbols}
$f \not\in V$ equipped with a function $ar: \Sigma \rightarrow \IN$.
The set $\IT(\Sigma)$ of {\em terms} over a signature $\Sigma$ is
defined recursively by:
\begin{itemise}
\item $V \subseteq \IT(\Sigma)$,
\item if $f \in \Sigma$ and $t_1,\ldots,t_{ar(f)} \in
\IT(\Sigma)$ then $f(t_1,\ldots,t_{ar(f)}) \in \IT(\Sigma)$.
\end{itemise}
A term $c()$ is abbreviated as $c$. For $t\in \IT(\Sigma)$,
$\var(t)$ denotes the set of variables that occur in $t$.
$T(\Sigma)$ is the set of closed terms over $\Sigma$, i.e.\
the terms $p \in \IT(\Sigma)$ with $\var(p)=\emptyset$.
A {\em $\Sigma$-substitution} $\sigma$ is a partial function from $V$
to $\IT(\Sigma)$. If $\sigma$ is a substitution and $S$ is any syntactic
object, then $\sigma(S)$ denotes the object obtained from $S$ by
replacing, for $x$ in the domain of $\sigma$, every occurrence of $x$
in $S$ by $\sigma(x)$. In that case $\sigma(S)$ is called a {\em
substitution instance} of $S$. A $\Sigma$-substitution is {\em closed} if
it is a total function from $V$ to $T(\Sigma)$.
\end{definition}
\begin{definition}\rm\label{df-TSS}
Let $\Sigma$ be a signature. A {\em positive $\Sigma$-literal} is an
expression $t \goto{a} t'$ and a {\em negative $\Sigma$-literal} an
expression $t \gonotto{a}$ with $t,t'\in \IT(\Sigma)$ and $a \in Act$.
A {\em transition rule} over $\Sigma$ is an expression of the form
$\frac{H}{\alpha}$ with $H$ a set of $\Sigma$-literals (the {\em
premises} of the rule) and $\alpha$ a positive $\Sigma$-literal (the
{\em conclusion}). The left- and right-hand side of $\alpha$ are
called the {\em source} and the {\em target} of the rule,
respectively. A rule $\frac{H}{\alpha}$ with $H=\emptyset$ is also
written $\alpha$. A \emph{transition system specification}
(\emph{TSS}), written $(\Sigma,R)$, consists of a signature $\Sigma$
and a set $R$ of transition rules over $\Sigma$. A TSS is {\em
positive} if the premises of its rules are positive.
\end{definition}
\begin{definition}\rm\label{df-GSOS}\cite{BIM95}
A \emph{GSOS} rule is a transition rule such that
\begin{itemise}
\item its source has the form $f(x_1,\ldots,x_{ar(f)})$ with $f\in
\Sigma$ and $x_i \in V$,
\item the left-hand sides of its premises are variables $x_i$ with
$1\leq i\leq ar(f)$,
\item the right-hand sides of its positive premises are variables that
that are all distinct, and that do not occur in its source,
\item its target only contains variables that also occur in its source
or premises.
\end{itemise}
A \emph{GSOS language}, or TSS in GSOS format, is a TSS whose rules
are GSOS rules.
\end{definition}
\begin{definition}\rm\label{df-transition}
A \emph{transition} over a signature $\Sigma$ is a closed positive
$\Sigma$-literal. With structural recursion on $p$ one defines when a
GSOS language $\GL$ generates a transition $p\goto{a}p'$ (notation
$p\goto{a}_\GL p'$):
$f(p_1,\ldots,p_n)\goto{a}_\GL q$ iff $\GL$ has a transition rule
$\frac{H}{f(x_1,...,x_n)\goto{a}t}$ and there is a closed substitution
$\sigma$ with $\sigma(x_i)=p_i$ for $i=1,...,n$ and $\sigma(t)=q$,
such that $p_i\goto{c}_\GL\sigma(y)$ for $(x_i\goto{c}y)\in H$ and
$\neg\exists r(p_i\goto{c}_\GL r)$ for $(x_i\gonotto{c})\in H$.
\end{definition}
Henceforth a GSOS language $\GL$ over a signature $\Sigma$ is assumed,
and closed $\Sigma$-terms will be called \emph{processes}. The
subscript $\GL$ will often be suppressed. Moreover, $Act=A\dcup\{\tau\}$
with $\tau$ the \emph{silent move} or \emph{hidden action}.
\begin{definition}\rm\label{df-bisimulation}
Two processes $t$ and $u$ are {\em weak bisimulation equivalent} or
{\em weakly bisimilar} ($t \bis{w} u$) if $t\rel u$ for a symmetric
binary relation $\rel$ on processes (a \emph{weak bisimulation})
satisfying, for $a\in Act$,
\begin{center}\hfill
if $p\rel q$ and $p \goto{a} p'$ then $\exists q_1, q_2, q'$ such
that $q\dto q_1\goto{\opt{a}}q_2\dto q' \wedge p' \rel q'$.
\hfill(*)
\end{center}
Here $p \dto p'$ abbreviates $p=p_0 \goto{\tau} p_1 \goto{\tau} \cdots
\goto{\tau} p_n = p'$ for some $n\geq 0$, whereas
$p\goto{\opt{a}}p'$ abbreviates $(p\goto{a}p') \vee
(a=\tau\wedge p=p')$.
$t$ and $u$ are {\em $\eta$-bisimilar} ($t \bis{\eta} u$) if in (*)
one additionally requires $p \rel q_1$;
$t$ and $u$ are {\em delay bisimilar} ($t \bis{d} u$) if in (*)
one additionally requires $q_2=q'$;
$t$ and $u$ are {\em branching bisimilar} ($t \bis{b} u$) if in (*)
one requires both;
$t$ and $u$ are {\em strongly bisimilar} ($t \bis{} u$) if in (*) one
simply requires $q\goto{a}q'$.
\\
Two processes $t$ and $u$ are {\em rooted weak bisimulation
equivalent} ($t \bis{rw} u$), if they satisfy
\begin{center}\vspace{-1pt}
\begin{tabular}{@{}l@{}}
if $t \goto{a} t'$ then $\exists u_1, u_2, u$ such
that $u\dto u_1\goto{a}u_2\dto u'$ and $t' \bis{w}
u'$, and\\
if $u \goto{a} u'$ then $\exists t_1, t_2, t$ such
that $t\dto t_1\goto{a}t_2\dto t'$ and $t' \bis{w} u'$.
\end{tabular}\vspace{-1pt}
\end{center}
They are {\em rooted $\eta$-bisimilar} ($t \bis{r\eta} u$) if above
one additionally requires $u_1=u$, $t_1=t$, and $t'\bis{\eta}u'$, they
are {\em rooted delay bisimilar} ($t \bis{rd} u$) if one requires
$u_2=u'$, $t_2=t'$ and $t'\bis{d}u'$, and they are {\em rooted
branching bisimilar} ($t \bis{rb} u$) if one requires $u_1=u$,
$u_2=u'$, $t_1=t$, $t_2=t'$ and $t'\bis{b}u'$.
\end{definition}
It is well known and easy to check that the nine relations on
processes defined above are equivalence relations indeed
\cite{Bas96,GW96}, and that, for $x \in \{$weak, $\eta$, delay,
branching, strong$\}$, $x$-bisimulation equivalence is the largest
$x$-bisimulation relation on processes. Moreover, $p\bis{rx}q$ implies
$p\bis{x}q$.
\begin{definition}\rm\label{df-congruence}
An equivalence relation $\sim$ on processes is a \emph{congruence} if
$$p_i \sim q_i \mbox{ for } i=1,\dots,ar(f) ~~\Rightarrow~~
f(p_1,\ldots,p_{ar(f)})\sim f(q_1,\ldots,q_{ar(f)})$$
for all $f\in\Sigma$.
This is equivalent to the requirement that for all $t \in \IT(\Sigma)$
and closed substitutions $\sigma, \nu: V \rightarrow T(\Sigma)$
$$\sigma(x) = \nu(x) \mbox{ for } x\in \var(t)
~~\Rightarrow~~ \sigma(t) = \nu(t).$$
\end{definition}
This note, and {\sc Bloom} \cite{Bl95}, deal with syntactic conditions
on GSOS languages that guarantee that the equivalence notions of
\df{bisimulation} are congruences.
\section{Simply Cool GSOS Languages}\label{simply cool}
In this section I define \emph{simply XB cool} rule formats, for
X$\in\{$W,D,H,B$\}$, such that on XB cool GSOS languages,
X-bisimulation equivalence is a congruence. In \cite{BIM95} it is
shown that strong bisimulation equivalence is a congruence on any GSOS
language. The proof is pretty straightforward; it consists of showing
that the congruence-closure of $\bis{}$ is a bisimulation. The same
idea can be applied almost verbatim to $\bis{w}$, $\bis{d}$,
$\bis{\eta}$ and $\bis{b}$, once we have lemmas like \lem{WB cool}
below. The simply XB cool formats contain the simplest syntactic
requirements that guarantee these lemmas to hold.
\begin{definition}\rm\label{df-straight}
Let $\GL$ be a positive GSOS language.
For an operator $f$ in $\GL$, the \emph{rules of $f$}
are the rules in $\GL$ with source $f(x_1,...,x_{ar(f)})$.
\begin{itemise}
\vspace{-1pt}
\item An operator in $\GL$ is \emph{straight} if it has no rules in
which a variable occurs multiple times in the left-hand side of
its premises. An operator is \emph{smooth} if moreover it has no
rules in which a variable occurs both in the target and in the
left-hand side of a premise.
\vspace{-1pt}
\item An argument $i\in\IN$ of an operator $f$ is \emph{active} if
$f$ has a rule in which $x_i$ appears as left-hand side of a premise.
\vspace{-1pt}
\item A variable $x$ occurring in a term $t$ is \emph{receiving} in
$t$ if $t$ is the target of a rule in $\GL$ in which $x$ is the
right-hand side of a premise. An argument $i\in\IN$ of an operator
$f$ is \emph{receiving} if a variable $x$ is receiving in a term $t$
that has a subterm $f(t_1,\ldots,t_n)$ with $x$ occurring in $t_i$.
\vspace{-3pt}
\item A rule of the form $\displaystyle
\frac{x_i\goto{\tau}y}{f(x_1,\ldots,x_n)\goto{\tau}f(x_1,\ldots,x_n)[y/x_i]}$
with $1\leq i\leq n$ is called a \emph{patience rule} for the
$i^{th}$ argument of $f$. Here $t[y/x]$ denotes term $t$ with all
occurrences of $x$ replaced by $y$.
\end{itemise}
\end{definition}
\begin{definition}\rm\label{df-simply cool}
A GSOS language $\GL$ is \emph{simply WB cool} if it is positive and
\begin{itemise}
\item[1.] all operators in $\GL$ are straight,
\item[2.] patience rules are the only rules in $\GL$ with $\tau$-premises,
\item[3.] every active argument of an operator has a patience rule,
\item[4.] every receiving argument of an operator has a patience rule,
\item[5.] all operators in $\GL$ are smooth.
\end{itemise}
The formats \emph{simply DB cool}, \emph{simply HB cool} and
\emph{simply BB cool} are defined likewise, but skipping Clause 4 for
DB and BB, and Clause 5 for HB and BB\@.
\end{definition}
The simply WB and BB cool formats above coincide with the ones of
\cite{Bl95}, whereas the simply DB cool format coincides with the {\tt
eb} format of \cite{UP02}.
\begin{lemma}\label{lem-WB cool}
Let $\GL$ be simply WB cool, let \plat{\frac{H}{s\goto{a}t}} be a rule in
$\GL$, and let $\nu$ be a closed substitution such that $\nu(x)\!\dto
\goto{\opt{c}} \dto \!\nu(y)$ for each premise $x\!\goto{c}\!y$ in $H$.\\
Then $\nu(s)\dto \goto{\opt{a}} \dto \nu(t)$.
\end{lemma}
Similar lemmas can be obtained for the other three formats, and these
yield the following congruence results. The proofs are in the full
version of this paper.
\begin{theorem}\label{thm-simply cool}
On any simply WB cool GSOS language, $\bis{w}$ is a congruence.
On any simply DB cool GSOS language, $\bis{d}$ is a congruence.
On any simply HB cool GSOS language, $\bis{\eta}$ is a congruence.
On any simply BB cool GSOS language, $\bis{b}$ is a congruence.
\end{theorem}
\section{Cool GSOS Languages}\label{cool}
In this section I will extend the simply XB cool rule formats to XB
cool rule formats and establish the associated congruence theorems
(X$\in\{$W,D,H,B$\}$).
\begin{definition}\rm\label{df-two-tiered}
A GSOS language is \emph{two-tiered} if its operators are partitioned
into \emph{abbreviations} and \emph{principal operators}, and for
every abbreviation $f$ a principal operator $f^\star$ is specified,
together with a substitution\\
$\sigma\!_f:\{x_1,\ldots,x_{ar(f^\star)}\}\rightarrow\{x_1,\ldots,x_{ar(f)}\}$,
such that the rules of $f$ are $$\displaystyle\left\{
\frac{\sigma\!_f(H)}{f(x_1,\ldots,x_{ar(f)})\goto{a}\sigma\!_f(t)}
\;\left|\; \frac{H}{f^\star(x_1,\ldots,x_{ar(f^*)})\goto{a}t} \mbox{
is a rule of } f^\star\right.\right\}.$$ Write $f(i)$ for the $j$ such
that $\sigma\!_f(x_i)=x_j$; take $f^\star=f$ and $f(i)=i$ in case $f$
is a principal operator.
\end{definition}
Trivially, any positive GSOS language can be extended
(\emph{straightened}) to a two-tiered GSOS language whose principal
operators are straight and smooth \cite{ABV94}.
\begin{example}\label{ex-straightening}
Let $\GL$ have an operator $f$ with rule \raisebox{-3pt}[0pt][7pt]{$
\displaystyle\frac{x_1\goto{a}y,~~x_1\goto{b}z}{f(x_1,x_2)\goto{a}
f(x_1,(f(y,x_2))}$}.
$\GL$ is straightened by adding a operator $f^\star$ with\vspace{-3pt}
$$\displaystyle \frac{x_1\goto{a}y,~~x_2\goto{b}z}
{f^\star(x_1,x_2,x_3,x_4)\goto{a}f(x_3,f(y,x_4))}.$$ In this case
$\sigma\!_f(x_1)=\sigma\!_f(x_2)=\sigma\!_f(x_3)=x_1$ and
$\sigma\!_f(x_4)=x_2$.
\end{example}
Equally trivial,
$f^\star(p_{f(1)},...,p_{f(n)})\goto{a}t$ iff
$f(p_1,...,p_n)\goto{a}t$;\\ so
$f^\star(p_{f(1)},...,p_{f(n)})\bis{} f(p_1,...,p_n)$.
\begin{definition}\rm\label{df-cool}
A two-tiered GSOS language $\GL$ is \emph{WB cool} if it is positive and
\begin{itemise}
\item[1.] all principal operators in $\GL$ are straight,
\item[2.] patience rules are the only rules of principal operators
with $\tau$-premises,
\item[3.] every active argument of a principal operator has a patience rule,
\item[4.] if argument $f(i)$ of $f$ is receiving, then
argument $i$ of $f^\star$ has a patience rule,
\item[5.] all principal operators in $\GL$ are smooth.
\end{itemise}
The formats \emph{DB cool}, \emph{HB cool} and \emph{BB cool} are
defined likewise, but skipping Clause 4 for DB and BB, and Clause 5
for HB and BB\@. Clause 4 may be weakened slightly; see \sect{extension}.
\end{definition}
Note that the simply cool formats defined before are exactly the cool formats
with the extra restriction that all operators are principal.
\begin{theorem}\label{thm-cool}
On any WB cool GSOS language, $\bis{w}$ is a congruence.
On any DB cool GSOS language, $\bis{d}$ is a congruence.
On any HB cool GSOS language, $\bis{\eta}$ is a congruence.
On any BB cool GSOS language, $\bis{b}$ is a congruence.
\end{theorem}
Given that the cool GSOS languages differ from the simply cool GSOS
language only by the addition of operators that can be regarded as
syntactic sugar, the theorems above are a simple consequence of the
corresponding theorems for simply cool GSOS languages. Details are in
the full version of this paper.
\subsection{A Small Extension}\label{extension}
Say that an argument $i$ of an operator $f$ is \emph{ignored} if
$f^\star$ has no argument $k$ with $f(k)=i$. In that case there can be
no rule with source $f(x_1,\ldots,x_{ar(f)})$ with $x_i$ in its
premises or in its target. A subterm $u$ of a term $t$ is
\emph{irrelevant} if occurs within an ignored argument $t_i$ of a
subterm $f(t_1,\ldots,t_{ar(f)})$ of $t$. Now \df{straight} of an
argument of an operator being receiving may be strengthened by
replacing ``a subterm $f(t_1,\ldots,t_n)$ with $x$ occurring in
$t_i$'' by ``a relevant subterm $f(t_1,\ldots,t_n)$ with $x$ a
relevant subterm of $t_i$''. This yields a slight weakening of Clause
4 in \df{cool}, still sufficient to obtain \thm{cool}.\vspace{-1pt}
\begin{example}\label{ignored variables} Let $\GL$ have a rule
$\displaystyle\frac{x_1\goto{a}y}{g(x_1)\goto{a}f(h(f(x_1,y)),k(y))}$.
By \df{straight} both the arguments of $h$ and $k$ are receiving, so
Clause 4 in \df{cool} demands patience rules for both $h^\star$ and
$k^\star$. Now suppose that $h^\star=h$, $k^\star=k$, $ar(f^\star)=1$
and $\sigma\!_f(x_1)=x_1$. This means that $f(x_1,x_2)$ is an
abbreviation for $f^\star(x_1)$ and the second argument of $f$ is
ignored. In such a case $f(p,q) \bis{} f(p,r)$ for all closed terms
$p$, $q$ and $r$. Now the weakened Clause 4 does not demand a
patience rule for either $h^\star$ or $k^\star$, since the arguments
of $h$ and $k$ are no longer receiving.
\end{example}
\section{Rooted Cool GSOS Languages}\label{rooted}
In this section I will define the (simply) RWB, RDB, RHB and RBB cool
rule formats and establish the associated congruence theorems.
In order to formulate the requirements for the RWB and RDB cool GSOS
languages I need the concept of a \emph{ruloid}, this being a kind of
derived GSOS rule.
\begin{definition}\rm\label{df-ruloid}
For $r$ transition rule, let RHS($r$) denote the set of right-hand sides
of its premises. Let $\GL$ be a positive GSOS language.
The class of \emph{$\GL$-ruloids} is the smallest set of rules such that
\begin{itemise}
\item $\frac{x\goto{a}y}{x\goto{a}y}$ is an $\GL$-ruloid, for every
$x,y\in V$ and $a\in Act$;
\item if $\sigma$ is a substitution, $\GL$ has a rule $\frac{H}{s\goto{a}t}$,
and for every premise $x\goto{c}y$ in $H$ there is an $\GL$-ruloid
\plat{r_y=\frac{H_y}{\sigma(x)\goto{c}\sigma(y)}}\vspace{7pt}
such that the sets RHS($r_y$) are pairwise disjoint and
each RHS($r_y$) is disjoint with $\var(\sigma(s))$, then
\plat{\frac{\bigcup_{y\in H}H_y}{\sigma(s)\goto{a}\sigma(t)}}
is an $\GL$-ruloid.
\end{itemise}
\end{definition}
Note that a transition $\alpha$, seen as a rule
\plat{\frac{\emptyset}{\alpha}}, is an $\GL$-ruloid iff it is generated by
$\GL$ in the sense of \df{transition}. The left-hand sides of
premises of a ruloid are variables that occur in its source, and the
right-hand sides are variables that are all distinct and do
not occur in its source. Its target only contains variables that also
occur elsewhere in the rule.\vspace{-7pt}
\begin{example}\label{ruloid}
Let $\GL$ contain the rule $\displaystyle
\frac{x_1\goto{a}y_1~~~x_2\goto{b}y_2}{f(x_1,x_2)\goto{a}g(x_1,y_1)}$.
Then $\GL$ has ruloids \centerline{\plat{\displaystyle
\frac{x\goto{a}x'~~~y\goto{b}y'}{f(x,y)\goto{a}g(x,x')}}
~~and~~
$\displaystyle\frac{x\goto{a}x'~~~y\goto{b}y'~~~z\goto{b}z'}
{f(f(x,y),z)\goto{a}g(f(x,y),g(x,x'))}$.}
\end{example}
\begin{definition}\rm\label{df-RWB cool}
A GSOS language $\GL$ is \emph{RWB cool} if
the operators can be partitioned in \emph{tame} and \emph{wild} ones,
such that
\begin{itemise}
\item[1.] the target of every rule contains only tame operations;
\item[2.] the sublanguage $\GL^{tame}$ of tame operators in $\GL$ is WB cool;
\item[3.] $\GL$ is positive, and for each rule
\plat{\frac{H}{s\goto{a}t}} there is a term $u$ and
a substitution $\sigma:\var(u)\rightarrow \var(s)$ such that\vspace{-2pt}
\begin{itemise2}
\item there is an $\GL$-ruloid \plat{\frac{K}{u\goto{a}v}} with
$\sigma(K)=H$ and $\sigma(v)=t$,
\item and for every premise $x \goto{c} y$ in $K$, $\GL$ has a rule
\plat{\frac{\sigma(x)\goto{\tau}y}
{s\goto{\tau}\sigma(u[y/x])}};
\end{itemise2}
\item[(4.]
if argument $f(i)$ of $f$ is receiving, then
argument $i$ of $f^\star$ has a patience rule.)
\end{itemise}
The formats \emph{RDB cool}, \emph{RHB cool} and \emph{RBB cool} are
defined likewise, adapting ``WB cool'' in the second clause
appropriately, but skipping the third clause for RHB and RBB, and the
last one for RDB and RBB\@. The last clause cannot be skipped for
RHB. The \emph{simply RXB cool} rule formats (X$\in\{$W,D,H,B$\}$) are
obtained by requiring the sublanguage of tame operators to be simply
XB cool.
\end{definition}
Note that in the third clause, $u$, $\sigma$ and the ruloid can always
be chosen in such a way that $v=t$. The instance of this clause with
$s=f(x_1,\ldots,x_{ar(f)})$ for a tame operator $f$ is (in the full
version of this paper) easily seen to be redundant.
The last clause above appeared before as Clause 4 in \df{cool} of the
WB and HB cool formats. Given that a term with a receiving variable
cannot contain wild operators, this clause is almost implied by Clause
2 above. All it adds, is that the requirement of Clause 4 for the
sublanguage of tame operators applies to ``receiving in $\GL$''
instead of merely ``receiving in $\GL^{tame}$\,''. Thus, the rules
for the wild operators help determine which variables in a term $t$
count as receiving. The following results are obtained in the full
version of this paper.
\begin{proposition}\label{pr-RWB cool}
In the definition of RWB cool above, Clause 4 is redundant.
\end{proposition}
\begin{theorem}\label{thm-rooted weak}
On any RWB cool GSOS language, $\bis{rw}$ is a congruence.
On any RDB cool GSOS language, $\bis{rd}$ is a congruence.
On any RHB cool GSOS language, $\bis{r\eta}$ is a congruence.
On any RBB cool GSOS language, $\bis{rb}$ is a congruence.
\end{theorem}
\begin{example}\label{ex-CCS}
The following fragment of CCS has the constant 0, unary operators
$a.\_\,$, binary operators + and $\|$, and
instances of the GSOS rules below. Here $a$ ranges over \plat{Act =
\names \dcup \overline\names \dcup \{\tau\}} with $\names$ a set of
\emph{names} and $\overline\names=\{\overline a \mid a\in\names\}$ the
set of \emph{co-names}. The function $\overline \cdot$ extends to
$\names \cup \overline\names$ (but not to $Act$) by
$\overline{\overline a}=a$.\vspace{-5pt}
$$\begin{array}{c}\displaystyle
\frac{x_1 \goto{a} y_1}{x_1+x_2 \goto{a} y_1}~~~~~
\frac{x_2 \goto{a} y_2}{x_1+x_2 \goto{a} y_2}~~~~~
a.x_1 \goto{a} x_1
\\[12pt]\displaystyle
\frac{x_1 \goto{a} y_1}{x_1 \| x_2 \goto{a} y_1\|x_2}~~~~~
\frac{x_2 \goto{a} y_2}{x_1 \| x_2 \goto{a} x_1\|y_2}~~~~~
\frac{x_1 \goto{a} y_1~~~x_2 \goto{\overline a} y_2}{x_1 \| x_2
\goto{\tau} y_1\|y_2}
\end{array}$$
The sublanguage without the + is simply WB cool, and the entire GSOS
language is simply RWB cool. Clause 3 of \df{RWB cool} applied to the
$i^{th}$ rule for the $+$ is satisfied by taking $u=x$, $\sigma(x)=x_i$,
and the ruloid \plat{\;\frac{x\goto{a}y_i}{x\goto{a}y_i}}.
\end{example}
\section{Comparison with Bloom's Formats}\label{Bloom}
Bloom's definitions of the cool formats differ in five ways from mine.
First of all Bloom requires \emph{bifurcation rules} for all operators
in $\GL^{tame}$, whereas I merely require patience rules for the
principal operators. As principal operators in $\GL^{tame}$ are
straight, and bifurcation rules for straight operators are exactly
patience rules, the difference is that I dropped the bifurcation
requirement for abbreviations (non-principal operators). This is
possible, because by \df{two-tiered}, which corresponds to Definition
3.5.5 in \cite{Bl95}, the rules for the abbreviations are completely
determined by the rules for their straightenings, and it turns out
that a bifurcation rule of an abbreviation $f$ is exactly what is
determined by the corresponding patience rule for its straightening
$f^\star$.
Bloom requires the existence of bifurcation/patience ruloids for receiving
variables in any term, whereas I require them for receiving arguments
of operators, which is a more syntactic and easy to check requirement.
The two approaches are shown equivalent in the full version of this
paper when using the extension of my formats of \sect{extension},
this being the reason behind that extension.
Bloom's WB and RWB cool formats use a so-called
\emph{$\varepsilon$-presentation}. This entails that rules may have
premises of the form $x \goto{\varepsilon} y$. In terms of
\df{transition}, the meaning of such premises is given by the
requirement that $\sigma(x)=\sigma(y)$ for
\plat{(x\goto{\varepsilon}y)\in H}. By using $\varepsilon$-premises,
any rule can be given a form in which the target is a univariate term,
having no variables in common with the source. This allows a
simplification of the statement of the bifurcation ruloids. Any
$\varepsilon$-presented GSOS language can be converted to
$\varepsilon$-free form by substitution, in each rule $r$, $x$ for $y$
for every premise $x\goto{\varepsilon}y$ of $r$.
I believe that my conventions for naming variables improve the ones of
\cite{Bl95}.
%\input{diagram}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\graphtemp=.5ex\advance\graphtemp by 0.085in
\rlap{\kern 0.300in\lower\graphtemp\hbox to 0pt{\hss $s$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.085in
\rlap{\kern 0.800in\lower\graphtemp\hbox to 0pt{\hss $t$\hss}}%
\special{pn 8}%
\special{ar 180 635 130 130 0 6.28319}%
\special{sh 0.000}%
\special{ia 300 585 85 85 0 6.28319}%
\special{ar 920 635 130 130 0 6.28319}%
\special{sh 0.000}%
\special{ia 800 585 85 85 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.585in
\rlap{\kern 0.300in\lower\graphtemp\hbox to 0pt{\hss $t_1$\hss}}%
\special{pa 150 510}%
\special{pa 245 520}%
\special{fp}%
\special{sh 1.000}%
\special{pa 148 485}%
\special{pa 245 520}%
\special{pa 143 534}%
\special{pa 148 485}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.585in
\rlap{\kern 0.800in\lower\graphtemp\hbox to 0pt{\hss $t_2$\hss}}%
\special{pa 950 510}%
\special{pa 855 520}%
\special{fp}%
\special{sh 1.000}%
\special{pa 957 534}%
\special{pa 855 520}%
\special{pa 952 485}%
\special{pa 957 534}%
\special{fp}%
\special{pa 300 170}%
\special{pa 300 500}%
\special{fp}%
\special{sh 1.000}%
\special{pa 325 400}%
\special{pa 300 500}%
\special{pa 275 400}%
\special{pa 325 400}%
\special{fp}%
\special{pa 800 170}%
\special{pa 800 500}%
\special{fp}%
\special{sh 1.000}%
\special{pa 825 400}%
\special{pa 800 500}%
\special{pa 775 400}%
\special{pa 825 400}%
\special{fp}%
\special{pa 385 85}%
\special{pa 715 85}%
\special{fp}%
\special{sh 1.000}%
\special{pa 615 60}%
\special{pa 715 85}%
\special{pa 615 110}%
\special{pa 615 60}%
\special{fp}%
\special{pa 360 145}%
\special{pa 740 525}%
\special{fp}%
\special{sh 1.000}%
\special{pa 687 437}%
\special{pa 740 525}%
\special{pa 652 472}%
\special{pa 687 437}%
\special{fp}%
\special{pa 360 525}%
\special{pa 740 145}%
\special{fp}%
\special{sh 1.000}%
\special{pa 652 198}%
\special{pa 740 145}%
\special{pa 687 233}%
\special{pa 652 198}%
\special{fp}%
\special{pa 385 585}%
\special{pa 715 585}%
\special{fp}%
\special{sh 1.000}%
\special{pa 615 560}%
\special{pa 715 585}%
\special{pa 615 610}%
\special{pa 615 560}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.020in
\rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.195in
\rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.640in
\rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.465in
\rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $a$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.285in
\rlap{\kern 0.240in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.285in
\rlap{\kern 0.860in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.635in
\rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.635in
\rlap{\kern 1.100in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize $\tau$}\hss}}%
\hbox{\vrule depth0.765in width0pt height 0pt}%
\kern 1.100in
}%
}%
\noindent
\begin{minipage}[t]{3.5in}
\hspace{1.5em}%
Bloom's rendering of the RWB cool format doesn't feature Clause 4
(and in view of \pr{RWB cool}, neither does mine), but Clause 3 is
much more involved. For every rule with conclusion $s\goto{a}t$ Bloom
requires the existence of two terms $t_1$ and $t_2$ and seven types of
derived operational rules, such that the diagram on the right commutes.
My\linebreak[2]\vspace{-8pt}
\end{minipage}
\hfill\box\graph\,\mbox{} Clause 3 stems from the observation that,
given Bloom's other restrictions, $t$ necessarily has the rules
required for $t_2$, so that one may always choose $t_2=t$. This leaves
only $t_1$ (called $u$ in \df{RWB cool}) and three types of rules, one
of which (the $t_1$-loop in the diagram above) is in fact a
bifurcation rule whose existence is already implied by the
requirements of \df{cool}.
In Clause 3 of \df{RWB cool}, Bloom requires that
\begin{equation}\label{var(u)}
\var(u)=\{y'\mid y\!\in\!\var(t)\}\mbox{ and }
\sigma(y')=\left\{\begin{array}{@{}l@{}}x\mbox{ if $H$ contains
a premise \plat{x\goto{c}y}}\\y\mbox{ otherwise.}
\end{array}\right.
\end{equation}
In order to match Bloom's format I
could have done the same, but this condition is not needed in the
proof and reduces the generality of the format.
\begin{proposition}\label{pr-bloom}
A GSOS language is WB cool, respectively RWB, BB or RBB cool, as
defined here, with the extension of \sect{extension} and the
restriction \mbox{\rm (\ref{var(u)})} above, iff it is WB cool, resp.\
RWB, BB or RBB cool, as defined in {\sc Bloom \cite{Bl95}}.
\end{proposition}
Moreover, my proofs that cool languages are compositional for bisimulation
equivalences greatly simplify the ones of Bloom \cite{Bl95} by using a
reduction of the general case to the simple case, instead of treating
the general formats directly.
\section{Turning GSOS Rules into Equations}
\label{sec-equations}
This section recapitulates the method of \cite{ABV94} to provide
finite equational axiomatisations of $\bis{}$ on an augmentation of
any given GSOS language.
\begin{definition}\rm
A process $p$, being a closed term in a GSOS language, is
\emph{finite} if there are only finitely many sequences of transitions
$p \goto{a_1} p_1 \goto{a_2} \cdots \goto{a_n} p_n$.
The length $n$ of the longest sequence of this form is called the
\emph{depth} of $p$.
\end{definition}
\begin{definition}\rm
An \emph{equational axiomatisation} Ax over a signature $\Sigma$ is
a set of equations $t=u$, called \emph{axioms}, with $t,u\in
\IT(\Sigma)$. It \emph{respects} an equivalence relation $\sim$ on
$T(\Sigma)$ if $\sigma(t)\sim\sigma(u)$ for any closed substitution
$\sigma:V\rightarrow T(\Sigma)$.
An \emph{instance} of axiom $t=u$ is an equation
$\sigma(C[t/x])=\sigma(C[u/x])$ where $\sigma$ is a substitution and
$C$ a term with $\var(C)\!=\!\{x\}$, and $x$ occurring only once in $C$.
An equation $p=q$ is \emph{derivable} from Ax, notation $p=_{\rm Ax}q$,
if there is a sequence $p_0,\ldots,p_n$ of terms with $n\geq 0$ such
that $p=p_0$, $q=p_n$ and for $i=1,\ldots,n$ the equation
$p_{i-1}=p_i$ is an instance of one of the axioms.
Ax is \emph{sound} for $\sim$ if $p=_{\rm Ax}q$ implies $p\sim q$
for $p,q\in T(\Sigma)$.
Ax is \emph{complete for $\sim$ on finite processes} if $p\sim q$
implies $p=_{\rm Ax}q$ for finite processes $p$ and $q$.
\end{definition}
Note that Ax is sound for $\sim$ iff Ax respects $\sim$ and $\sim$ is a
congruence.
\begin{definition}\em\label{df-basic}
A GSOS language $\GL$ \emph{extends BCCS} (\emph{basic} CCS) if it contains
the operators 0, $a.\_\,$ and $+$ of \ex{CCS}.\\
A \emph{basic process} is a closed term
build from the operators mentioned above only.
A \emph{head normal form} is a closed term
of the form $0 + a_1.p_1 + \cdots + a_n.p_n$ for $n\geq 0$.
An axiomatisation on $\GL$ is \emph{head normalising} if any term
$f(p_1,\ldots,p_{ar(f)})$ with the $p_i$ basic processes
can be converted into head normal form.
\end{definition}
\begin{proposition}
\begin{table}[b]
\vspace{-1.7em}
$$\begin{array}{@{}rcl@{~~~}l@{~~~~~~~~~}r@{~=~}l@{~~~{\rm CM}}c@{}}
x+(y+z)&=&(x+y)+z &{\rm A1}& x\|y & x\leftmerge y + y\leftmerge x + x|y &1\\
x+y &=& y+x &{\rm A2}& a.x\leftmerge y& a.(x\| y) &2\\
x+x &=& x &{\rm A3}& 0\leftmerge y & 0 &3\\
x+0 &=& x &{\rm A4}&(x+y)\leftmerge z &x\leftmerge z+y\leftmerge z&4\\
&& & & a.x | \overline a.y & \tau.(x\|y) &5\\
a.(\tau.(x+y)+x)&=&a.(x+y)&{\rm T1}& a.x|b.y &
0~~~~~~~~~~~(\mbox{if }b\neq\overline a)&6\\
\tau.x+x&=&\tau.x &{\rm T2}& 0|x & x|0 ~=~ 0 &7\\
a.(\tau.x+y)+a.x&=&a.(\tau.x+y)&{\rm T3}&(x+y)|z&x|z+y|z &8\\
&& & & x|(y+z) & x|y + x|z &9\\
\end{array}$$
\caption{Complete equational axiomatisations of BCCS and the parallel
composition}\label{BCCS}
\vspace{-1em}
\end{table}
Let $\GL$ be a GSOS language extending BCCS, and {\rm Ax} a head
normalising equational axiomatisation, respecting $\bis{\!}$, and
containing the axioms {\rm A1--4} of Table~\ref{BCCS}. Then {\rm Ax} is
sound and complete for $\bis{\!}$ on finite processes.
\end{proposition}
\begin{proof}
Using induction on the depth of $p$ and a nested structural induction,
the axioms can convert any finite process $p$ into a basic process.
Here one uses that strongly bisimilar processes have the same depth.
Now apply the well-known fact that the axioms A1--4 are
sound and complete for $\bis{\!}$ on basic processes \cite{Mi90ccs}.
\end{proof}
For the parallel composition operator $\|$ of CCS no finite equational
head normalising axiomatisation respecting strong bisimulation
equivalence exists \cite{Mo90a}. However, {\sc Bergstra \& Klop}
\cite{BK85} gave such an axiomatisation on the language obtained by
adding two auxiliary operators, the \emph{left merge}
$\leftmerge$\vspace{-1ex} and the \emph{communication} merge $|$, with
rules $\displaystyle \frac{x_1 \goto{a} y_1}{x_1 \leftmerge x_2
\goto{a} y_1\|x_2}$ and $\displaystyle\frac{x_1 \goto{a}
y_1~~~x_2 \goto{\overline a} y_2}{x_1|x_2 \goto{\tau} y_1\|y_2}$,
provided the alphabet $Act$ of actions is finite. The axioms are CM1--9
of Table~\ref{BCCS}, in which + binds weakest and $a.\_\,$ strongest,
and $a,b$ range over $Act$.
{\sc Aceto, Bloom \& Vaandrager} \cite{ABV94} generalise this idea to
arbitrary GSOS languages with finitely many rules, each with
finitely many premises, and assuming a finite alphabet $Act$. I
recapitulate their method for positive languages only.
A smooth
operator (\df{straight}) only has rules of the form $\displaystyle
\frac{\{x_i \goto{c_i} y_i \mid
i\!\in\!I\}}{f(x_1,\ldots,x_n)\goto{a}t}$. The \emph{trigger} of such
a rule is the partial function $\uparrow_r:
\{i,\ldots,n\}\rightharpoonup Act$ given by $\uparrow_r(i)=c_i$ if
$i\!\in\!I$, and $\uparrow_r(i)$ is undefined otherwise.
\begin{definition}\em\label{distinctive}\cite{ABV94}
A smooth GSOS operator $f$ is \emph{distinctive}, if no two rules of
$f$ have the same trigger, and the triggers of all rules of $f$ have
the same domain.
\end{definition}
All operators of CCS, as well as \plat{\leftmerge} and $|$, are smooth.
The operators $0$, $a.\_\,$, \plat{\leftmerge} and $|$ are
distinctive, but $\|$ is not. Its triggers have
domains $\{1\}$, $\{2\}$ and $\{1,2\}$.
For every smooth and distinctive operator $f$,
{\sc Aceto, Bloom \& Vaandrager} declare four types of axioms.
First of all, for every rule $r$ as above there is an axiom
$f(\sigma(x_1),\ldots,\sigma(x_n))=a.\sigma(t)$, where
$\sigma:\{x_1,\ldots,x_n\}\rightarrow \IT(\Sigma)$ is the substitution
given by $\sigma(x_i)=c_i.y_i$ for $i\!\in\!I$ and $\sigma(x_i)=x_i$
for $i\!\not\in\!I$. Such an axiom is called an \emph{action law}.
Examples are CM2 and CM5 in Table~\ref{BCCS}.
Secondly, whenever $I$ is the set of active arguments of $f$, but $f$
has no rule of the form above (where the name of the variables $y_i$
is of no importance), there is an axiom
$f(\sigma(x_1),\ldots,\sigma(x_n))=0$, with $\sigma$ as above (for an
arbitrary choice of distinct variables $y_i$). Such an axiom is an
\emph{inaction law}. An example is CM6. If $f$ has $k$ active
arguments, in total there are $|Act|^k$ action and inaction laws for
$f$, one for every conceivable trigger with as domain the active
arguments of $f$.
Finally, for any active argument $i$ of $f$, there are laws\vspace{-1ex}
\[ f(x_1,\ldots x_{i-1},0,x_{i+1},\ldots,x_n) = 0~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~\mbox{and}\]\vspace{-2em}
\[f(x_1,\ldots,x_i+x_i',\ldots,x_n) =
f(x_1,\ldots,x_i,\ldots,x_n) + f(x_1,\ldots,x_i',\ldots,x_n).\]
Examples for the second type of {inaction law} are CM3 and CM7,
and examples of \emph{distributivity laws} are CM4, CM8 and CM9.
It is not hard to see that all axioms above respect $\bis{}$ and that
together they bring any term $f(p_1,\ldots,p_{ar(f)})$ with the $p_i$
basic processes in head normal form.
The method of \cite{ABV94} makes three types of additions to a given
finite GSOS language $\GL$, and provides an equational head
normalising axiomatisation on the resulting language, that respects
strong bisimulation.
First of all, the operators $0$, $a.\_\,$ and $+$ are added, if not
already there. The corresponding axioms are A1--4 of
Table~\ref{BCCS}. If all other operators are smooth and distinctive, for
each of them the axioms just described are taken, which finishes the
job. (In the presence of negative premises, this step is slightly more
complex.)
In case there are operators $f$ that are smooth but not distinctive, the
set of operational rules of $f$ is partitioned into subsets $D$ such
that no two rules in $D$ have the same trigger, and the triggers of
all rules in $D$ have the same domain. Note that such a partition
can always be found---possibly by taking exactly one rule in each subset
$D$. Now for any subset $D$ in the partition, an operator $f_D$ with
$ar(f_D)=ar(f)$ is added to the language, whose rules are exactly the
rules in that subset, but with $f_D$ in the source. By definition,
$f_D$ is distinctive. Now add an axiom $f(x_1,\ldots,x_{ar(f)}) =
\sum f_D(x_1,\ldots,x_{ar(f)})$, where the sum is taken over all
subsets in the partition, and apply the method above to the operators
$f_D$. Again, it is trivial to check that the axioms respect $\bis{}$
and are head normalising.
Applied to the $\|$ of CCS, this technique yields the left merge and
communication merge as auxiliary operators, as well as a right
merge, and the axiom CM1.
In case of operators $f$ that are not smooth, a smooth operator
$f^\star$ is added to $\GL$, of which $f$ is an abbreviation
in the sense of \df{two-tiered} (cf.\ \ex{straightening}).
The treatment of $f^\star$ proceeds as above, and the project is
finished by the axiom $$f(p_1,...,p_n)=f^\star(p_{f(1)},...,p_{f(n)}).$$
Besides completeness for finite processes, using an infinitary
induction principle the method of \cite{ABV94} even yields
completeness for arbitrary processes. I will not treat this here, as
it does not generalise to weak equivalences.
\section{Turning Cool GSOS Rules into Equations}
\label{sec-cool-equations}
The method of \cite{ABV94} does not apply to $\bis{w}$, $\bis{d}$,
$\bis{\eta}$, and $\bis{b}$, because these equivalences fail to be
congruences for the $+$. However, Bloom \cite{Bl95} shows that the
method applies more or less verbatim to $\bis{rb}$. This section
observes that the same holds for $\bis{r\eta}$, and finds an
adaptation to yield finite equational axiomatisations of
$\bis{rw}$ (resp.\ $\bis{rd}$) that are sound and complete for finite
processes on an augmentation of any RWB cool (resp.\ RDB cool) GSOS
language.
On basic processes, the axioms A1--4 together with T1--T3 are complete
for $\bis{rw}$ \cite{Mi90ccs}, whereas complete axiomatisations for
$\bis{rd}$, $\bis{r\eta}$ and $\bis{rb}$ are obtained by dropping T3,
T2 or both, respectively \cite{GW96}. So in order to get
axiomatisations of these equivalences that are complete for finite processes,
all that is needed is head normalisation. The simplest approach is to
use the same head normalising axioms as in the previous section,
reasoning that axioms that respect $\bis{}$ surely respect a coarser
equivalence like $\bis{rb}$ or $\bis{rw}$. The only way this approach
could fail is when the auxiliary operators generated by \cite{ABV94}
fail to be congruences for the equivalence relation at hand. The
operators $0$, $a.\_\,$ and $+$ are WB cool, and thus
unproblematic. As observed in \cite{Bl95}, for any RBB cool GSOS
language, the augmented language is also RBB cool. Namely, the new
operators do not show up in targets of new rules, so classifying all
auxiliary operators as wild is sufficient. Since the auxiliary
operators do not increase the collection of receiving arguments of
operators either, it follows likewise that for any RHB cool GSOS
language, the augmented language is also RHB cool. Hence one obtains
\begin{proposition}
The method of \cite{ABV94}, together with axiom T1 (and T3), yields
finite equational axiomatisations of $\bis{rb}$ (resp.\ $\bis{r\eta}$)
that are sound and complete for finite processes on an augmentation of
any RBB cool (resp.\ RHB cool) GSOS language.
\end{proposition}
For $\bis{rw}$ and $\bis{rd}$ this approach fails. In particular,
these equivalences fail to be congruences for the communication merge:
one has $\tau.a.0 \bis{rd} \tau.a.0+a.0$ but $$0 \bis{}
(\tau.a.0 | \overline{a}.b.0) \nobis{rd} ((\tau.a.0+a.0)|\overline a.b.0)
\bis{} \tau.b.0.$$
\begin{trivlist} \item[\hspace{\labelsep}\bf Conjecture.]\it
There exists no GSOS language including the parallel composition of
CCS and $\geq\!2$ visible actions that admits a finite equational
axiomatisation of weak bisimulation equivalence that is sound and
complete for finite processes.
\end{trivlist}
Nevertheless, such an axiomatisation was found by {\sc Bergstra \&
Klop} \cite{BK85}, using a variant of the communication merge that is
not a GSOS operator. Their axiomatisation of $\|$ is obtained from the
one in Table 1 by requiring $a,b\neq\tau$ in CM6, and adding
the axioms $\tau.x|y = x|\tau.y = x|y$. Here I generalise their
approach to arbitrary RWB cool (or RDB cool) GSOS languages.
The RWB cool format can be extended by allowing wild operators $f$,
besides GSOS rules satisfying Clause 3 of \df{RWB cool}, also to have
rules of which all premises have the form $x \dto\goto{c}y$ with $c\in
A$. For such rules Clause 3 is not required, but in fulfilling
Clause 4, they do count in determining which arguments are
receiving. A similar extension applies to the RDB cool format.
\begin{theorem}\label{thm-extended cool}
On any extended-RWB cool TSS, $\bis{rw}$ is a congruence.
On any extended-RDB cool TSS, $\bis{rd}$ is a congruence.
\end{theorem}
In an RWB (or RDB) cool language, the smooth operators $f^\star$ that
are needed to axiomatise a non-smooth operator $f$ are unproblematic.
For tame operators $f$, they are already in the language, and for a
wild $f$ it is not hard to define them in such a way that the
augmented language remains RWB (or RDB) cool. Of the operators $f_D$
needed to axiomatise a non-distinctive operator $f$, those that have
exactly one active argument can be made to satisfy Clause 3 of \df{RWB
cool} by including the relevant $\tau$-rule in $D$. All operators
$f_D$ with another number of active arguments cannot have
$\tau$-premises, by Definitions~\ref{df-RWB cool}
and~\ref{df-cool}. These operators $f_D$ are replaced by counterparts
$f'_D$, obtained by replacing each premise $x\goto{c}y$ in a rule for
$f_D$ by $x\dto\goto{c}y$. By \thm{extended cool}, $\bis{rw}$ (or
$\bis{rd}$) is a congruence for $f'_D$. Furthermore,
$f(x_1,\ldots,x_{ar(f)}) \bis{rw} \sum f'_D(x_1,\ldots,x_{ar(f)})$.
Now the required axiomatisation is obtained by omitting all inaction
laws for the modified operators $f'_D$ with $\sigma(x_i)=\tau.y_i$ for
some active argument $i$, and instead adding \emph{$\tau$-laws}
$f'_D(x_1,\ldots,\tau.x_i,\ldots,x_n) = f'_D(x_1,\ldots,x_i,\ldots,x_n).$
\section{A Challenge}\label{challenge}
All equivalences of \df{bisimulation} are congruences of the GSOS
language with rules\vspace{-1.5ex}
$$\frac{x_1\goto{a}y}{f(x_1)\goto{a}g(y)} ~~~~~
\frac{x_1\goto{\tau}y}{g(x_1)\goto{\tau}g(y)} ~~~~~ g(x_1)\goto{\tau} !x_1$$
\vspace{-1ex}
$$\frac{x_1\goto{a}y}{!x_1\goto{a}y\|!x_1}~~~~~
\frac{x_1 \goto{a} y_1}{x_1 \| x_2 \goto{a} y_1\|x_2}~~~~~
\frac{x_2 \goto{a} y_2}{x_1 \| x_2 \goto{a} x_1\|y_2}$$
for $a\!\in\!Act$. Here, the operator $!x$ can be understood as a
parallel composition of infinitely many copies of $x$. The rules for
$f$, $g$ and $\|$ are WB cool, but the one for $!$ is not. It is not
even RBB safe in the sense of \cite{Fok00b}.\\[1ex]
{\bf Open problem.\,} Find a congruence format that includes the
language above.
%\bibliography{/import/mellotron/1/rvg/Stanford/lib/abbreviations,/import/mellotron/1/rvg/Stanford/lib/dbase,/import/mellotron/1/rvg/Stanford/lib/biblio/glabbeek,/import/mellotron/1/rvg/Stanford/lib/new}
\begin{thebibliography}{10}
\bibitem{ABV94}
{\sc L.~Aceto, B.~Bloom \& F.W. Vaandrager} (1994):
\newblock {\em Turning {SOS} rules into equations.}
\newblock {\sl Information and Computation} 111(1), pp. 1--52.
\bibitem{Bas96}
{\sc T.~Basten} (1996):
\newblock {\em Branching bisimulation is an equivalence indeed!}
\newblock {\sl Information Processing Letters} 58(3), pp. 141--147.
\bibitem{BK85}
{\sc J.A. Bergstra \& J.W. Klop} (1985):
\newblock {\em Algebra of communicating processes with abstraction.}
\newblock {\sl Theoretical Computer Science} 37(1), pp. 77--121.
\bibitem{Bl95}
{\sc B.~Bloom} (1995):
\newblock {\em Structural operational semantics for weak bisimulations.}
\newblock {\sl Theoretical Computer Science} 146, pp. 25--68.
\bibitem{BIM95}
{\sc B.~Bloom, S.~Istrail \& A.R. Meyer} (1995):
\newblock {\em Bisimulation can't be traced.}
\newblock {\sl Journal of the ACM} 42(1), pp. 232--268.
\bibitem{Fok00b}
{\sc W.J. Fokkink} (2000):
\newblock {\em Rooted branching bisimulation as a congruence.}
\newblock {\sl Journal of Computer and System Sciences} 60(1), pp. 13--37.
\bibitem{GW96}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1996):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock {\sl Journal of the ACM} 43(3), pp. 555--600.
\bibitem{Mi90ccs}
{\sc R.~Milner} (1990):
\newblock {\em Operational and algebraic semantics of concurrent processes.}
\newblock In J.~van Leeuwen, editor: {\sl Handbook of Theoretical Computer Science}, chapter~19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201--1242.
\newblock Alternatively see{ \em Communication and Concurrency},
Prentice-Hall International, Englewood Cliffs, 1989, or {\em A Calculus of Communicating Systems}, LNCS 92, Springer-Verlag, 1980.
\bibitem{Mo90a}
{\sc F.~Moller} (1990):
\newblock {\em The nonexistence of finite axiomatisations for {CCS} congruences.}
\newblock In {\sl Proceedings $5^{th}$ Annual Symposium on Logic in Computer Science, {\rm Philadelphia, USA}}, IEEE Computer Society Press, pp. 142--153.
\bibitem{Pl04}
{\sc G.D. Plotkin} (2004):
\newblock {\em A structural approach to operational semantics.}
\newblock {\sl The Journal of Logic and Algebraic Programming} 60--61, pp. 17--139.
\newblock First appeared in 1981.
\bibitem{dS85}
{\sc R.~de Simone} (1985):
\newblock {\em Higher-level synchronising devices in {{\sc Meije}-SCCS}.}
\newblock {\sl Theoretical Computer Science} 37, pp. 245--267.
\bibitem{Ul92}
{\sc I.~Ulidowski} (1992):
\newblock {\em Equivalences on observable processes.}
\newblock In {\sl Proceedings $7^{th}$ Annual Symposium on Logic in Computer Science, {\rm Santa Cruz, California}}, IEEE Computer Society Press, pp. 148--159.
\bibitem{UP02}
{\sc I.~Ulidowski \& I.~Phillips} (2002):
\newblock {\em Ordered SOS rules and process languages for branching and eager bisimulations.}
\newblock {\sl Information \& Computation} 178, pp. 180--213.
\bibitem{UY00}
{\sc I.~Ulidowski \& S.~Yuen} (2000):
\newblock {\em Process languages for rooted eager bisimulation.}
\newblock In C.~Palamidessi, editor: {\sl {\rm Proceedings of the 11th International Conference on} Concurrency Theory{\rm, CONCUR 2000}}, {\sl \rm LNCS} 1877, Springer, pp. 275--289.
\end{thebibliography}
\end{document}