\documentclass{entcs}
\usepackage{entcsmacro}
\newfont{\fsc}{eusm10 scaled 1200}
\usepackage{amsmath} % \boldsymbol
\usepackage{dsfont}

\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}} % no vertical space
\newcommand{\diam}[1]{\langle#1\rangle}
\newcommand{\eps}{\langle\epsilon\rangle}
\newcommand{\trans}[1]{\stackrel{#1}{\longrightarrow}}
\newcommand{\ntrans}[1]{\mathrel{\hspace{.4em}\not\hspace{-.4em}\trans{#1\;}}}
\newcommand{\epsarrow}{\stackrel{\epsilon}{\Longrightarrow}}
\newcommand{\bis}[1]{\; \raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{#1}\,}
\newcommand{\var}{{\it var}}
\newcommand{\ar}{{\it ar}}
\newcommand{\IO}[1]{\mathds{O}_{#1}}
\renewcommand{\phi}{\varphi}


\def\lastname{Fokkink, van Glabbeek and de Wind}

\begin{document}
\begin{frontmatter}
\title{Divide and Congruence\\ Applied to $\eta$-Bisimulation}
\author{Wan Fokkink\thanksref{myemail}}
\address{Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam\\
CWI, Department of Software Engineering, Amsterdam}
\author{Rob van Glabbeek\thanksref{cocoemail}}
\address{National ICT Australia, Sydney\\
Univ.\ of New South Wales, School of Computer Science and Engineering, Sydney}
\author{Paulien de Wind\thanksref{coemail}}
\address{Vrije Universiteit Amsterdam, Department of Computer Science, Amsterdam}
\thanks[myemail]{Email: \href{mailto:wanf@cs.vu.nl}
{\texttt{\normalshape wanf@cs.vu.nl}}}
\thanks[cocoemail]{Email: \href{mailto:rvg@cs.stanford.edu}
{\texttt{\normalshape rvg@cs.stanford.edu}}}
\thanks[coemail]{Email: \href{mailto:pdwind@cs.vu.nl}
{\texttt{\normalshape pdwind@cs.vu.nl}}}

\begin{abstract}
We present congruence formats for $\eta$- and rooted $\eta$-bisimulation equivalence. These formats are derived using a method for decomposing modal formulas in process algebra. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra.
\end{abstract}
\begin{keyword}
Structural operational semantics;  modal logic; decomposition; congruence; $\eta$-bisimulation
\end{keyword}
\end{frontmatter}

\section{Introduction}\label{sec:introduction}

Structural operational semantics \cite{Plo04} provides process algebras and specification languages with an interpretation. It generates a labelled transition system, in which states are the closed terms over a (single-sorted, first-order) signature, and transitions between states may be supplied with labels. The transitions between states are obtained from a transition system specification, which consists of a set of proof rules called transition rules.

Labelled transition systems can be distinguished from each other by a wide range of semantic equivalences, based on e.g.\ branching structure or decorated versions of execution sequences. {\sc Van Glabbeek} \cite{vGl93} classified equivalences for processes that take into account the internal action $\tau$. Here we focus on one such equivalence, called $\eta$-bisimulation \cite{BavGl87}.

In general a semantic equivalence induced by a transition system specification is not a congruence, i.e.\ the equivalence class of a term $f(p_1,\ldots,p_n)$ need not be determined by the equivalence classes of its arguments $p_1,\ldots,p_n$. Being a congruence is an important property, for instance in order to fit the equivalence into an axiomatic framework. Syntactic formats for transition rules have been developed with respect to several semantic equivalences, to ensure that such an equivalence is a congruence. These formats help to avoid repetitive congruence proofs. Several congruence formats were introduced for bisimulation, such as the De Simone format \cite{Sim85}, the GSOS format \cite{BIM95}, the tyft/tyxt format \cite{GV92}, and the ntyft/ntyxt format \cite{Gro93}. {\sc Bloom} \cite{Blo95} introduced congruence formats for weak and branching bisimulation and for rooted weak and branching bisimulation. These formats include so-called patience rules for arguments $i$ of function symbols $f$, which imply that a term $f(p_1,\ldots,p_n)$ inherits the $\tau$-transitions of its argument $p_i$. Furthermore, arguments of function symbols that contain running processes are marked, and this marking is used to restrict occurrences of variables in transition rules. Recently, {\sc van Glabbeek} \cite{vGl05} significantly simplified the formats from \cite{Blo95}, and presented similar formats for delay and $\eta$-bisimulation and for rooted delay and $\eta$-bisimulation.

{\sc Van Glabbeek} \cite{vGl01,vGl93} gave characterisations of equivalences in terms of the observations that an experimenter could make during a session with a process. Modal logic captures such observations. A modal characterisation of an equivalence consists of a class $C$ of modal formulas such that two processes are equivalent if and only if they make true the same formulas in $C$. For instance, Hennessy-Milner logic \cite{HM85} is the modal characterisation of bisimulation.

{\sc Larsen and Xinxin} \cite{LX91} introduced a method for decomposing formulas from Hennessy-Milner logic for concrete processes, with respect to terms from a process algebra with a structural operational semantics in De Simone format. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy certain other formulas, obtained by decomposing the original formula. This method was extended by {\sc Bloom, Fokkink \& van Glabbeek} \cite{BFvG04} to ntyft/ntyxt format without lookahead, and by {\sc Fokkink, van Glabbeek \& de Wind} to tyft/tyxt format in the full version of \cite{FvGdW03}. In \cite{BFvG04}, the decomposition method was applied to obtain congruence formats for behavioural equivalences from \cite{vGl01}. The idea is that given an equivalence and its modal characterisation $C$, the congruence format for this equivalence must ensure that decomposing a formula in $C$ always produces formulas in $C$.

In an unpublished manuscript, we extend the work of \cite{BFvG04} to processes with $\tau$-transitions. We present a method for decomposing formulas from modal logic for processes with $\tau$-transitions, and use this decomposition method to obtain congruence formats for branching and rooted branching bisimulation.

In the current paper, we use this decomposition method to obtain congruence formats for $\eta$- and rooted $\eta$-bisimulation. Thus we drive home the point that, in contrast to the ad hoc construction of congruence formats from the past, we can now systematically derive expressive congruence formats from the modal characterisations of semantic equivalences. Our formats use two predicates on arguments of function symbols, to mark both running processes and processes that may have started running.


\section{Preliminaries}

\subsection{Equivalences on labelled transition systems}\label{sec:equivalences_terms}

A \emph{labelled transition system (LTS)} is a pair $(\mathds{P},\rightarrow)$ with $\mathds{P}$ a set of \emph{processes} and $\rightarrow\;\subseteq\mathds{P}\times(A\cup\{\tau\})\times\mathds{P}$ where $\tau$ is an \emph{internal action} and $A$ a set of \emph{actions} not containing $\tau$.
We use $\alpha,\beta,\gamma$ for elements of $A\cup\{\tau\}$ and $a,b$ for elements of $A$. We write $p\trans\alpha q$ for $(p,\alpha,q)\in\;\rightarrow$ and $p\ntrans\alpha$ for $\neg\exists q\in\mathds{P}:p\trans\alpha q$, and $\epsarrow$ for the transitive-reflexive closure of $\trans{\tau}$.

\begin{definition}{\bf \cite{BavGl87}}\label{def:eta}
A symmetric relation $B\subseteq\mathds{P}\times\mathds{P}$ is an \emph{$\eta$-bisimulation} if $pBq$ and $p\trans{\alpha}p'$ implies that either $\alpha = \tau$ and $p'\,B\,q$, or $q\epsarrow q' \trans{\alpha} q'' \epsarrow q'''$ for some $q',q'',q'''$ with $pBq'$ and $p'Bq'''$.
Processes $p,q$ are {\em $\eta$-bisimilar}, denoted by $p\bis{\eta}q$, if there exists an $\eta$-bisimulation $B$ with $pBq$.
\end{definition}
$\eta$-bisimulation is not a congruence with respect to most process algebras from the literature, meaning that the equivalence class of a term $f(p_1,\ldots,p_n)$ is not always determined by the equivalence classes of its arguments $p_1,\ldots,p_n$. A rootedness condition remedies this imperfection.

\begin{definition}{\bf \cite{BavGl87}}
A symmetric relation $R\subseteq\mathds{P}\times\mathds{P}$ is a \emph{rooted $\eta$-bisimulation} if $pRq$ and $p \trans{\alpha} p'$ implies that $q \trans{\alpha} q' \epsarrow q''$ for some $q',q''$ with $p'\bis{\eta}q''$.
Processes $p,q$ are \emph{rooted $\eta$-bisimilar}, denoted by $p\bis{r\eta}q$, if there exists a rooted $\eta$-bisimulation $R$ with $pRq$.
\end{definition}


\subsection{Modal logic}\label{sec:modal}

Modal logic aims to formulate properties of processes in an LTS. Following \cite{vGl93}, we extend Hennessy-Milner logic \cite{HM85} with the modal connective $\eps$.

\begin{definition}\label{def:formulas}
The class $\mathds{O}$ of \emph{modal formulas} is defined as follows, where $I$ ranges over all index sets: \vspace{-1mm}
\[
\mathds{O} \qquad \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \diam{\alpha}\phi ~|~ \eps\phi
\vspace{-1mm}
\]
\end{definition}
\noindent
$p\models\phi$ denotes that $p$ satisfies $\phi$. By definition, $p\models\diam{\alpha}\phi$ if $p\trans{\alpha}p'$ with $p'\models\phi$, and $p\models\eps\phi$ if $p\epsarrow p'$ with $p'\models\phi$. We use abbreviations $\top$ for the empty conjunction, $\phi_1\wedge\phi_2$ for $\bigwedge_{i\in\{1,2\}}\phi_i$, and $\phi\diam{\alpha}\phi'$ for $\phi\land\diam{\alpha}\phi'$. We write $\phi\equiv\phi'$ if $p\models\phi\Leftrightarrow p\models\phi'$ for any process $p$ in any LTS.

\begin{definition}
The subclasses $\IO{\eta}$ and $\IO{r\eta}$ of $\mathds{O}$ are defined as follows: \vspace*{-1mm}
\begin{align*}
&\IO{\eta}       && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \eps\phi ~|~ \eps(\phi\diam{a}\eps\phi) & (a\in A) \vspace{-1mm} \\
&\IO{r\eta}      && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \diam{\alpha}\eps\hat\phi ~|~ \hat\phi & (\hat\phi\in\IO{\eta},\,\alpha\in A\cup\{\tau\}) \vspace{-1mm}
\end{align*}
The classes $\IO{\eta}^\equiv$ and $\IO{r\eta}^\equiv$ are the closures of $\IO{\eta}$, respectively $\IO{r\eta}$, under $\equiv$.
\end{definition}
\noindent
The last clause in the definition of $\IO{r\eta}$ guarantees that
$\IO{\eta} \subseteq \IO{r\eta}$, which we need in the proof of
Prop.~\ref{prop:rooted_eta_preservation}. Also without this clause it
would follow that $\IO{\eta}^\equiv\subseteq\IO{r\eta}^\equiv$, using
structural induction and $\eps\phi\equiv\phi\wedge\diam{\tau}\eps\phi$. 

For $L\subseteq\mathds{O}$, we write $p\sim_L q$ if $p$ and $q$ satisfy the same formulas in $L$.
Note that, trivially, $p\sim_{\IO{\eta}}q \Leftrightarrow
p\sim_{\IO{\eta}^\equiv}q$ and $p\sim_{\IO{r\eta}}q \Leftrightarrow
p\sim_{\IO{r\eta}^\equiv}q$.

\begin{theorem}\label{thm:characterisation}
$p\bis{\eta}q\Leftrightarrow p\sim_{\IO{\eta}}q$ and $p\bis{r\eta}q\Leftrightarrow p\sim_{\IO{r\eta}}q$, for all $p,q\in\mathds{P}$.
\end{theorem}
\noindent
A proof of this theorem is presented in the appendix.

\subsection{Structural operational semantics}\label{sec:sos}

Let $V$ be an infinite set of variables, with typical elements $x,y,z$. A syntactic object is {\em closed} if it does not contain any variables. A \emph{signature} is a set $\Sigma$ of function symbols $f$ with arity $ar(f)$. We always take $|\Sigma|, |A| \leq |V|$. The set $\mathds{T}(\Sigma)$ of terms over $\Sigma$ and $V$ is defined as usual. $t,u$ denote terms and $p,q$ closed terms. $\var(t)$ is the set of variables that occur in $t$. A substitution is a partial function from $V$ to $\mathds{T}(\Sigma)$. A closed substitution $\sigma$ is a total function from $V$ to closed terms.

\begin{definition}\label{def:TSS}
A (\emph{positive} or \emph{negative}) \emph{literal} is an expression $t \trans\alpha t'$ or $t\ntrans\alpha$. A \emph{(transition) rule} is of the form $\frac{H}{t\trans\alpha t'}$ with $H$ a set of literals called the \emph{premises}. $t\trans\alpha t'$ is the \emph{conclusion} and $t$ the \emph{source} of the rule. A rule $\frac{\emptyset}{t\trans\alpha t'}$ is also written $t\trans\alpha t'$. A \emph{transition system specification (TSS)} is a set of transition rules.
\end{definition}

\begin{definition}\label{def:proof}
Let $P=(\Sigma,R)$ be a TSS. An {\em irredundant proof} from $P$ of a rule $\frac{H}{t\trans\alpha t'}$ is a well-founded tree with the nodes labelled by literals and some of the leaves marked ``hypothesis'', such that the root has label $t\trans\alpha t'$, $H$ is the set of labels of the hypotheses, and if $\mu$ is the label of a node that is not a hypothesis and $K$ is the set of labels of the children of this node, then $\mu$ is positive and $\frac{K}{\mu}$ is a substitution instance of a rule in $R$.
\end{definition}
\noindent
The proof of $\frac{H}{t\trans\alpha t'}$ is called irredundant because $H$ must equal (instead of include)
the set of labels of the hypotheses. This irredundancy will be crucial for the preservation of our congruence formats
in Sect.\ \ref{sec:formats} (see Prop.~\ref{prop:preservation_eta_bisimulation_safe}).

A TSS is meant to specify an LTS in which the transitions are closed positive literals. A TSS with only positive premises
specifies an LTS in a straightforward way, but it is not so easy to associate an LTS to a TSS with negative premises.
From \cite{vGl04} we adopt the notion of a well-supported proof of a closed literal.
Literals $t \trans{\alpha} t'$ and $t\ntrans{\alpha}$ are said to \emph{deny} each other.

\begin{definition}\label{def:wsp}
Let $P=(\Sigma,R)$ be a TSS. A \emph{well-supported proof} from $P$ of a closed literal ${\mu}$ is a well-founded tree with the nodes labelled by closed literals, such that the root is labelled by $\mu$, and if $\nu$ is the label of a node and $K$ is the set of labels of the children of this node, then:
\begin{enumerate}
\item either $\nu$ is positive and $\frac{K}{\nu}$ is a closed substitution instance of a rule in $R$;
\item or $\nu$ is negative and for each set $N$ of closed negative literals with $\frac{N}{\kappa}$ irredundantly provable
from $P$ and $\kappa$ a closed positive literal denying $\nu$, a literal in $K$ denies one in $N$.
\end{enumerate}
$P\vdash_{\it ws}\mu$ denotes that a well-supported proof from $P$ of $\mu$ exists.
$P$ is \emph{complete} if for each $p$ and $\alpha$, either $P\vdash_{\it ws}p\ntrans\alpha$ or
$P\vdash_{\it ws}p\trans\alpha p'$ for some $p'$.
\end{definition}
\noindent
A complete TSS specifies an LTS, consisting of the {\it ws}-provable closed positive literals.


\subsection{Notions regarding transition rules}

In this section we present terminology for syntactic restrictions on rules, originating from \cite{BFvG04,Gro93,GV92}.

\begin{definition}\label{def:ntytt}
An \emph{ntytt rule} is a rule in which the right-hand sides of positive premises are variables that are all distinct, and that do not occur in the source. An ntytt rule is an \emph{ntyxt rule} if its source is a variable, an \emph{ntyft rule} if its source contains exactly one function symbol and no multiple occurrences of variables, and an \emph{nxytt rule} if the left-hand sides of its premises are variables. 
\end{definition} 

\begin{definition}\label{def:decent}
A variable in a rule is \emph{free} if it occurs neither in the source nor in right-hand sides of premises. A rule has \emph{lookahead} if some variable occurs in the right-hand side of a premise and in the left-hand side of a premise. A rule is \emph{decent} if it has no lookahead and does not contain free variables.
\end{definition}
\noindent
The ntyft/ntyxt and ready simulation formats \cite{Gro93,BFvG04} were originally introduced
to guarantee congruence for bisimulation and ready simulation.

\begin{definition}\label{def:ready_sim}
A TSS is in \emph{ntyft/ntyxt format} if it consists of ntyft and ntyxt rules,
and in \emph{ready simulation format} if moreover its rules do not have lookahead.
\end{definition}
A predicate $\aleph$ marks arguments of function symbols that contain
running processes (cf.\ \cite{BFvG04}). Typically, in process algebra,
$\aleph$ holds for the arguments of the merge $\|$, but not for the arguments
of alternative composition $+$.

\begin{definition}\label{def:liquid/frozen}
Let $\aleph$ be a unary predicate on $\{(f,i)\mid 1 \leq i \leq ar(f),~f \in \Sigma \}$. If $\aleph(f,i)$, then argument $i$ of $f$ is {\em liquid}; otherwise it is {\em frozen}. An occurrence of $x$ in $t$ is {\em at an $\aleph$-liquid position} if either $t=x$, or $t=f(t_1,\ldots,t_{ar(f)})$ and the occurrence is at an $\aleph$-liquid position in $t_i$ for a liquid argument $i$ of $f$.
\end{definition}
\noindent
A patience rule for an argument $i$ of a function symbol $f$ expresses that term $f(p_1,\ldots,p_n)$ inherits
the $\tau$-transitions of argument $p_i$ (cf.\ \cite{Blo95,Fok00}). We will require the presence of patience rules
for liquid arguments.

\begin{definition}\label{def:patience_rule}
An ntyft rule is a {\em patience rule} for $(f,i)$, with $1\leq i\leq\ar(f)$, if it is of the form
\vspace*{-5mm}
\[
\frac{x_i\trans{\tau}y}{f(x_1,\ldots,x_i,\ldots,x_{\ar(f)})\trans{\tau}
f(x_1,\ldots,x_{i-1},y,x_{i+1}\ldots,x_{\ar(f)})} \vspace*{-1mm}
\]
It is an {\em $\aleph$-patience rule} if $\aleph(f,i)$.
\end{definition}
\noindent
An ntytt rule is {\em patient} with respect to $\aleph$ if it is irredundantly provable from the $\aleph$-patience rules. Such rules have the form $\frac{t\trans\tau y}{C[t]\trans\tau C[y]}$ with $C[]$ an $\aleph$-liquid context, meaning that the context symbol $[]$ occurs at an $\aleph$-liquid position.

\begin{definition}
A TSS is \emph{$\aleph$-patient} if it contains all $\aleph$-patience rules.
It is \emph{abstraction-free} if only patience rules have a conclusion of the form $t\trans{\tau}u$.
\end{definition}

\subsection{Decomposition of modal formulas}

To decompose modal formulas, we use a result from \cite{BFvG04},
where for any TSS $P$ in ready simulation format
a collection of decent nxytt rules, called {\it $P$-ruloids}, is constructed.
We explain this construction on a rather superficial level;
the precise transformation can be found in \cite{BFvG04}.

First $P$ is converted to a TSS in decent ntyft format. In this conversion from \cite{GV92},
free variables in a rule are replaced by closed terms, and if the source is of the form $x$ then this variable
is replaced by a term $f(x_1,\ldots,x_n)$ for each $f\in\Sigma$. Next, using a construction from \cite{FvG96}, left-hand sides
of positive premises are reduced to variables. Roughly the idea is, given a premise $f(t_1,\ldots,t_n)\trans{\alpha}y$ in
a rule $r$, and a rule $\frac{H}{f(x_1,\ldots,x_n)\trans{\alpha}t}$, to transform $r$ by replacing the
aforementioned premise by $H$, $y$ by $t$, and the $x_i$ by the $t_i$; this is repeated (transfinitely) until all
positive premises with a non-variable left-hand side have disappeared. In the final transformation step,
rules with a {\it negative} conclusion $t\ntrans\alpha$ are introduced.
The motivation is that instead of the notion of well-founded provability in Def.\ \ref{def:wsp}, we want
a more constructive notion like Def.\ \ref{def:proof}, by making it possible that a negative premise is matched
with a negative conclusion. A rule $r$ with a conclusion $f(x_1,\ldots,x_n)\ntrans{\alpha}$ is obtained by picking
one premise from each rule with a conclusion $f(x_1,\ldots,x_n)\trans{\alpha}t$, and including the denial of
each of the selected premises as a premise of $r$. For this last transformation it is essential that rules
do not have lookahead.

The resulting TSS, which is in decent ntyft format, is denoted by $P^+$.
In \cite{BFvG04} it is established that $P^+\vdash\mu\Leftrightarrow P\vdash_{\it ws}\mu$ for all closed literals $\mu$.
The notion of irredundant provability is adapted in a straightforward
fashion to accommodate rules with a negative conclusion. $P$-ruloids are the decent nxytt rules that
are irredundantly provable from $P^+$. The following correspondence result from \cite{BFvG04} between
a TSS and its ruloids plays a crucial role in the decomposition method employed here.
It says that there is a well-supported proof from $P$ of a transition $p \trans{a}q$,
with $p$ a closed substitution instance of a term $t$, if and only if there
is a proof of this transition that uses at the root a $P$-ruloid with source $t$.

\begin{proposition}\label{prop:ruloid}
Let $P$ be a TSS in ready simulation format. Then $P\vdash_{\it ws}\sigma(t)\trans\alpha p$
if and only if there are a $P$-ruloid $\frac{H}{t\trans\alpha u}$
and a $\sigma'$ with $P\vdash_{\it ws}\sigma'(\mu)$ for $\mu\in H$, $\sigma'(t)=\sigma(t)$
and $\sigma'(u)=p$.
\end{proposition}
We now show how one can decompose formulas from $\mathds{O}$.
To each term $t$ and formula $\phi$ we assign a set $t^{-1}(\phi)$ of {\em decomposition mappings}
$\psi:V\rightarrow\mathds{O}$. Each of these mappings $\psi\in t^{-1}(\phi)$ guarantees that
$\sigma(t)\models\phi$ if $\sigma(x)\models\psi(x)$ for $x\in\var(t)$. Vice versa, whenever
$\sigma(t)\models\phi$, there is a decomposition mapping $\psi \in t^{-1}(\phi)$ with
$\sigma(x)\models\psi(x)$ for $x \in \var(t)$. This is formalised in Thm.~\ref{thm:decomposition}.

\begin{definition}\label{def:decomposition}
Let $P$ be an $\aleph$-patient, abstraction-free TSS in ready simulation format. We define $\cdot^{-1}:\mathds{T}(\Sigma)\times\mathds{O}\rightarrow\mbox{\fsc P}(V\rightarrow\mathds{O})$ as follows. Let $t$ denote a univariate term, i.e.\ without multiple occurrences of the same variable.

\begin{enumerate}
\item\label{item:conj}
$\psi\in t^{-1}(\bigwedge_{i\in I}\phi_i)$ iff for $x\in V$
\vspace*{-3mm}
\[
\psi(x)= \displaystyle{\bigwedge_{i\in I}\psi_i(x)}\vspace*{-5mm}
\]
where $\psi_i\in t^{-1}(\phi_i)$ for $i\in I$. \vspace*{1mm}
\item
$\psi\in t^{-1}(\diam\alpha\phi)$ iff there is a $P$-ruloid $\frac{H}{t\trans{\alpha}u}$
and a $\chi\in u^{-1}(\phi)$ with
\[
\psi(x)=\left\{
  \begin{array}{ll}
  \displaystyle{\chi(x)\ \land\ \bigwedge_{x\trans{\beta}y\in H}\!\!\!\!\!\diam{\beta}\chi(y)
                \ \land\  \bigwedge_{x\ntrans{\gamma}\in H}\!\!\!\!\!\neg\diam{\gamma}\top} & \mbox{if $x\in\var(t)$}\\
  \top & \mbox{if $x\not\in\var(t)$}
  \end{array}
\right.
\]

\item
$\psi\in t^{-1}(\neg\phi)$ iff there is a function $h:t^{-1}(\phi)\rightarrow\var(t)$ with
\[
\psi(x)= \displaystyle{\bigwedge_{\chi\in h^{-1}(x)}\!\!\!\neg\chi(x)}\qquad\text{ for }x\in V
\]

\item
$\psi\in t^{-1}(\eps\phi)$ iff there is a $\chi\in t^{-1}(\phi)$ with \vspace{-1mm}
\[
\psi(x)=\left\{
\begin{array}{ll}
\eps\chi(x) & \textrm{if $x$ occurs $\aleph$-liquid in $t$}\\
\chi(x) & \textrm{otherwise}\\
\end{array}
\right.
\]

\item
$\psi\in\rho(t)^{-1}(\phi)$ for $\rho:\var(t)\rightarrow V$ not injective
iff there is a $\chi\in t^{-1}(\phi)$ with \vspace{-1mm}
\[
\psi(x)=\bigwedge_{y\in\rho^{-1}(x)}\chi(y)\qquad\text{ for }x\in V
\]

\end{enumerate}
\end{definition}
\noindent
It is not hard to see that if $\psi\in t^{-1}(\phi)$, then $\psi(x)\equiv\top$ for $x\not\in\var(t)$.

To explain the idea behind Def.~\ref{def:decomposition}, we expand on two of its cases.
Consider $t^{-1}(\diam{\alpha}\phi)$, and let $\sigma$ be any closed substitution. The question is
under which conditions $\psi(x)\in\mathds{O}$ on $\sigma(x)$, for $x\in\var(t)$, there is a transition
$\sigma(t)\trans{\alpha}q$ with $q\models\phi$. According to Prop.~\ref{prop:ruloid}, there is such a transition
if and only if there is a closed substitution $\sigma'$ with $\sigma'(t)=\sigma(t)$ and a $P$-ruloid $\frac{H}{t\trans\alpha u}$ such that
(1) the premises in $\sigma'(H)$ are satisfied and (2) $\sigma'(u)\models\phi$. The first condition
is covered if for $x\in\var(t)$, $\psi(x)$ contains conjuncts
$\diam{\beta}\top$ for $x\trans{\beta}y\in H$ and conjuncts $\neg\diam{\gamma}\top$
for $x\ntrans{\gamma}\;\in H$. By adding a conjunct $\chi(x)$, and replacing each
conjunct $\diam{\beta}\top$ by $\diam{\beta}\chi(y)$, for some
$\chi\in u^{-1}(\phi)$, the second condition is covered as well.

Consider $t^{-1}(\neg\phi)$, and let $\sigma$ be any closed substitution.
We have $\sigma(t)\not\models\phi$ if and only if there is no $\chi\in t^{-1}(\phi)$
such that $\sigma(x)\models\chi(x)$ for all $x\in\var(t)$.
In other words, for each $\chi\in t^{-1}(\phi)$, $\psi(x)$
must contain a conjunct $\neg\chi(x)$, for some $x\in\var(t)$.

The following theorem, whose proof is omitted here, will be the key to
the forthcoming congruence results.

\begin{theorem}\label{thm:decomposition}
Given a complete TSS in ready simulation format that contains the $\aleph$-patience rules for some $\aleph$. For any term $t$, closed substitution $\sigma$ and $\phi\in\mathds{O}$: \vspace{-1mm}
\[
\sigma(t)\models\phi\ \Leftrightarrow
\ \exists\psi\in t^{-1}(\phi)\ \forall x\in \var(t):\sigma(x)\models\psi(x)
\]
\end{theorem}


\section[Eta-Bisimulation as a Congruence]{$\eta$-Bisimulation as a Congruence}

We proceed to apply the decomposition method from the previous section to derive congruence formats
for $\eta$- and rooted $\eta$-bisimulation equivalence. The idea is that the $\eta$-bisimulation
format must guarantee that a formula from $\IO{\eta}$ is always decomposed into formulas from $\IO{\eta}^\equiv$
(see Prop.~\ref{prop:retab-retab}).
Likewise, the rooted $\eta$-bisimulation format must guarantee that a formula from $\IO{r\eta}$ is always
decomposed into formulas from $\IO{r\eta}^\equiv$ (see Prop.~\ref{prop:rooted_eta_preservation}).
This implies the desired congruence results (see Thm.~\ref{thm:congruence1} and Thm.~\ref{thm:congruence2}).

In order minimise the complexity inherent in the combination of modal
decomposition and abstraction, we apply the decomposition method
to abstrac\-tion-free TSSs, and extend our results to the general case
using the well-known compositionality of the abstraction operator.

\subsection{Congruence formats}\label{sec:formats}

We assume a second predicate $\Lambda$ on arguments of function symbols, to
denote that the processes they contain may have started running (but may
currently be resting). Always $\aleph\subseteq\Lambda$.
Typically, in process algebra, $\aleph$ holds for the first argument of sequential
composition while only $\Lambda$ holds for the second argument, and $\Lambda$ does
not hold for the arguments of alternative composition.

\begin{definition}\label{def:rooted_eta_bisimulation_safe}
Let $\aleph\subseteq\Lambda$. An ntytt rule $\frac{H}{t\trans\alpha u}$ is {\em rooted $\eta$-bisimulation safe}
with respect to $\aleph$ and $\Lambda$ if:
\begin{enumerate}
\item
it has no lookahead,
\item
right-hand sides of premises occur only at $\aleph$-liquid positions in $u$, and
\item
if $x$ occurs exactly once\footnote{Only the requirements for rules in
 which $t$ is univariate matter. The current formulation of
    Def.~\ref{def:rooted_eta_bisimulation_safe} for general terms $t$ paves
    the way for Prop.~\ref{prop:preservation_eta_bisimulation_safe}.}
 in $t$, at a $\Lambda$-liquid position, then:
\begin{enumerate}
\item all occurrences of $x$ in the rule are at $\Lambda$-liquid positions,
\item $x$ has no $\aleph$-liquid occurrences in left-hand sides of
  negative premises,
\item $x$ has at most one $\aleph$-liquid occurrence in the left-hand
      side of one positive premise, and this premise has a label from $A$, and
\item if $x$ occurs at an $\aleph$-frozen position in $t$, then $x$
      does not occur at $\aleph$-liquid positions in left-hand sides
      of premises.
\end{enumerate}
\end{enumerate}
In case $\Lambda$ is the universal predicate, we say that the rule is {\em $\eta$-bisimulation safe} with respect to $\aleph$.
\end{definition}

\begin{definition}\label{def:eta_bisimulation_format}
A TSS in ready simulation format is in {\em rooted $\eta$-bisimulation format}
if, for some $\aleph\subseteq\Lambda$, it consists of the $\aleph$-patience rules and
rules that are rooted $\eta$-bisimulation safe with respect to $\aleph$ and $\Lambda$.

A TSS in ready simulation format is in {\em $\eta$-bisimulation format}
if, for some $\aleph$, it consists of the $\aleph$-patience rules and
rules that are $\eta$-bisimulation safe with respect to $\aleph$.
\end{definition}
\noindent
The operators \emph{initial priority} (with frozen argument),
\emph{binary Kleene star} (with both arguments frozen) and
\emph{action refinement} (with only the second argument frozen)
of~\cite{BFvG04} fit the rooted $\eta$-bisimulation format.  In these
applications, as well as for capturing the operators of CCS and
similar languages, it suffices to take $\Lambda = \aleph$.  In the
following example this is not possible.

\begin{example}
Let $f$ be a binary operator that interleaves actions $\alpha\in A\cup\{\tau\}$
 from its arguments, until its first arguments produces an action
 $crash$. Then $f$ performs the actions $alert$ and $prevent~ meltdown$,
 without any $\tau$-steps in between, and subsequently continues as
 its second argument.\vspace{-1ex}
{\small$$\begin{array}{@{}c@{~~~~}c@{~~~~}c@{~~~~}c@{}}
  \displaystyle\frac{x\trans{\alpha}x'}{f(x,y)\trans{\alpha}f(x',y)}&
  \displaystyle\frac{y\trans{\alpha}y'}{f(x,y)\trans{\alpha}f(x,y')}&
  \displaystyle\frac{x\trans{crash}x'}{f(x,y)\trans{alert} pm.y}&
  pm.y \stackrel{prevent}{\raisebox{0pt}[11pt]{$\stackrel{meltdown}{\raisebox{0pt}[4pt]{$-\!\!\!-\!\!\!-\!\!\!-\!\!\!\longrightarrow$}}$}} y
\end{array}$$}%
  $pm$ is a CCS action-prefixing operator. For this TSS to
  be in (rooted) $\eta$-bisimulation format it is essential that the
  argument of $pm$ is marked as $\aleph$-frozen (and hence not
  accompanied by a patience rule) but $\Lambda$-liquid, for it harbours
  a process that has already started but is not currently running.
\end{example}
\noindent
In the definition of modal decomposition, we did not use the rules
from the original TSS $P$, but the $P$-ruloids. Therefore we must
verify that if $P$ is in (rooted) $\eta$-bisimulation format, then so
are the $P$-ruloids.

\begin{proposition}
\label{prop:preservation_eta_bisimulation_safe}
If a TSS $P$ is in (rooted) $\eta$-bisimulation format with respect
to some $\aleph$, then each $P$-ruloid is either patient or
(rooted) $\eta$-bisimulation safe with respect to $\aleph$.
\end{proposition}
\noindent
The proof of Prop.~\ref{prop:preservation_eta_bisimulation_safe} is omitted here.
The key part of the proof is to show that the decent (rooted) $\eta$-bisimulation format is preserved under
irredundant provability.
(The adjective irredundant is essential here.)

\subsection{Preservation of modal characterisations}\label{sec:eta}

From now on we will mention patient and (rooted) branching safe rules without reference to the accompanying predicates $\aleph$ and $\Lambda$.

\begin{lemma}\label{patience}
Given a TSS in ready simulation format. For any term $t$, $\phi\in\mathds{O}$ and variable $x$ that occurs only $\aleph$-liquid in $t$, $\psi\in t^{-1}(\eps\phi)\Rightarrow \psi(x)\equiv\eps\psi(x)$.
\end{lemma}
\begin{proof}
Let $\psi\in t^{-1}(\eps\phi)$ and $x$ occur only $\aleph$-liquid in $t$. Then by Def.~\ref{def:decomposition}.iv  and \ref{def:decomposition}.v, $\psi(x)$ is of the form $\bigwedge_{i\in I}\eps\phi_i$. So $\psi(x)\equiv\eps\psi(x)$.
\end{proof}

\begin{proposition}\label{prop:retab-retab}
Let $P$ be an abstraction-free TSS in rooted $\eta$-bisimulation format. For any term $t$ and variable $x$ that occurs only $\Lambda$-liquid in $t$:
\[
\phi\in\IO{\eta}\ \Rightarrow\ \forall\psi\in t^{-1}(\phi):\psi(x)\in\IO{\eta}^\equiv
\]
\end{proposition}

\begin{proof}
We apply structural induction on $\phi$.
Let $\phi\in\IO{\eta}$. Let $t\in\mathds{T}(\Sigma)$ and $\psi\in t^{-1}(\phi)$, and let $x$ occur only $\Lambda$-liquid in $t$. First we treat the case where $t$ is univariate. If $x\not\in\var(t)$, then $\psi(x)=\top\in\IO{\eta}^\equiv$. Suppose $x$ occurs once in $t$.

\begin{itemize}
\item $\phi=\bigwedge_{i\in I}\phi_i$ with $\phi_i\in\IO{\eta}$ for $i\in I$. By Def.~\ref{def:decomposition}.i, $\psi(x)=\bigwedge_{i\in I}\psi_i(x)$ with $\psi_i\in t^{-1}(\phi_i)$ for $i\in I$. By induction, $\psi_i(x)\in\IO{\eta}^\equiv$ for $i\in I$, so $\psi(x)\in\IO{\eta}^\equiv$.

\item $\phi=\neg\phi'$ with $\phi'\in\IO{\eta}$. By Def.~\ref{def:decomposition}.iii, there is a function $h:t^{-1}(\phi')\rightarrow \var(t)$ such that $\psi(x)=\bigwedge_{\chi\in h^{-1}(x)}\neg\chi(x)$. By induction, $\chi(x)\in\IO{\eta}^\equiv$ for $\chi\in h^{-1}(x)$, so $\psi(x)\in\IO{\eta}^\equiv$.

\item $\phi=\eps\phi'$ with $\phi'\in\IO{\eta}$. By Def.~\ref{def:decomposition}.iv, either $\psi(x)=\eps\chi(x)$ or $\psi(x)=\chi(x)$ for some $\chi\in t^{-1}(\phi')$. By induction on formula size, $\chi(x)\in\IO{\eta}^\equiv$. So $\psi(x)\in\IO{\eta}^\equiv$.

\item $\phi=\eps(\phi_1\diam{a}\eps\phi_2)$ with $\phi_1,\phi_2\in\IO{\eta}$. By Def.~\ref{def:decomposition}.iv, either $\psi(x)=\eps\chi(x)$ or $\psi(x)=\chi(x)$ for some $\chi\in t^{-1}(\phi_1\diam{a}\eps\phi_2)$. By Def.~\ref{def:decomposition}.i, $\chi(x)=\chi_1(x)\land\chi_2(x)$ with $\chi_1\in t^{-1}(\phi_1)$ and $\chi_2\in t^{-1}(\diam{a}\eps\phi_2)$. By induction on formula size, $\chi_1(x)\in\IO{\eta}^\equiv$. By Def.~\ref{def:decomposition}.ii,
\[
\chi_2(x)=\xi(x)\land
\bigwedge_{x\trans{\beta}y\in H}\diam{\beta}\xi(y) \land
\bigwedge_{x\ntrans{\gamma}\in H}\neg\diam{\gamma}\top
\]
for some $\xi\in u^{-1}(\eps\phi_2)$ and some $P$-ruloid $\frac{H}{t\trans{a}u}$. Since $a\not=\tau$, by Prop.~\ref{prop:preservation_eta_bisimulation_safe}, $\frac{H}{t\trans{a}u}$ is rooted $\eta$-bisimulation safe. Since the occurrence of $x$ in $t$ is $\Lambda$-liquid, $x$ occurs only $\Lambda$-liquid in $u$. Moreover, variables in right-hand sides of premises in $H$ occur only $\aleph$-liquid (hence $\Lambda$-liquid) in $u$. So in the previous case we proved that $\xi(x)\in\IO{\eta}^\equiv$ and $\xi(y)\in\IO{\eta}^\equiv$ for \plat{$x\trans{\beta}y\in H$}. We distinguish two cases.

\begin{description}
\item[{\sc Case 1:}]
The occurrence of $x$ in $t$ is $\aleph$-liquid. Then $\psi(x)=\eps\chi(x)$. Since $\frac{H}{t\trans{a}u}$ is rooted $\eta$-bisimulation safe and an nxytt rule, $x$ does not occur in left-hand sides of negative premises in $H$, and at most once in the left-hand side of one positive premise in $H$, which is of the form \plat{$x\trans{b}y$} with $b\in A$. The right-hand side, $y$, of such a premise, occurs only $\aleph$-liquid in $u$, so by Lem.\ \ref{patience}, $\xi(y)\equiv\eps\xi(y)$. Hence, either $\chi_2(x)=\xi(x)$ or $\chi_2(x)=\xi(x)\diam{b}\xi(y)\equiv\xi(x)\diam{b}\eps\xi(y)$. Since $\psi(x)=\eps(\chi_1(x)\land\chi_2(x))$, either $\psi(x)=\eps(\chi_1(x)\land\xi(x))\in\IO{\eta}^\equiv$ or $\psi(x)\equiv\eps(\chi_1(x)\land\xi(x)\diam{b}\eps\xi(y))\in\IO{\eta}^\equiv$.

\item[{\sc Case 2:}]
The occurrence of $x$ in $t$ is $\aleph$-frozen. Then $\psi(x)=\chi(x)$. Since $\frac{H}{t\trans{a}u}$ is rooted $\eta$-bisimulation safe and an nxytt rule, $x$ does not occur in left-hand sides of premises in $H$. So $\chi_2(x)=\xi(x)$, and thus $\psi(x)=\chi_1(x)\wedge\chi_2(x)=\chi_1(x)\wedge\xi(x)\in\IO{\eta}^\equiv$.
\end{description}
\end{itemize}
Finally, suppose $t$ is not univariate. Then $t=\rho(u)$ for some univariate term $u$ and $\rho:\var(u)\rightarrow V$ not injective. By Def.~\ref{def:decomposition}.v, $\psi(x)=\bigwedge_{y\in\rho^{-1}(x)}\chi(y)$ for some $\chi\in u^{-1}(\phi)$. Since $u$ is univariate, and for each $y\in\rho^{-1}(x)$ the occurrence in $u$ is $\Lambda$-liquid, $\chi(y)\in\IO{\eta}^\equiv$ for $y\in\rho^{-1}(x)$. Hence, $\psi(x)\in\IO{\eta}^\equiv$.
\end{proof}

\begin{proposition}\label{prop:rooted_eta_preservation}
Let $P$ be an abstraction-free TSS in rooted $\eta$-bisimulation format. For any term $t$ and variable $x$:
\[
\phi\in\IO{r\eta}\ \Rightarrow\ \forall\psi\in t^{-1}(\phi):\psi(x)\in\IO{r\eta}^\equiv
\]
\end{proposition}

\begin{trivlist} \item[\hspace{\labelsep}\bf Proof.]
We apply structural induction on $\phi$.  Let $\phi\in\IO{r\eta}$,
$t\in\mathds{T}(\Sigma)$ and $\psi\in t^{-1}(\phi)$. We restrict
attention to the case where $t$ is univariate; the general case then
follows just as at the end of the proof of Prop.~\ref{prop:retab-retab}. If
$x\not\in\var(t)$, then $\psi(x)=\top\in\IO{r\eta}^\equiv$. So suppose
$x$ occurs once in $t$.

\begin{itemize}
\item
The cases $\phi=\bigwedge_{i\in I}\phi_i$ and $\phi=\neg\phi'$ proceed
as in the proof of Prop.~\ref{prop:retab-retab}.

\item
$\phi=\diam\alpha\eps\phi'$ with $\phi'\in\IO{\eta}$. By Def.~\ref{def:decomposition}.ii,
\[
\psi(x)=\chi(x)\land
\bigwedge_{x\trans\beta y\in H}\diam{\beta}\chi(y)\land
\bigwedge_{x\ntrans\gamma\in H}\neg\diam{\gamma}\top
\]
for some $\chi\in u^{-1}(\eps\phi')$ and some $P$-ruloid
$\frac{H}{t\trans\alpha u}$. By induction, $\chi(x)\in\IO{r\eta}$.
(Induction may be applied because $\eps\phi' \in
\IO{\eta}\subseteq\IO{r\eta}$ and $\eps\phi'$ is a strict subformula
of $\phi$.) By Prop.~\ref{prop:preservation_eta_bisimulation_safe},
$\frac{H}{t\trans\alpha u}$ is either rooted $\eta$-bisimulation safe
or patient. Thus variables in right-hand sides of premises in $H$
occur only $\aleph$-liquid in $u$. By Prop.~\ref{prop:retab-retab},
$\chi(y)\in\IO{\eta}$ for $x\trans{\beta}y\in H$.  Moreover, by
Lemma~\ref{patience}, $\chi(y)\equiv\eps\chi(y)$.  Hence
$\diam{\beta}\chi(y)\equiv\diam\beta\eps\chi(y)\in\IO{r\eta}^\equiv$. Also
$\neg\diam{\gamma}\top\equiv\neg\diam{\gamma}\eps\top\in\IO{r\eta}^\equiv$.
Hence, $\psi(x)\in\IO{r\eta}$.
\item
$\phi\in\IO{\eta}$. If the occurrence of $x$ in $t$ is $\Lambda$-liquid, then $\psi(x)\in\IO{r\eta}^\equiv$ follows from Prop.\ \ref{prop:retab-retab}. So we can assume that this occurrence is $\Lambda$-frozen. The cases $\phi=\bigwedge_{i\in I}\phi_i$ and $\phi=\neg\phi'$ proceed as before. We focus on the other two cases.
\item[$\ast$]
$\phi=\eps\phi'$ with $\phi'\in\IO{\eta} \subseteq \IO{r\eta}$.
Since the occurrence of $x$ in $t$ is $\Lambda$-frozen, by Def.~\ref{def:decomposition}.iv, $\psi(x)=\chi(x)$ for some $\chi\in t^{-1}(\phi')$. By induction on formula size, $\chi(x)\in\IO{r\eta}$. So $\psi(x)\in\IO{r\eta}$.

\item[$\ast$]
$\phi=\eps(\phi_1\diam{a}\eps\phi_2)$  with $\phi_1,\phi_2\in\IO{\eta} \subseteq \IO{r\eta}$.
Since the occurrence of $x$ in $t$ is $\Lambda$-frozen, by
Def.~\ref{def:decomposition}.iv, $\psi(x)=\chi(x)$ for some $\chi\in
t^{-1}(\phi_1\diam{a}\eps\phi_2)$. By Def.~\ref{def:decomposition}.i,
$\chi(x)=\chi_1(x)\land\chi_2(x)$ with $\chi_1\in t^{-1}(\phi_1)$ and
$\chi_2\in t^{-1}(\diam{a}\eps\phi_2)$. By induction on formula size,
$\chi_1(x),\chi_2(x)\in\IO{r\eta}$. Hence, $\psi(x)\in\IO{r\eta}$.\hfill$\Box$
\end{itemize}
\end{trivlist}

\subsection{Congruence results}

Finally we are in a position to prove the promised congruence results.

\begin{lemma}\label{lem:congruence1}
Given a complete abstraction-free TSS in $\eta$-bisimulation format.
If $\sigma(x) \bis{\eta} \sigma'(x)$ for $x \in \var(t)$, then $\sigma(t) \bis{\eta} \sigma'(t)$.
\end{lemma}

\begin{proof}
By Thm.~\ref{thm:characterisation}, $\sigma(x) \bis{\eta} \sigma'(x)$
 implies $\sigma(x) \sim_{\IO{\eta}^\equiv} \sigma'(x)$ for $x \in \var(t)$.
Let $\sigma(t)\models\phi \in \IO{\eta}$. By
 Thm.~\ref{thm:decomposition} there is a $\psi \in t^{-1}(\phi)$ with
 $\sigma(x) \models \psi(x)$ for $x\in\var(t)$. Since $\Lambda$ is
 universal, by Prop.~\ref{prop:retab-retab}, $\psi(x) \in
 \IO{\eta}^\equiv$ for $x\in\var(t)$. Since $\sigma(x)
 \sim_{\IO{\eta}^\equiv} \sigma'(x)$, $\sigma'(x)\models\psi(x)$ for
 $x \in \var(t)$. By Thm.~\ref{thm:decomposition},
 $\sigma'(t)\models\phi$.  Likewise, $\sigma'(t)\models\phi \in \IO{\eta}$ implies $\sigma(t)\models\phi$. So $\sigma(t) \sim_{\IO{\eta}} \sigma'(t)$. Hence, $\sigma(t) \bis{\eta} \sigma'(t)$.
\end{proof}

\begin{theorem}\label{thm:congruence1}
Given a complete TSS $P=(\Sigma,R)$ in $\eta$-bisimulation format.
If $\sigma(x) \bis{\eta} \sigma'(x)$ for $x \in \var(t)$, then $\sigma(t) \bis{\eta} \sigma'(t)$.
\end{theorem}

\begin{proof}
Let $P'$ be obtained from $P$, by changing in all rules expect
$\aleph$-patience rules a conclusion of the form \plat{$t \trans{\tau} u$}
into \plat{$t \trans{i} u$}, for a fresh action $i\not\in A\cup\{\tau\}$.
By construction, $P'$ is abstraction-free and in $\eta$-bisimulation format.
So by Lemma~\ref{lem:congruence1}, $\bis{\eta}$ is a congruence for
all operators of $P'$.

Let $P''$ be obtained from $P'$ by adding a new operator $\tau_i$ with
rules\vspace{-1ex}
$$\frac{x\trans{\alpha}y}{\tau_i(x)\trans{\alpha}\tau_i(y)}~~~(\alpha\neq i)
~~~~~~~~~~~~~~\frac{x\trans{i}y}{\tau_i(x)\trans{\tau}\tau_i(y)}$$
This operator turns all $i$-labels into $\tau$-labels.
It is well-known \cite{BavGl87} and trivial to check that $\bis{\eta}$
is a congruence for $\tau_i$ as well.

If follows trivially that for any operator $f\in\Sigma$ the behaviour
of $\tau_i \circ f$ in $P''$ is the same as the behaviour of $f$ in $P$.
So as $\bis{\eta}$ is a congruence for $\tau_i \circ f$ in $P''$, it
must be a congruence for $f$ in $P$.
\end{proof}

\begin{lemma}\label{lem:congruence2}
Given a complete abstraction-free TSS in rooted $\eta$-bisimulation format.
If $\sigma(x) \bis{r\eta} \sigma'(x)$ for $x \in \var(t)$, then $\sigma(t) \bis{r\eta} \sigma'(t)$.
\end{lemma}

\begin{theorem}\label{thm:congruence2}
Given a complete TSS in rooted $\eta$-bisimulation format.
If $\sigma(x) \bis{r\eta} \sigma'(x)$ for $x \in \var(t)$, then $\sigma(t) \bis{r\eta} \sigma'(t)$.
\end{theorem}
\noindent
The proof of Lemma~\ref{lem:congruence2} is similar to the one of
Lemma~\ref{lem:congruence1}, except that
Prop.~\ref{prop:rooted_eta_preservation} is applied instead of
Prop.~\ref{prop:retab-retab}.  Likewise, the proof of
Thm.~\ref{thm:congruence2} is similar to the one of
Thm.~\ref{thm:congruence1}.

\section{Related work}
The only other formats for $\eta$- and rooted $\eta$-bisimulation that
we are aware of appeared in \cite{vGl05}. Those formats are contained
in the GSOS format \cite{BIM95}.
The formats of \cite{vGl05} distinguish so-called ``principal''
operators and ``abbreviations''. The latter can be regarded as
syntactic sugar, adding nothing that could not be expressed with
principal operators. Our formats are incomparable with the ones of
\cite{vGl05}. However, our formats generalise the result of
simplifying the formats of \cite{vGl05} by requiring all operators to
be principal. 

For the $\eta$-bisimulation format our generalisation
consists in allowing transition rules outside the GSOS format; the
simplified format of \cite{vGl05} is exactly the intersection of our
$\eta$-bisimulation format and the GSOS format. However, the
intersection of our rooted $\eta$-bisimulation format and the GSOS
format is still a proper generalisation of the simplified format for
rooted $\eta$-bisimulation of \cite{vGl05}.
The latter can be described as the intersection of our rooted
$\eta$-bisimulation format and the GSOS format in which all arguments
of all operators that occur in the right-hand sides of conclusions of
transition rules, are required to be $\Lambda$-liquid.

The format of \cite{vGl05} for rooted $\eta$-bisimulation, following
\cite{Blo95}, distinguishes ``tame'' and ``wild'' function symbols. In
terms of our approach, wild operators have only $\Lambda$-frozen
arguments, and tame operators only $\Lambda$-liquid arguments. The idea
to allow operators with both kinds of arguments stems from
\cite{Fok00}.
\vspace{-1ex}


\bibliographystyle{plain}
\begin{thebibliography}{10}
\vspace{-1ex}

\bibitem{BavGl87}
J. Baeten and R. van Glabbeek.
\newblock Another look at abstraction in process algebra.
\newblock In {\em Proc.\ ICALP'87}, LNCS 267, pp.\ 84--94. Springer 1987
\vspace{-1ex}

\bibitem{Blo95}
B.~Bloom.
\newblock Structural operational semantics for weak bisimulations.
\newblock {\em Theoretical Computer Science}, 146(1/2):25--68, 1995.
\vspace{-1ex}

\bibitem{BFvG04}
B.~Bloom, W. Fokkink, and R.~van Glabbeek.
\newblock Precongruence formats for decorated trace semantics.
\newblock {\em ACM Transactions on Computational Logic}, 5(1):26--78, 2004.
\vspace{-1ex}

\bibitem{BIM95}
B.~Bloom, S.~Istrail, and A.~Meyer.
\newblock Bisimulation can't be traced.
\newblock {\em Journal of the ACM}, 42(1):232--268, 1995.
\vspace{-1ex}

\bibitem{Fok00}
W. Fokkink.
\newblock Rooted branching bisimulation as a congruence.
\newblock {\em Journal of Computer and System Sciences}, 60(1):13--37, 2000.
\vspace{-1ex}

\bibitem{FvG96}
W. Fokkink and R.~van Glabbeek.
\newblock Ntyft/ntyxt rules reduce to ntree rules.
\newblock {\em Information and Computation}, 126(1):1--10, 1996.
\vspace{-1ex}

\bibitem{FvGdW03}
W. Fokkink, R.~van Glabbeek, and P.~de Wind.
\newblock Compositionality of {H}ennessy-{M}ilner logic by structural operational semantics.
\newblock Extended abstract appeared in: {\em Proc.\ FCT'03}, LNCS 2751, pp.\ 412--422. Springer, 2003.
\vspace{-1ex}

\bibitem{vGl93}
R.~van Glabbeek.
\newblock The linear time-branching time spectrum {II}: The semantics of
  sequential systems with silent moves.
\newblock In {\em Proc.\ CONCUR'93}, LNCS 715, pp.\ 66--81. Springer, 1993.
\vspace{-1ex}

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

\bibitem{vGl04}
R. van Glabbeek.
\newblock The meaning of negative premises in transition system specifications {II}.
\newblock {\em Journal of Logic and Algebraic Programming}, 60/61:229--258, 2004.
\vspace{-1ex}

\bibitem{vGl05}
R.~van Glabbeek.
\newblock On cool congruence formats for weak bisimulations. \\
\newblock \url{http://theory.stanford.edu/~rvg/abstracts.html#58}.
\vspace{-1ex}

\bibitem{Gro93}
J.F. Groote.
\newblock Transition system specifications with negative premises.
\newblock {\em Theoretical Computer Science}, 118(2):263--299, 1993.
\vspace{-1ex}

\bibitem{GV92}
J.F. Groote and F.~Vaandrager.
\newblock Structured operational semantics and bisimulation as a congruence.
\newblock {\em Information and Computation}, 100(2):202--260, 1992.
\vspace{-1ex}

\bibitem{HM85}
M. Hennessy and R.~Milner.
\newblock Algebraic laws for non-determinism and concurrency.
\newblock {\em Journal of the ACM}, 32(1):137--161, 1985.
\vspace{-1ex}

\bibitem{LX91}
K.G. Larsen and L.~Xinxin.
\newblock Compositionality through an operational semantics of contexts.
\newblock {\em Journal of Logic and Computation}, 1(6):761--795, 1991.
\vspace{-1ex}

\bibitem{Plo04}
G. Plotkin.
\newblock A structural approach to operational semantics.
\newblock {\em Journal of Logic and Algebraic Programming}, 60/61:17--139, 2004.
\newblock Originally appeared in 1981.
\vspace{-1ex}

\bibitem{Sim85}
R.~de Simone.
\newblock Higher-level synchronising devices in \textsc{Meije}--{SCCS}.
\newblock {\em Theoretical Computer Science}, 37(3):245--267, 1985.

\end{thebibliography}

\appendix

\section[Modal Characterisation of Eta-Bisimulation]{Modal Characterisation of $\eta$-Bisimulation}

We prove the first part of Thm.\ \ref{thm:characterisation}, which states
that $\IO{\eta}$ is a modal characterisation of $\eta$-bisimulation equivalence.
We need  to prove, given an LTS $(\mathds{P},\rightarrow)$, that
$p\bis{\eta}q\Leftrightarrow p\sim_{\IO{\eta}}q$ for all $p,q\in\mathds{P}$.

\begin{proof}
($\Rightarrow$) Suppose $p\bis{\eta}q$, and $p\models\phi$ for some $\phi\in\IO{\eta}$. We prove $q\models\phi$, by structural induction on $\phi$. The reverse implication follows by symmetry.
\begin{itemize}
\item
$\phi=\bigwedge_{i\in I}\phi_i$. Then $p\models\phi_i$ for $i\in I$. By induction $q\models\phi_i$ for $i\in I$, so $q\models\bigwedge_{i\in I}\phi_i$.
\item
$\phi=\neg\phi'$. Then $p\not\models\phi'$. By induction $q\not\models\phi'$, so $q\models\neg\phi'$.
\item
$\phi=\eps\phi$. Then for some $n$ there are $p_0,\ldots,p_n\in\mathds{P}$ with $p_n=p$, $p_{i+1}\trans{\tau}p_i$ for $i\in\{0,\ldots,n-1\}$, and $p_0\models\phi$. We apply induction on $n$.
\begin{description}
\item
[$\boldsymbol{n=0}$] $p\models\phi$, so by induction on formula size, $q\models\phi$. Hence $q\models\eps\phi$.
\item
[$\boldsymbol{n>0}$] Since $p_n\trans{\tau}p_{n-1}$, according to Def.~\ref{def:eta} there are two possibilities.
\begin{enumerate}
\item
Either $p_{n-1}\bis{\eta}q$. Since $p_{n-1}\models\eps\phi$, by induction on $n$, $q\models\eps\phi$.
\item
Or $q\epsarrow q'\trans{\tau}q''\epsarrow q'''$ with $p_{n-1}\bis{\eta}q'''$. Since $p_{n-1}\models\eps\phi$, by induction on $n$, $q'''\models\eps\phi$. Hence $q\models\eps\phi$.
\end{enumerate}
\end{description}
\item
$\phi=\eps(\phi_1\diam{a}\eps\phi_2)$. Then for some $n$ there are $p_0,\ldots,p_n\in\mathds{P}$ with $p_n=p$, $p_{i+1}\trans{\tau}p_i$ for $i\in\{0,\ldots,n-1\}$, and $p_0\models\phi_1\diam{a}\eps\phi_2$. We apply induction on $n$.
\begin{description}
\item
[$\boldsymbol{n=0}$] Then $p\models\phi_1$, and there is a $p'\in\mathds{P}$ with $p\trans{a}p'$ and $p'\models\eps\phi_2$. By Def.~\ref{def:eta}, $q\epsarrow q'\trans{a}q''\epsarrow q'''$ with $p\bis{\eta}q'$ and $p'\bis{\eta}q'''$. By induction on formula size, $q'\models\phi_1$ and $q'''\models\eps\phi_2$. Hence $q\models\eps(\phi_1\diam{a}\eps\phi_2)$.
\item
[$\boldsymbol{n>0}$] Since $p_n\trans{\tau}p_{n-1}$, according to Def.~\ref{def:eta} there are two possibilities.
\begin{enumerate}
\item
Either $p_{n-1}\bis{\eta}q$. Since $p_{n-1}\models\eps(\phi_1\diam{a}\eps\phi_2)$, by induction on $n$, $q\models\eps(\phi_1\diam{a}\eps\phi_2)$.
\item
Or $q\epsarrow q'\trans{\tau}q''\epsarrow q'''$ with $p_{n-1}\bis{\eta}q'''$. By induction on $n$, $p_{n-1}\models\eps(\phi_1\diam{a}\eps\phi_2)$, so $q'''\models\eps(\phi_1\diam{a}\eps\phi_2)$. Hence $q\models\eps(\phi_1\diam{a}\eps\phi_2)$.
\end{enumerate}
\end{description}
We conclude that $p\sim_{\IO{\eta}}q$.
\end{itemize}
($\Leftarrow$)
We prove that $\sim_{\IO{\eta}}$ is an $\eta$-bisimulation relation. The relation is clearly symmetric. Let $p\sim_{\IO{\eta}}q$. Suppose $p\trans{\alpha}p'$. If $\alpha=\tau$ and $p'\sim_{\IO{\eta}}q$, then the first condition of Def.\ \ref{def:eta} is fulfilled. So we can assume that either (i) $\alpha\not=\tau$ or (ii) $p'\not\sim_{\IO{\eta}}q$. We define
\[
\begin{array}{lcl}
Q' &=& \{q'\in\mathds{P}\mid q\epsarrow q'\wedge p\not\sim_{\IO{\eta}}q'\} \\
Q''' &=& \{q'''\in\mathds{P}\mid\exists q',q''\in\mathds{P}:q\epsarrow q'\trans\alpha q''\epsarrow q'''\wedge p'\not\sim_{\IO{\eta}}q'''\}
\end{array}
\]
For each $q'\in Q'$, let $\phi_{q'}$ be a formula in $\IO{\eta}$ such that $p\models\phi_{q'}$ and $q'\not\models\phi_{q'}$. (Such a formula always exists because $\IO{\eta}$ is closed under negation $\neg$.) We define
\[
\phi=\bigwedge_{q'\in Q'}\phi_{q'}
\]
Similarly, for each $q'''\in Q'''$, let $\psi_{q'''}$ be a formula in $\IO{\eta}$ such that $p'\models\psi_{q'''}$ and $q'''\not\models\psi_{q'''}$. We define
\[
\psi=\bigwedge_{q'''\in Q'''}\psi_{q'''}
\]
Clearly, $\phi,\psi\in\IO{\eta}$, $p\models\phi$ and $p'\models\psi$. We distinguish two cases.
\begin{enumerate}
\item
$\alpha\not=\tau$. Since $p\models\eps(\phi\diam\alpha\eps\psi)\in\!\IO{\eta}$ and $p\!\sim_{\IO{\eta}}\! q$, also $q\models\eps(\phi\diam\alpha\eps\psi)$. Hence, $q\epsarrow q'\trans\alpha q''\epsarrow q'''$ with $q'\models\phi$ and $q'''\models\psi$. By the definition of $\phi$ and $\psi$ it follows that $p\sim_{\IO{\eta}}q'$ and $p'\sim_{\IO{\eta}}q'''$.
\item
$\alpha=\tau$ and $p'\not\sim_{\IO{\eta}}q$. Let $\hat\phi\in\IO{\eta}$ such that $p'\models\hat\phi$ and $q\not\models\hat\phi$. Since $p\models\eps(\hat\phi\wedge\psi)\in\IO{\eta}$ and $p\sim_{\IO{\eta}}q$, also $q\models\eps(\hat\phi\wedge\psi)$. Since $q\not\models\hat\phi$, $q\trans\tau q''\epsarrow q'''$ with $q'''\models\hat\phi\wedge\psi$. By the definition of $\psi$ it follows that $p'\sim_{\IO{\eta}}q'''$.
\end{enumerate}
Both cases imply that the second condition of Def.\ \ref{def:eta} is fulfilled. We therefore conclude that $\sim_{\IO{\eta}}$ is an $\eta$-bisimulation relation.
\end{proof}
Using the first part of Thm.~\ref{thm:characterisation}, which was proved above, it is not hard to derive the second part of Thm.~\ref{thm:characterisation}, i.e.\ that $\IO{r\eta}$ is a modal characterisation of rooted $\eta$-bisimulation equivalence.

\end{document}
