\documentclass[runningheads]{llncs}
\newfont{\fsc}{eusm10}
\usepackage{theorem}\theorembodyfont{\rmfamily}
\usepackage{url}
\usepackage{amsmath} % \boldsymbol
\usepackage{dsfont}
\usepackage{epsfig}
\usepackage{amssymb}

\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{\notbis}[1]{\not\mathrel{\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}\,_{#1}\,}}
\newcommand{\var}{{\it var}}
\newcommand{\ar}{{\it ar}}
\newcommand{\IO}[1]{\mathds{O}_{#1}}
\renewcommand{\phi}{\varphi}

\begin{document}
\pagestyle{headings}
\mainmatter

\title{Divide and Congruence: \\
       From Decomposition of Modalities \\
       to Preservation of Branching Bisimulation}
\titlerunning{Divide and Congruence}
\authorrunning{W.J. Fokkink, R.J. van Glabbeek and P. de Wind}

\author{Wan Fokkink \inst{1,2} \and Rob van Glabbeek \inst{3,4} \and Paulien de Wind \inst{1}}
\institute{
Vrije Universiteit Amsterdam, Section Theoretical Computer Science, Amsterdam
\and
CWI, Department of Software Engineering, Amsterdam
\and
National ICT Australia, Sydney
\and
University of New South Wales, School of Computer Science and Engineering, Sydney \\
\email{\{wanf,pdwind\}@cs.vu.nl, rvg@cs.stanford.edu}
}

\date{}
\maketitle

\begin{abstract}
We present a method for decomposing modal formulas for processes with the internal action $\tau$. 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. We use this decomposition method to derive congruence formats for branching and rooted branching bisimulation equivalence.
\end{abstract}


\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 behavioural 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 branching bisimulation \cite{GlWe96}.

In general a behavioural 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 behavioural 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.

Behavioural equivalences can be characterised 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 a modal characterisation of bisimulation.

{\sc Larsen and Liu} \cite{LL91} 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} \cite{FvGdW03} to tyft/tyxt format. In \cite{BFvG04}, the decomposition method was applied to obtain congruence formats for a range of behavioural equivalences. 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$.

Here 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. In order to minimise the complexity inherent in the combination of modal decomposition and the internal action $\tau$, we apply the decomposition method to so-called abstraction-free TSSs, where only the patience rules contain the label $\tau$ in the conclusion. Furthermore, we use this decomposition method to obtain congruence formats for branching and rooted branching bisimulation. These formats include TSSs that are not abstraction-free, owing to the compositionality of the abstraction operator, which renames certain actions into $\tau$. Our formats use two predicates on arguments of function symbols, to mark both running processes and processes that may have started running. Our congruence formats are more liberal than the simply BB and RBB cool formats from \cite{Blo95} and the RBB safe format from \cite{Fok00}. In Sect.\ \ref{sec:related} we will present a more in-depth comparison with congruence formats from \cite{Blo95,Fok00,vGl05}.

In a companion paper \cite{FvGdW05}, we derive congruence formats for $\eta$- and rooted $\eta$-bisimulation, with a reference to the current paper for the decomposition method. 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 behavioural equivalences.


\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 \plat{$p\trans\alpha q$} for $(p,\alpha,q)\in\;\rightarrow$ and \plat{$p\ntrans\alpha$} for \plat{$\neg\exists q\in\mathds{P}:p\trans\alpha q$}. Furthermore, \plat{$\epsarrow$} denotes the transitive-reflexive closure of \plat{$\trans{\tau}$}.

\begin{definition}[\cite{GlWe96}]\label{def:bb}
A symmetric relation $B\subseteq\mathds{P}\times\mathds{P}$ is a \emph{branching bisimulation} if $pBq$ and \plat{$p\trans{\alpha}p'$} implies that either $\alpha = \tau$ and $p'\,B\,q$, or \plat{$q\epsarrow q' \trans{\alpha} q''$} for some $q'$ and $q''$ with $pBq'$ and $p'Bq''$.

Processes $p,q$ are {\em branching bisimilar}, denoted by $p\bis{b}q$, if there exists a branching bisimulation $B$ with $pBq$.
\end{definition}
Branching 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}[\cite{GlWe96}]\label{def:rbb}
A symmetric relation $R\subseteq\mathds{P}\times\mathds{P}$ is a \emph{rooted branching bisimulation} if $pRq$ and \plat{$p \trans{\alpha} p'$} implies that \plat{$q \trans{\alpha}q '$} for some
$q'$ with $p'\bis{b}q'$.

Processes $p,q$ are \emph{rooted branching bisimilar}, denoted by $p\bis{rb}q$, if there exists a rooted branching 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 connectives $\eps\phi$ and $\diam{\hat\tau}\phi$.

\begin{definition}\label{def:formulas}
The class $\mathds{O}$ of \emph{modal formulas} is defined as follows, where $I$ ranges over all index sets:
\[
\mathds{O} \qquad \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \diam{\alpha}\phi ~|~ \eps\phi ~|~ \diam{\hat\tau}\phi
\]
\end{definition}
\noindent
$p\models\phi$ denotes that $p$ satisfies $\phi$. By definition, $p\models\diam{\alpha}\phi$ if \plat{$p\trans{\alpha}p'$} with $p'\models\phi$, $p\models\eps\phi$ if \plat{$p\epsarrow p'$} with $p'\models\phi$, and $p\models\diam{\hat\tau}\phi$ if either $p\models\phi$ or \plat{$p\trans{\tau}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$, $\phi\diam{\alpha}\phi'$ for $\phi\land\diam{\alpha}\phi'$, and $\phi\diam{\hat\tau}\phi'$ for $\phi\land\diam{\hat\tau}\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{b}$ and $\IO{rb}$ of $\mathds{O}$ are defined as follows:
\begin{align*}
&\IO{b}       && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \eps(\phi\diam{\hat{\tau}}\phi') ~|~ \eps(\phi\diam{a}\phi') \\
&\IO{rb}      && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \diam{\alpha}\hat\phi ~|~ \hat\phi ~(\hat\phi\in\IO{b})
\end{align*}
The classes $\IO{b}^\equiv$ and $\IO{rb}^\equiv$ are the closures of $\IO{b}$, respectively $\IO{rb}$, under $\equiv$.
\end{definition}
\noindent
The last clause in the definition of $\IO{rb}$ guarantees that $\IO{b} \subseteq \IO{rb}$, which will be needed in the proof of Prop.~\ref{prop:rooted_bra_preservation}. If this clause were omitted, it would still follow that $\IO{b}^\equiv\subseteq\IO{rb}^\equiv$, using structural induction together with $\eps\phi\equiv\phi\vee\diam{\tau}\eps\phi$ and $\diam{\hat\tau} \phi \equiv \phi \vee \diam\tau \phi$. Note that if $\phi\in\IO{b}^\equiv$, then $\eps\phi\equiv\eps(\phi\diam{\hat\tau}\phi)\in\IO{b}^\equiv$.

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{b}}q \Leftrightarrow p\sim_{\IO{b}^\equiv}q$ and $p\sim_{\IO{rb}}q \Leftrightarrow p\sim_{\IO{rb}^\equiv}q$.

\begin{theorem}\label{thm:characterisation}
$p\bis{b}q\Leftrightarrow p\sim_{\IO{b}}q$ and $p\bis{rb}q\Leftrightarrow p\sim_{\IO{rb}}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 \plat{$t \trans\alpha t'$} or \plat{$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}. \plat{$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 \plat{$t\trans\alpha t'$}. %A \emph{transition system specification (TSS)} is a set of transition rules.
A {\em transition system specification (TSS)}, written $(\Sigma,R)$,
consists of a signature $\Sigma$ and a collection $R$
of transition rules over $\Sigma$.
\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 \plat{$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_bra_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 \plat{$t \trans{\alpha} t'$} and \plat{$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 \plat{$P\vdash_{\it ws}p\ntrans\alpha$} or
\plat{$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} (or {\em $\aleph$-liquid} for short), 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$; otherwise the occurrence is at an {\em $\aleph$-frozen} position.
\end{definition}
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 $\aleph$-liquid arguments.

\begin{definition}\label{def:patience_rule}
An ntyft rule is a {\em patience rule} for $f$ if it is of the form
\[
\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)})}
\]
It is an {\em $\aleph$-patience rule} if $\aleph(f,i)$.
\end{definition}
\noindent
An ntytt rule is {\em $\aleph$-patient} 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{abstraction-free} with respect to $\aleph$ if only $\aleph$-patience rules
have a conclusion of the form \plat{$t\trans{\tau}u$}.
\end{definition}
\noindent
In Section \ref{sec:bra} we will obtain preservation results of modal
formulas in $\IO{b}$ and $\IO{rb}$ on abstraction-free TSSs. We will lift these
to congruence results for $\bis{b}$ and $\bis{rb}$ on general TSSs,
using two facts: abstraction operators preserve $\bis{b}$ and $\bis{rb}$,
and each TSS can be embedded in an abstraction-free TSS augmented
with an abstraction operator.


\subsection{Ruloids}

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 \plat{$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 \plat{$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 \plat{$f(x_1,\ldots,x_n)\ntrans{\alpha}$} is obtained by picking
one premise from each rule with a conclusion \plat{$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^+$.
The notion of irredundant provability is adapted in a straightforward
fashion to accommodate rules with a negative conclusion.
In \cite{BFvG04} it is established that $P\vdash_{\it ws}\mu$ if and only if $\mu$ is irredundantly
provable from $P^+$, for all closed literals $\mu$. $P$-ruloids are those 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 \plat{$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}[\cite{BFvG04}]\label{prop:ruloid}
Let $P$ be a TSS in ready simulation format.\\
Then \plat{$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}
\noindent
It is not hard to see that the notion of abstraction-freeness is preserved by the transformation to $P$-ruloids.

\begin{lemma}
\label{lem:abstractionfree}
If a TSS $P$ is abstraction-free with respect to some $\aleph$, then
all $P$-ruloids with a conclusion of the form \plat{$t\trans{\tau}u$}
are $\aleph$-patient.
\end{lemma}


\section{Decomposition of Modal Formulas}

In this section we 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}.

In order to minimise the complexity inherent in the combination of modal decomposition and the internal action $\tau$, we apply the decomposition method to abstraction-free TSSs. In Sect.\ \ref{sec:congruence}, where we will develop congruence formats on the basis of this decomposition method, we will be able to circumvent the restriction to abstraction-free TSSs, owing to the compositionality of the abstraction operator.

\begin{definition}\label{def:decomposition}
Let $P$ be a TSS in ready simulation format, which contains the $\aleph$-patience rules and is abstraction-free with respect to $\aleph$. 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{dec1}
$\psi\in t^{-1}(\bigwedge_{i\in I}\phi_i)$ iff for $x\in V$
\[
\psi(x)= \displaystyle{\bigwedge_{i\in I}\psi_i(x)}
\]
where $\psi_i\in t^{-1}(\phi_i)$ for $i\in I$. 

\item\label{dec2}
$\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\label{dec3}
$\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\label{dec4}
$\psi\in t^{-1}(\eps\phi)$ iff there is a $\chi\in t^{-1}(\phi)$ with
\[
\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\label{dec5}
$\psi\in t^{-1}(\diam{\hat\tau}\phi)$ iff one of the following holds:

\begin{enumerate}
\item
$\psi\in t^{-1}(\phi)$, or

\item
there is an $x_0\in V$ that occurs $\aleph$-liquid in $t$ and a $\chi\in t^{-1}(\phi)$ such that
\[
\psi(x)=\left\{
\begin{array}{ll}
\diam{\hat\tau}\chi(x) & \textrm{if $x=x_0$} \\
\chi(x) & \textrm{if $x\not=x_0$}\\
\end{array}
\right.
\]
\end{enumerate}

\item\label{dec6}
$\psi\in\rho(t)^{-1}(\phi)$ for $\rho:\var(t)\rightarrow V$ not injective
iff there is a $\chi\in t^{-1}(\phi)$ with
\[
\psi(x)=\bigwedge_{y\in\rho^{-1}(x)}\chi(y)\qquad\text{ for }x\in V
\]
\end{enumerate}
\end{definition}
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}(\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)$.

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
\plat{$\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 \plat{$x\trans{\beta}y\in H$} and conjuncts $\neg\diam{\gamma}\top$
for \plat{$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.

The following theorem will be the key to the forthcoming congruence results.

\begin{theorem}\label{thm:decomposition}
Given a complete TSS $P$ in ready simulation format, which contains the $\aleph$-patience rules and is abstraction-free with respect to $\aleph$. For any term $t$, closed substitution $\sigma$ and $\phi\in\mathds{O}$:
\[
\sigma(t)\models\phi\ \Leftrightarrow
\ \exists\psi\in t^{-1}(\phi)\ \forall x\in \var(t):\sigma(x)\models\psi(x)
\]
\end{theorem}

\begin{proof}
By structural induction on $\phi$. First we treat the case where $t$ is univariate.
\begin{itemize}

\item
$\phi=\bigwedge_{i\in I}\phi_i$

$\sigma(t) \models \bigwedge_{i\in I}\phi_i\ \Leftrightarrow
\ \forall i\in I: \sigma(t) \models \phi_i
\Leftrightarrow\ \forall i\in I\ \exists \psi_i \in t^{-1} (\phi_i)\ \forall x\in\var(t): \sigma(x) \models \psi_i(x)
\Leftrightarrow\ \exists \psi \in t^{-1}(\bigwedge_{i\in I}\phi_i)\ \forall x\in \var(t): \sigma(x) \models \psi(x)$.

\item
$\phi=\neg\phi'$

$\sigma(t)\models\neg\phi'\Leftrightarrow \sigma(t)\not\models\phi'\Leftrightarrow\exists h:t^{-1}(\phi')\rightarrow \var(t)\ \forall\chi\in t^{-1}(\phi'):\sigma(h(\chi))\not\models\chi(h(\chi))\Leftrightarrow\exists h:t^{-1}(\phi')\rightarrow \var(t)\ \forall x\in\var(t):\sigma(x)\models\bigwedge_{\chi\in h^{-1}(x)}\neg\chi(x)\Leftrightarrow\exists\psi\in t^{-1}(\neg\phi')\ \forall x\in\var(t):\sigma(x)\models\psi(x)$.

\item
$\phi=\diam{\alpha}\phi'$

($\Rightarrow$)
Let $\sigma(t)\models \diam{\alpha}\phi'$. Then \plat{$P \vdash_{\it ws} \sigma(t) \trans{\alpha} p$} with $p \models \phi'$. By Prop.\ \ref{prop:ruloid} there is 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)$, i.e.\ $\sigma'(x) = \sigma(x)$ for $x \in \var(t)$, and $\sigma'(u)=p$. Since $\sigma'(u) \models \phi'$, by induction there is a $\chi \in u^{-1} (\phi')$ with $\sigma'(z) \models \chi(z)$ for $z \in \var(u)$. Furthermore, $\sigma'(z) \models \chi(z)\equiv\top$ for $z \not\in \var(u)$. Define $\psi \in t^{-1}(\diam{\alpha}\phi')$ as in Def.~\ref{def:decomposition}.\ref{dec3}, using $\frac{H}{t \trans{\alpha} u}$ and $\chi$. Let $x \in \var(t)$. For \plat{$x\trans{\beta}y\in H$}, \plat{$P \vdash_{\it ws} \sigma'(x) \trans{\beta} \sigma'(y) \models \chi(y)$}, so $\sigma'(x) \models\diam{\beta}\chi(y)$. Moreover, for \plat{$x\ntrans{\gamma}\;\in H$}, \plat{$P \vdash_{\it ws} \sigma'(x) \ntrans{\gamma}$}, so the consistency of $\vdash_{\it ws}$ (see \cite{vGl04}) yields $P\not\vdash_{\it ws}\sigma'(x)\trans{\gamma}q$ for all closed terms $q$, and thus $\sigma'(x) \models \neg\diam{\gamma}\top$. Hence $\sigma(x) = \sigma'(x) \models \psi(x)$.

\vspace{2mm}
($\Leftarrow$) Let $\psi \in t^{-1}(\diam{\alpha}\phi')$ with $\sigma(x)
\models \psi(x)$ for $x \in \var(t)$. There is a $P$-ruloid
\[
\frac{\{x\trans{\beta_i}y_i\mid i\in I_x,\ x\in\var(t)\} \cup
\{x\ntrans{\gamma_j}\mid j\in J_x,\ x\in\var(t)\}}{t \trans{\alpha} u}
\]
and a $\chi \in u^{-1}(\phi')$ with $\psi(x) = \chi(x) \land \bigwedge_{i\in I_x} \diam{\beta_i}\chi(y_i) \land\bigwedge_{j \in J_x}\neg\diam{\gamma_j}\top$ for $x \in \var(t)$. For $x\in \var(t)$, $\sigma(x)\models\psi(x)$ yields, for $i\in I_x$, \plat{$P \vdash_{\it ws} \sigma(x) \trans{\beta_i} p_i$} with $p_i \models \chi(y_i)$ for some closed term $p_i$; moreover, for $j\in J_x$, \plat{$P \not\vdash_{\it ws} \sigma(x) \trans{\gamma_j} q$} for all closed terms $q$, so by the completeness of $P$, \plat{$P \vdash_{\it ws} \sigma(x) \ntrans{\gamma_j}$}. Define $\sigma'(x) = \sigma(x)$ and $\sigma'(y_i) = p_i$ for $x \in \var(t)$ and $i \in I_x$. Here we use that the $y_i$ are all different and do not occur in $t$. Then $\sigma'(z) \models \chi(z)$ for $z\in \var(u)$, since $\var(u)\subseteq\{x,y_i\mid x\in\var(t),i\in I_x\}$. So by induction, $\sigma'(u) \models \phi'$. Moreover, for $x\in\var(t)$, $P \vdash_{\it ws} \sigma'(x) \trans{\beta_i} \sigma'(y_i)$ for $i\in I_x$, and \plat{$P \vdash_{\it ws} \sigma'(x) \ntrans{\gamma_j}$} for $j\in J_x$, so by Prop.\ \ref{prop:ruloid}, \plat{$P \vdash_{\it ws} \sigma'(t) \trans{\alpha} \sigma'(u)$}. Hence $\sigma(t) = \sigma'(t) \models \diam{\alpha}\phi'$.

\item
$\phi=\eps\phi'$

($\Rightarrow$)
We prove by induction on $n$: if \plat{$P\vdash_{\it ws}p_i\trans{\tau}p_{i+1}$} for $i\in\{0,\ldots,n-1\}$ with $\sigma(t)=p_0$ and $p_n\models\phi'$, then there is a $\psi\in t^{-1}(\eps\phi')$ with $\sigma(x)\models\psi(x)$ for $x\in \var(t)$.

\begin{description}
\item[$\boldsymbol{n=0}$] 
Since $\sigma(t)=p_0\models\phi'$, by induction on formula size, there is a $\chi\in t^{-1}(\phi')$ with $\sigma(x)\models\chi(x)$ for $x\in \var(t)$. Define $\psi\in t^{-1}(\eps\phi')$ as in Def.~\ref{def:decomposition}.\ref{dec4}, using $\chi$. Then $\sigma(x)\models\psi(x)$ for $x\in \var(t)$.

\item[$\boldsymbol{n>0}$] 
Since \plat{$P\vdash_{\it ws}\sigma(t)\trans{\tau}p_1$}, by Prop.\ \ref{prop:ruloid} there is a $P$-ruloid $\frac{H}{t\trans{\tau}u}$ and a $\sigma'$ with $P\vdash_{\it ws}\sigma'(\mu)$ for $\mu\in H$, $\sigma'(t)=\sigma(t)$, i.e.\ $\sigma'(x)=\sigma(x)$ for $x\in \var(t)$, and $\sigma'(u)=p_1$. Since $\sigma'(u)=p_1\trans{\tau}\cdots\trans{\tau}p_n\models\eps\phi'$, by induction on $n$, there is a $\chi\in u^{-1}(\eps\phi')$ with $\sigma'(y)\models\chi(y)$ for $y\in \var(u)$. Furthermore, $\sigma'(y)\models\chi(y)\equiv\top$ for $y\not\in\var(u)$. Since $P$ is abstraction-free, by Lem.\ \ref{lem:abstractionfree}, the $P$-ruloid $\frac{H}{t\trans{\tau}u}$ must be $\aleph$-patient. Thus \plat{$H=\{x_0\trans{\tau}y_0\}$}, where $x_0$ occurs $\aleph$-liquid in $t$ and, since $t$ is univariate, $u=t[y_0/x_0]$. Moreover, $y_0\not\in\var(t)$, so $u$ is also univariate. The occurrence of $y_0$ in $u$ is $\aleph$-liquid, so according to Def.~\ref{def:decomposition}.\ref{dec4}, $\chi(y_0)$ is of the form $\eps\phi''$. Let $\psi(x_0)=\chi(y_0)$, $\psi(y_0)=\chi(x_0)\equiv\top$, and $\psi(z)=\chi(z)$ otherwise. By alpha-conversion, $\chi\in u^{-1}(\eps\phi')$ implies $\psi\in t^{-1}(\eps\phi')$. For $x\in \var(t)\backslash\{x_0\}$, $\sigma(x)=\sigma'(x)\models\chi(x)=\psi(x)$. Furthermore, \plat{$P\vdash_{\it ws}\sigma'(x_0)\trans{\tau}\sigma'(y_0)$} and $\sigma'(y_0)\models\chi(y_0)=\psi(x_0)$; so since $\psi(x_0)$ is of the form $\eps\phi''$, $\sigma(x_0)=\sigma'(x_0)\models\psi(x_0)$.
\end{description}

\vspace{1mm}
($\Leftarrow$)
Let $\psi\in t^{-1}(\eps\phi')$ with $\sigma(x)\models\psi(x)$ for $x\in\var(t)$. Then there is a  $\chi\in t^{-1}(\phi')$ with $\psi(x)=\eps\chi(x)$ if $x$ occurs $\aleph$-liquid in $t$ and $\psi(x)=\chi(x)$ otherwise. For each $x$ that occurs $\aleph$-liquid in $t$, $\sigma(x)\models\psi(x)=\eps\chi(x)$, i.e.\ \plat{$\sigma(x)\epsarrow p_x$} with $p_x\models\chi(x)$. Define $\sigma'(x)=p_x$ if $x$ occurs $\aleph$-liquid in $t$ and $\sigma'(x)=\sigma(x)$ otherwise. Due to the presence of the $\aleph$-patience rules and the fact that $t$ is univariate, \plat{$\sigma(t)\epsarrow \sigma'(t)$}. Furthermore, $\sigma'(x)\models\chi(x)$ for $x\in \var(t)$, so by induction on formula size, $\sigma'(t)\models\phi'$. Hence $\sigma(t)\models\eps\phi'$.

\item
$\phi=\diam{\hat\tau}\phi'$

($\Rightarrow$)
Suppose $\sigma(t)\models\diam{\hat\tau}\phi'$. Then either $\sigma(t)\models\phi'$ or \plat{$P\vdash_{\it ws}\sigma(t)\trans{\tau}p\models\phi'$} for some closed term $p$. In the first case, by induction there is a $\psi\in t^{-1}(\phi')$ such that $\sigma(x)\models\psi(x)$ for $x\in\var(t)$; by Def.~\ref{def:decomposition}.\ref{dec5}(a), $\psi\in t^{-1}(\diam{\hat\tau}\phi')$, and we are done. In the second case, by Prop.~\ref{prop:ruloid} there is a $P$-ruloid $\frac{H}{t\trans{\tau}u}$ and a closed substitution $\sigma'$ with $P\vdash_{\it ws}\sigma'(\mu)$ for $\mu\in H$, $\sigma'(t)=\sigma(t)$, i.e.\ $\sigma'(x)=\sigma(x)$ for $x\in \var(t)$, and $\sigma'(u)=p$. Since $\sigma'(u)\models\phi'$, by induction there is a $\chi\in u^{-1}(\phi')$ such that $\sigma'(y)\models\chi(y)$ for $y\in \var(u)$. Furthermore, $\sigma'(y)\models\chi(y)\equiv\top$ for $y\not\in \var(u)$. Since $P$ is abstraction-free, by Lem.~\ref{lem:abstractionfree}, the $P$-ruloid $\frac{H}{t\trans{\tau}u}$ must be $\aleph$-patient. Thus \plat{$H=\{x_0\trans{\tau}y_0\}$}, where $x_0$ occurs $\aleph$-liquid in $t$ and, since $t$ is univariate, $u=t[y_0/x_0]$. Moreover, $y_0\not\in\var(t)$, so $u$ is also univariate. Let $\psi(x_0)=\diam{\hat\tau}\chi(y_0)$, $\psi(y_0)=\chi(x_0)\equiv\top$, and $\psi(x)=\chi(x)$ otherwise. By Def.~\ref{def:decomposition}.\ref{dec5}(b) together with alpha-conversion, $\psi\in t^{-1}(\diam{\hat\tau}\phi')$. For $x\in \var(t)\backslash\{x_0\}$, $\sigma(x)=\sigma'(x)\models\chi(x)=\psi(x)$. Moreover, since \plat{$P\vdash_{\it ws}\sigma'(x_0)\trans{\tau}\sigma'(y_0)$} and $\sigma'(y_0)\models\chi(y_0)$, it follows that $\sigma(x_0)=\sigma'(x_0)\models\diam{\hat\tau}\chi(y_0)=\psi(x_0)$.

\vspace{2mm}
($\Leftarrow$)
Suppose $\psi\in t^{-1}(\diam{\hat\tau}\phi')$ with $\sigma(x)\models\psi(x)$ for all $x\in\var(t)$. If $\psi\in t^{-1}(\phi')$, then by induction $\sigma(t)\models\phi'$, so $\sigma(t)\models\diam{\hat\tau}\phi'$, and we are done. Suppose that for some $\chi\in t^{-1}(\phi')$ and some $x_0$ that occurs $\aleph$-liquid in $t$, $\psi(x)=\chi(x)$ for $x\not=x_0$ and $\psi(x_0)=\diam{\hat\tau}\chi(x_0)$. Then $\sigma(x)\models\chi(x)$ for $x\in\var(t)\backslash\{x_0\}$. Furthermore, $\sigma(x_0)\models\psi(x_0)=\diam{\hat\tau}\chi(x_0)$, so either $\sigma(x_0)\models\chi(x_0)$ or \plat{$\sigma(x_0)\trans{\tau}p\models\chi(x_0)$} for some closed term $p$. In the first case, by induction $\sigma(t)\models\phi'$, so $\sigma(t)\models\diam{\hat\tau}\phi'$, and we are done. In the second case, define $\sigma'(x)=\sigma(x)$ for $x\in\var(t)$ and $\sigma'(y_0)=p$. Since \plat{$P\vdash_{\it ws}\sigma'(x_0)\trans{\tau}\sigma'(y_0)$}, and $\frac{x_0\trans{\tau}y_0}{t\trans{\tau}t[y_0/x_0]}$ is an $\aleph$-patient $P$-ruloid, by Prop.~\ref{prop:ruloid}, \plat{$P\vdash_{\it ws}\sigma'(t)\trans{\tau}\sigma'(t[y_0/x_0])$}. Furthermore, by induction $\sigma'(t[y_0/x_0])\models\phi'$. Hence $\sigma(t)=\sigma'(t)\models\diam{\hat\tau}\phi'$.

\end{itemize}
Finally, suppose $t$ is not univariate. Let $t=\rho(u)$ for some univariate $u$ and $\rho:\var(u)\rightarrow V$
not injective.
$\sigma(\rho(u))\models\phi \Leftrightarrow
\exists\chi\in u^{-1}(\phi)\ \forall y\in\var(u): \sigma(\rho(y))\models\chi(y) \Leftrightarrow
\exists\chi\in u^{-1}(\phi)\ \forall x\in\var(t): \sigma(x)\models\bigwedge_{y\in\rho^{-1}(x)}\chi(y) \Leftrightarrow
\exists\psi\in t^{-1}(\phi)\ \forall x\in\var(t): \sigma(x)\models\psi(x)$. \qed
\end{proof}

\noindent
The part of Thm.~\ref{thm:decomposition} that deals with the modalities $\bigwedge_{i\in I}$,
$\neg$ and $\diam{\alpha}$ only has been established in \cite{FvGdW03}.
There, a few examples are given showing how Def.~\ref{def:decomposition} can be used to
decompose a modal formula, as well as a counterexample showing that
the completeness requirement in Thm.~\ref{thm:decomposition} cannot simply be skipped.
The inclusion of the modalities $\diam{\epsilon}$ and
$\diam{\hat\tau}$ is new. The following example illustrates the use of
the decomposition method on a formula with the modality $\diam{\epsilon}$.

\begin{example}\label{ex:application_decomposition}
Let $A=\{a\}$ and $P=(\Sigma,R)$, where $\Sigma$ consists of a binary function symbol $\|$ with liquid arguments,
and $R$ contains the rules $\frac{x\trans\alpha x'}{x\|y\trans\alpha x'\|y}$ and
$\frac{y\trans\alpha y'}{x\|y\trans\alpha x\|y'}$ for $\alpha\in\{a,\tau\}$.
The TSS $P$ is complete and in ready simulation format. Furthermore, it contains the two
patience rules and is abstraction-free.

We compute $(x\|y)^{-1}(\eps\diam{a}\top)$. By Def.~\ref{def:decomposition}.\ref{dec4}, for each $\psi\in(x\|y)^{-1}(\eps\diam{a}\top)$ we have $\psi(x)=\eps\chi(x)$ and $\psi(y)=\eps\chi(y)$ for some $\chi\in(x\|y)^{-1}(\diam{a}\top)$. According to Def.~\ref{def:decomposition}.\ref{dec3}, $(x\|y)^{-1}(\diam{a}\top)=\{\chi_1,\chi_2\}$, where $\chi_1$ and $\chi_2$ are constructed from the only $P$-ruloids with a conclusion \plat{$x\|y\trans a\_$}, namely $\frac{x\trans a x'}{x\|y\trans a x'\|y}$ and $\frac{y\trans a y'}{x\|y\trans a x\|y'}$, together with $\xi_1\in(x'\|y)^{-1}(\top)$ resp.\ $\xi_2\in(x\|y')^{-1}(\top)$:
$$\begin{array}{l@{~~~~~}l}
\chi_1(x)=\xi_1(x)\land\diam a\xi_1(x')\equiv\diam a\top & \chi_2(x)=\top\\
\chi_1(y)=\top & \chi_2(y)=\xi_2(y)\land\diam a\xi_2(y')\equiv\diam a\top
\end{array}$$
Hence $(x\|y)^{-1}(\eps\diam{a}\top)=\{\psi_1,\psi_2\}$ with $\psi_1$ and $\psi_2$ defined as follows:
$$\begin{array}{l@{~~~~~}l}
\psi_1(x)=\eps\chi_1(x)\equiv\eps\diam a\top & \psi_2(x)=\eps\chi_2(x)=\eps\top\equiv\top \\
\psi_1(y)=\eps\chi_1(y)=\eps\top\equiv\top   & \psi_2(y)=\eps\chi_2(y)\equiv\eps\diam a\top 
\end{array}$$
\end{example}


\section{Branching Bisimulation as a Congruence}
\label{sec:congruence}

We proceed to apply the decomposition method from the previous section to derive congruence formats
for branching and rooted branching bisimulation equivalence. The idea is that the branching bisimulation
format must guarantee that a formula from $\IO{b}$ is always decomposed into formulas from $\IO{b}^\equiv$
(see Prop.~\ref{prop:rbrab-rbrab}).
Likewise, the rooted branching bisimulation format must guarantee that a formula from $\IO{rb}$ is always
decomposed into formulas from $\IO{rb}^\equiv$ (see Prop.~\ref{prop:rooted_bra_preservation}).
This implies the desired congruence results (see Thm.~\ref{thm:congruence1} and Thm.~\ref{thm:congruence2}).
In the derivation of the congruence formats, we will circumvent the restriction in the decomposition method
to abstraction-free TSSs, using 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 might currently be resting,
in which case no patience rules are needed for these arguments. Always $\aleph\subseteq\Lambda$.

\begin{definition}\label{def:rooted_bra_bisimulation_safe}
Let $\aleph\subseteq\Lambda$. An ntytt rule $\frac{H}{t\trans\alpha u}$ is {\em rooted branching bisimulation safe}
with respect to $\aleph$ and $\Lambda$ if:
\begin{enumerate}
\item
it has no lookahead,
\item
right-hand sides of premises occur only $\Lambda$-liquid in $u$, and
\item
if $x$ occurs exactly once\footnote{For the rooted branching bisimulation format
 in Def.~\ref{def:bra_bisimulation_format}, only the requirements for rules in
 which $t$ is univariate matter. The formulation of
 Def.~\ref{def:rooted_bra_bisimulation_safe} for general terms $t$ paves
 the way for Prop.~\ref{prop:preservation_bra_bisimulation_safe}.}
 in $t$, at a $\Lambda$-liquid position, then:
\begin{enumerate}
\item all occurrences of $x$ in the rule are $\Lambda$-liquid,
\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 $\aleph$-frozen in $t$, then $x$ does not occur $\aleph$-liquid
      in left-hand sides of premises.
\end{enumerate}
\end{enumerate}
In case $\Lambda$ is the universal predicate, we say that the rule is {\em branching bisimulation safe} with respect to $\aleph$.
\end{definition}

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

A TSS in ready simulation format is in {\em branching bisimulation format}
if, for some $\aleph$, it consists of the $\aleph$-patience rules and
rules that are branching bisimulation safe with respect to $\aleph$.
\end{definition}
%
If a TSS $P$ is in rooted branching bisimulation format then there
are smallest predicates $\aleph_0$ and $\Lambda_0$ such that $P$
consists of the $\aleph_0$-patience rules and rules that are rooted
branching bisimulation safe with respect to $\aleph_0$ and $\Lambda_0$.
Namely the $\Lambda_0$-liquid arguments are \emph{generated} by
requirements 2 and 3(a) of Def.\ \ref{def:rooted_bra_bisimulation_safe}; they are the smallest collection
of arguments such that these two requirements are satisfied.
Given $\Lambda_0$, $\aleph_0$ is the unique collection of arguments
within $\Lambda_0$ for which patience rules exists. For any TSS $P$,
$\aleph_0$ and $\Lambda_0$ can be calculated in this way, and whether
$P$ is in rooted branching bisimulation format then depends solely on
whether requirements 1 and 3(b--d) of Def.\ \ref{def:rooted_bra_bisimulation_safe} are satisfied.

When restricting to TSSs consisting of nxytt rules only, it becomes
easier to reformulate the definition of the rooted branching
bisimulation format without mentioning $\aleph$.
Namely, requirements 3(b--d) of Def.\ \ref{def:rooted_bra_bisimulation_safe}, together with the existence
of the patience rules required in Def.\ \ref{def:bra_bisimulation_format} then amount to
\begin{itemize}
\item [3.]
\begin{itemize}
\item [(b)] $x$ does not occur as the left-hand side of a negative premise,
\item [(c)] $x$ occurs at most once as the left-hand side of a
            positive premise, and this premise has a label from $A$, and 
\item [(d)] if within $t$, $x$ occurs in an argument of an operator $f$ for
            which there is no patience rule, then $x$ does not occur in the
            left-hand side of premises.
\end{itemize}
\end{itemize}
A TSS is now in rooted branching bisimulation format if it consists of
patience rules and rules that are rooted branching bisimulation safe with respect
to $\Lambda$ and that collection of patience rules.

Using this, it is not hard to see that the rooted branching
bisimulation format strengthens the RBB safe format from \cite{Fok00}.

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) branching bisimulation format, then so
are the $P$-ruloids.

\begin{proposition}
\label{prop:preservation_bra_bisimulation_safe}
If a TSS $P$ is in (rooted) branching bisimulation format with respect
to some $\aleph$ (and $\Lambda$), then each $P$-ruloid is either $\aleph$-patient
or (rooted) branching bisimulation safe with respect to $\aleph$ (and $\Lambda$).
\end{proposition}
The proof of Prop.~\ref{prop:preservation_bra_bisimulation_safe} is omitted here. The key part of the proof is to show that the decent (rooted) branching bisimulation format is preserved under irredundant provability. The adjective irredundant is essential here; this preservation result would fail if ``junk'' could be added to the premises of derived transition rules.


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

In this section we prove that given a TSS in rooted branching bisimulation format, if $\psi\in t^{-1}(\phi)$ with $\phi\in\IO{b}$, then $\psi(x)\in\IO{b}^{\equiv}$ if $x$ occurs only $\Lambda$-liquid in $t$. (That is why in the branching bisimulation format, $\Lambda$ must be universal.) If $\phi\in\IO{rb}$, then $\psi(x)\in\IO{rb}^{\equiv}$ for all variables $x$.

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

\begin{proof}
We apply structural induction on $\phi\in\IO{b}$. 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)\equiv\top\in\IO{b}^\equiv$. Suppose $x$ occurs once in $t$.

\begin{itemize}
\item $\phi=\bigwedge_{i\in I}\phi_i$ with $\phi_i\in\IO{b}$ for $i\in I$. By Def.~\ref{def:decomposition}.\ref{dec1}, $\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{b}^\equiv$ for $i\in I$, so $\psi(x)\in\IO{b}^\equiv$.

\item $\phi=\neg\phi'$ with $\phi'\in\IO{b}$. By Def.~\ref{def:decomposition}.\ref{dec2}, 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{b}^\equiv$ for $\chi\in h^{-1}(x)$, so $\psi(x)\in\IO{b}^\equiv$.

\item $\phi=\eps(\phi_1\diam{\hat\tau}\phi_2)$ with $\phi_1,\phi_2\in\IO{b}$. By Def.~\ref{def:decomposition}.\ref{dec4}, either $\psi(x)=\eps\chi(x)$ if $x$ occurs $\aleph$-liquid in $t$, or $\psi(x)=\chi(x)$ if $x$ occurs $\aleph$-frozen in $t$, for some $\chi\in t^{-1}(\phi_1\diam{\hat\tau}\phi_2)$. By Def.~\ref{def:decomposition}.\ref{dec1}, $\chi(x)=\chi_1(x)\land\chi_2(x)$ with $\chi_1\in t^{-1}(\phi_1)$ and $\chi_2\in t^{-1}(\diam{\hat\tau}\phi_2)$. By Def.~\ref{def:decomposition}.\ref{dec5}, either $\chi_2(x)=\diam{\hat\tau}\xi(x)$ and $x$ occurs $\aleph$-liquid in $t$, or $\chi_2(x)=\xi(x)$, for some $\xi\in t^{-1}(\phi_2)$. So $\psi(x)$ is of the form $\eps(\chi_1(x)\diam{\hat\tau}\xi(x))$, $\eps(\chi_1(x)\land\xi(x))$ or $\chi_1(x)\land\xi(x)$. By induction, $\chi_1(x),\xi(x)\in\IO{b}^\equiv$. Hence $\psi(x)\in\IO{b}^\equiv$.

\item $\phi=\eps(\phi_1\diam{a}\phi_2)$ with $\phi_1,\phi_2\in\IO{b}$. By Def.~\ref{def:decomposition}.\ref{dec4}, either $\psi(x)=\eps\chi(x)$ if $x$ occurs $\aleph$-liquid in $t$, or $\psi(x)=\chi(x)$ if $x$ occurs $\aleph$-frozen in $t$, for some $\chi\in t^{-1}(\phi_1\diam{a}\phi_2)$. By Def.~\ref{def:decomposition}.\ref{dec1}, $\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}\phi_2)$. By induction, $\chi_1(x)\in\IO{b}^\equiv$. By Def.~\ref{def:decomposition}.\ref{dec3},
\[
\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}(\phi_2)$ and $P$-ruloid $\frac{H}{t\trans{a}u}$. Since $a\not=\tau$, by Prop.~\ref{prop:preservation_bra_bisimulation_safe}, $\frac{H}{t\trans{a}u}$ is rooted branching bisimulation safe with respect to $\aleph$ and $\Lambda$. 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 $\Lambda$-liquid in $u$. So by induction, $\xi(x)\in\IO{b}^\equiv$ and $\xi(y)\in\IO{b}^\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 branching bisimulation safe with respect to $\aleph$ and $\Lambda$ 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$. Hence either $\chi_2(x)=\xi(x)$ or $\chi_2(x)=\xi(x)\diam{b}\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{b}^\equiv$ or $\psi(x)\equiv\eps(\chi_1(x)\land\xi(x)\diam{b}\xi(y))\in\IO{b}^\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 branching bisimulation safe with respect to $\aleph$ and $\Lambda$ 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{b}^\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}.\ref{dec6}, $\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{b}^\equiv$ for $y\in\rho^{-1}(x)$. Hence $\psi(x)\in\IO{b}^\equiv$. \qed
\end{proof}

\begin{proposition}\label{prop:rooted_bra_preservation}
Let $P$ be an abstraction-free TSS in rooted branching bisimulation format, with respect to some $\aleph$ and $\Lambda$. For any term $t$ and variable $x$:
\[
\phi\in\IO{rb}\ \Rightarrow\ \forall\psi\in t^{-1}(\phi):\psi(x)\in\IO{rb}^\equiv
\]
\end{proposition}

\begin{proof}
We apply structural induction on $\phi\in\IO{rb}$.
Let $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:rbrab-rbrab}. If
$x\not\in\var(t)$, then $\psi(x)\equiv\top\in\IO{rb}^\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:rbrab-rbrab}.

\item
$\phi=\diam\alpha\phi'$ with $\phi'\in\IO{b}$. By Def.~\ref{def:decomposition}.\ref{dec3},
\[
\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}(\phi')$ and $P$-ruloid $\frac{H}{t\trans\alpha u}$. By induction, $\chi(x)\in\IO{rb}^\equiv$. (Induction may be applied because $\phi'\in\IO{b}\subseteq\IO{rb}$.) By Prop.~\ref{prop:preservation_bra_bisimulation_safe}, $\frac{H}{t\trans\alpha u}$ is either rooted branching bisimulation safe with respect to $\aleph$ and $\Lambda$ or $\aleph$-patient. In either case, variables in right-hand sides of premises in $H$ occur only $\Lambda$-liquid in $u$. By Prop.~\ref{prop:rbrab-rbrab}, $\chi(y)\in\IO{b}^\equiv$ for \plat{$x\trans{\beta}y\in H$}, so $\diam{\beta}\chi(y)\in\IO{rb}^\equiv$. Also $\neg\diam{\gamma}\top\in\IO{rb}^\equiv$. Hence $\psi(x)\in\IO{rb}^\equiv$.
\item
$\phi\in\IO{b}$. If the occurrence of $x$ in $t$ is $\Lambda$-liquid, then $\psi(x)\in\IO{rb}^\equiv$ follows from Prop.\ \ref{prop:rbrab-rbrab}. So we can assume that this occurrence is $\Lambda$-frozen, and hence $\aleph$-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_1\diam{\hat\tau}\phi_2)$ with $\phi_1,\phi_2\in\IO{b} \subseteq \IO{rb}$.
Since the occurrence of $x$ in $t$ is $\aleph$-frozen, by Def.~\ref{def:decomposition}.\ref{dec4}, $\psi(x)=\chi(x)$ for some $\chi\in t^{-1}(\phi_1\diam{\hat\tau}\phi_2)$. By Def.~\ref{def:decomposition}.\ref{dec1}, $\chi(x)=\chi_1(x)\land\chi_2(x)$ with $\chi_1\in t^{-1}(\phi_1)$ and $\chi_2\in t^{-1}(\diam{\hat\tau}\phi_2)$. Since the occurrence of $x$ in $t$ is $\aleph$-frozen, by Def.~\ref{def:decomposition}.\ref{dec5}, $\chi_2(x)=\xi(x)$ for some $\xi\in t^{-1}(\phi_2)$. By induction, $\chi_1(x),\xi(x)\in\IO{rb}^\equiv$. Hence $\psi(x)\in\IO{rb}^\equiv$.
\item[$\ast$]
$\phi=\eps(\phi_1\diam{a}\phi_2)$  with $\phi_1,\phi_2\in\IO{b} \subseteq \IO{rb}$.
Since the occurrence of $x$ in $t$ is $\aleph$-frozen, by
Def.~\ref{def:decomposition}.\ref{dec4}, $\psi(x)=\chi(x)$ for some $\chi\in
t^{-1}(\phi_1\diam{a}\phi_2)$. By Def.~\ref{def:decomposition}.\ref{dec1},
$\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}\phi_2)$. By induction,
$\chi_1(x),\chi_2(x)\in\IO{rb}^\equiv$. Hence $\psi(x)\in\IO{rb}^\equiv$. \qed
\end{itemize}
\end{proof}

\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 branching bisimulation format, with respect to some $\aleph$.
If $\sigma(x) \bis{b} \sigma'(x)$ for $x \!\in\! \var(t)$, then $\sigma(t) \bis{b} \sigma'(t)$.
\end{lemma}

\begin{proof}
By Thm.~\ref{thm:characterisation}, $\sigma(x) \bis{b} \sigma'(x)$
 implies $\sigma(x) \sim_{\IO{b}^\equiv} \sigma'(x)$ for $x \in \var(t)$.
Let $\sigma(t)\models\phi \in \IO{b}$. 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:rbrab-rbrab}, $\psi(x) \in
 \IO{b}^\equiv$ for $x\in\var(t)$. Since $\sigma(x)
 \sim_{\IO{b}^\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{b}$ implies $\sigma(t)\models\phi$. So $\sigma(t) \sim_{\IO{b}} \sigma'(t)$. Hence $\sigma(t) \bis{b} \sigma'(t)$. \qed
\end{proof}

\begin{theorem}\label{thm:congruence1}
Given a complete TSS $P=(\Sigma,R)$ in branching bisimulation format, with respect to some $\aleph$.
If $\sigma(x) \bis{b} \sigma'(x)$ for $x \!\in\! \var(t)$, then $\sigma(t) \bis{b} \sigma'(t)$.
\end{theorem}

\begin{proof}
Let $P'$ be obtained from $P$, by changing in all rules, expect the
$\aleph$-patience rules, conclusions 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 branching bisimulation format
with respect to $\aleph$. So by Lem.~\ref{lem:congruence1}, $\bis{b}$ 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 and trivial to check that $\bis{b}$
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{b}$ is a congruence for $\tau_i \circ f$ in $P''$, it
must be a congruence for $f$ in $P$. \qed
\end{proof}

\begin{lemma}\label{lem:congruence2}
Given a complete, abstraction-free TSS in rooted branching bisimulation format,
with respect to some $\aleph$ and $\Lambda$.
If $\sigma(x) \bis{rb} \sigma'(x)$ for $x \!\in\! \var(t)$, then $\sigma(t) \bis{rb} \sigma'(t)$.
\end{lemma}

\begin{theorem}\label{thm:congruence2}
Given a complete TSS in rooted branching bisimulation format,
with respect to some $\aleph$ and $\Lambda$.
If $\sigma(x) \bis{rb} \sigma'\hspace{-0.26184pt}(x)$ for $x\!\in\! \var(t)$, then $\sigma(t) \bis{rb} \sigma'(t)$.
\end{theorem}
\noindent
The proof of Lem.~\ref{lem:congruence2} is similar to the one of
Lem.~\ref{lem:congruence1}, except that
Prop.~\ref{prop:rooted_bra_preservation} is applied instead of
Prop.~\ref{prop:rbrab-rbrab}.  Likewise, the proof of
Thm.~\ref{thm:congruence2} is similar to the one of
Thm.~\ref{thm:congruence1}.


\section{Applications}
\label{sec:applications}

In this section we present four applications of the rooted branching bisimulation format.

\subsection{Basic Process Algebra}
\label{sec:bpa}

Basic process algebra BPA \cite{BK84} assumes a collection ${\it Act}$ of constants,
called {\em atomic actions}, which upon execution terminate successfully.
The signature of BPA moreover includes function symbols $\_+\_$ and
$\_{\cdot}\_$ of arity two, called {\em alternative composition} and
{\em sequential composition}, respectively. Intuitively, $t_1+t_2$
executes either $t_1$ or $t_2$, while $t_1{\cdot}t_2$ first executes $t_1$
and upon successful termination executes $t_2$.
We assume a special atomic action ${\it tick}\in{\it Act}$, indicating
the activity of successful termination upon executing the internal
action $\tau$, and a special constant {\em deadlock} $\delta$,
outside ${\it Act}$, which does not display any behaviour.
These intuitions are made precise by means of the transition rules for BPA$^{\it tick}_{\delta}$ presented
below. In these rules, $\ell$ ranges over ${\it Act}$, and
$\alpha$ over $A=\{\ell,\ell_\surd\mid\ell\in{\it Act}\}$. The label $\ell_\surd$ denotes
that upon execution of $\ell$, the process terminates successfully.

\[
\begin{array}{c}
\ell\trans{\ell_\surd}\delta\hspace*{1cm}
{\displaystyle\frac{x_1\trans \alpha y}{x_1+x_2\trans \alpha y}}\hspace*{1cm}
{\displaystyle\frac{x_2\trans \alpha y}{x_1+x_2\trans \alpha y}}\\
\\
{\displaystyle\frac{x_1\trans \ell y}{x_1{\cdot}x_2\trans \ell y{\cdot}x_2}}
\hspace{1cm}
{\displaystyle\frac{x_1\trans{\ell_\surd}y}{x_1{\cdot}x_2\trans{\ell}x_2}}
\end{array}
\]

\vspace{2mm}
\noindent
The label ${\it tick}$ counts as internal action, and for this
reason the labels ${\it tick}$ and ${\it tick}_\surd$ can also be written $\tau$
and $\tau_\surd$, respectively. The label $\tau_\surd$ denotes termination and counts
as a normal observable action. When this action occurs in the first
component of a sequential composition, it changes into the internal
action $\tau$, so that this TSS is not abstraction-free.
We do not have $a \bis{rb} a{\cdot}{\it tick}$, as the former process performs one
visible action and the latter two. For this reason we call the
constant ${\it tick}$ ${\it tick}$, rather than $\tau$.

The TSS above is in rooted branching bisimulation format, if we take the arguments of
alternative composition to be $\Lambda$-frozen, the first argument of sequential
composition to be $\aleph$-liquid, and the second argument of sequential composition
to be $\aleph$-frozen. For the sake of the application to the action refinement operator,
in Sect.\ \ref{sec:refinement}, we take the second argument of sequential composition
to be $\Lambda$-liquid.

\begin{corollary}
Rooted branching bisimulation is a congruence for BPA$^{\it tick}_{\delta}$.
\end{corollary}


\subsection{Binary Kleene star}

The {\em binary Kleene star} $t_1{}^\ast t_2$ \cite{Kle56} repeatedly executes
$t_1$ until it executes $t_2$. This operational behaviour is captured by the
following rules, which are added to the rules for BPA$^{\it tick}_{\delta}$.

\[
{\displaystyle\frac{x_1\trans \ell y}{x_1{}^\ast x_2\trans \ell y{\cdot}(x_1{}^\ast x_2)}}
\hspace{1cm}{\displaystyle\frac{x_1\trans{\ell_\surd}y}{x_1{}^\ast x_2\trans{\ell}x_1{}^\ast x_2}}
\hspace{1cm}{\displaystyle\frac{x_2\trans \alpha y}{x_1{}^\ast x_2\trans \alpha y}}\\
\]

\vspace{2mm}
\noindent
The resulting TSS is in rooted branching bisimulation format, if we take the arguments
of the binary Kleene star to be $\Lambda$-frozen.

\begin{corollary}
Rooted branching bisimulation is a congruence for BPA$^{\it tick}_{\delta}$ with the binary Kleene star.
\end{corollary}


\subsection{Initial Priority}

{\em Initial priority} is a unary function symbol that assumes an ordering
on labels (which is usually defined on the level of atomic actions).
The term $\theta(t)$ executes the transitions of $t$,
with the restriction that an initial transition $t\trans \alpha t_1$ only gives
rise to an initial transition $\theta(t)\trans \alpha t_1$ if there does not exist
an initial transition $t\trans \beta t_2$ with $\alpha<\beta$. This intuition is
captured by the rule for the initial priority operator below,
which is added to the rules for BPA$^{\it tick}_{\delta}$.

\[
\frac{x\trans \alpha y~~~~x\ntrans \beta\mbox{ for } \alpha<\beta}{\theta(x)\trans \alpha y}
\]

\vspace{2mm}
\noindent
The resulting TSS is in rooted branching bisimulation format, if we take 
the argument of initial priority to be $\Lambda$-frozen.

\begin{corollary}
Rooted branching bisimulation is a congruence for BPA$^{\it tick}_{\delta}$ with initial priority.
\end{corollary}


\subsection{Action Refinement}
\label{sec:refinement}

In the previous applications, it sufficed to take $\Lambda=\aleph$. In the following example, however, this is not possible.

The binary {\em action refinement} operator $t_1[\ell\leadsto t_2]$, for
$\ell\in{\it Act}\backslash\{{\it tick}\}$, replaces each $\ell$-transition in $t_1$ by $t_2$. Its
transition rules, presented below, are added to the rules for BPA$^{\it tick}_{\delta}$.

\[
\begin{array}{c}
{\displaystyle\frac{x_1\trans \alpha y}{x_1[\ell\leadsto x_2]\trans \alpha y[\ell\leadsto x_2]}}
\hspace{5mm}(\alpha\not=\ell,\ell_\surd) \\
\\
{\displaystyle\frac{x_1\trans{\ell}y_1~~~~x_2\trans{\ell'}y_2}
{x_1[\ell\leadsto x_2]\trans{\ell'}y_2{\cdot}(y_1[\ell\leadsto x_2])}}
\hspace{1cm}
{\displaystyle\frac{x_1\trans{\ell_\surd}y_1~~~~x_2\trans{\ell'}y_2}
{x_1[\ell\leadsto x_2]\trans{\ell'}y_2}} \\
\\
{\displaystyle\frac{x_1\trans{\ell}y_1~~~~x_2\trans{\ell'_\surd}y_2}
{x_1[\ell\leadsto x_2]\trans{\ell'}y_1[\ell\leadsto x_2]}}
\hspace{1cm}
{\displaystyle\frac{x_1\trans{\ell_\surd}y_1~~~~x_2\trans{\ell'_\surd}y_2}
{x_1[\ell\leadsto x_2]\trans{\ell'_\surd}y_2}}
\end{array}
\]

\vspace{2mm}
\noindent
The resulting TSS is in rooted branching bisimulation format, if we take the first argument of action refinement to be $\aleph$-liquid and the second argument to be $\Lambda$-frozen. For the second rule to be rooted branching bisimulation safe, it is essential that the second argument of sequential composition is $\Lambda$-liquid, for else it would violate restriction 2 of Def.\ \ref{def:rooted_bra_bisimulation_safe}.

\begin{corollary}
Rooted branching bisimulation is a congruence for BPA$^{\it tick}_{\delta}$ with action refinement.
\end{corollary}


\section{Counterexamples}

This section presents a series of counterexamples of complete TSSs in ntyft/ntyxt format, to show that none of the syntactic restrictions of our congruence formats can be omitted. (Of course it remains possible that certain restrictions can be refined.) In \cite{GV92} a series of counterexamples can be found showing that the syntactic restrictions of the ntyft/ntyxt format are essential as well. Furthermore, in \cite{BolG96} a counterexample is given to show that completeness (there called positive after reduction) is essential.

It is well-known that branching bisimulation is not a congruence for BPA$^{\it tick}_\delta$. For instance, $a\bis{b}{\it tick}{\cdot}a$, but $a+c\notbis{b}({\it tick}{\cdot}a)+c$. Still we saw in Sect.~\ref{sec:bpa} that the TSS for this process algebra is in rooted branching bisimulation format. This shows that universality of the predicate $\Lambda$ cannot be omitted from the branching bisimulation format.

The examples in this section assume an action set $A=\{a,b,c\}$ and a TSS $P=\{\Sigma,R\}$, where the signature $\Sigma$ contains the constant $0$ and unary function symbols $\alpha\_$ for $\alpha\in A\cup\{\tau\}$, and $R$ contains the rules \plat{$\alpha x\trans\alpha x$} for $\alpha\in A\cup\{\tau\}$. The argument of $\alpha\_$ is $\aleph$-frozen. Unlike before, in this section occurrences of $a,b,c$ as labels in rules are explicit action names, instead of parameters ranging over $A$.

\begin{example}
We extend $P$ with the following rule:
$$\frac{x\trans a y\quad y\trans b z}{f(x)\trans{c}0}$$
The rule above is not rooted branching bisimulation safe, because it contains lookahead, violating restriction 1 (of Def.\ \ref{def:rooted_bra_bisimulation_safe}). Clearly, $ab0\bis{rb}a\tau b0$ (and thus $ab0\bis{b}a\tau b0$). However, $f(ab0)\notbis{b}f(a\tau b0)$ (and thus $f(ab0)\notbis{rb}f(a\tau b0)$), since $f(ab0)\trans{c}0$, while $f(a\tau b0)\ntrans\alpha$ for $\alpha\in\{c,\tau\}$.
\end{example}

\begin{example}
We extend $P$ with the following rule:
$$\frac{x\trans a y}{f(x)\trans a f(y)}$$
The argument of $f$ must be $\aleph$-frozen, in view of the restriction in Def.\ \ref{def:bra_bisimulation_format} that for each $\aleph$-liquid argument there is an $\aleph$-patience rule. The rule above is not rooted branching bisimulation safe. Namely, if the argument of $f$ is $\Lambda$-frozen, then $y$ occurs both as the right-hand side of a premise and $\Lambda$-frozen in the right-hand side of the conclusion, violating restriction 2. And if the argument of $f$ is $\Lambda$-liquid, then $x$ occurs $\Lambda$-liquid and $\aleph$-frozen in the source and $\aleph$-liquid in the left-hand side of the premise, violating restriction 3(d). We have $f(aa0)\notbis{b}f(a\tau a0)$, since $f(aa0)\trans a f(a0)\trans a f(0)$, while $f(a\tau a0)$ can only do an $a$-transition to $f(\tau a0)$, and $f(\tau a0)\ntrans\alpha$ for $\alpha\in\{a,\tau\}$.
\end{example}

\begin{example}
We extend $P$ with the following rules:
$$\frac{x\trans\tau y}{f(x)\trans\tau f(y)}\qquad\frac{x\trans a y}{f(x)\trans a f(y)}\qquad\frac{x\ntrans a}{f(x)\trans c 0}$$
The argument of $f$ has to be $\Lambda$-liquid, for else the first and second rule would violate restriction 2. It even has to be $\aleph$-liquid, for otherwise these rules would violate requirement 3(d). However, with the argument of $f$ $\aleph$-liquid, the third rule is not rooted branching bisimulation safe, because $x$ occurs $\aleph$-liquid both in the source and in the left-hand side of the negative premise, violating restriction 3(b). We have $f(aa0)\notbis{b}f(a\tau a0)$, since $f(a\tau a0)\trans a f(\tau a0)\trans c 0$, while $f(aa0)$ can only do an $a$-transition to $f(a0)$, and $f(a0)\ntrans\alpha$ for $\alpha\in\{c,\tau\}$.
\end{example}

\begin{example}
We extend $P$ with the following rules:
$$\frac{x\trans\tau y}{f(x)\trans\tau f(y)}\qquad\frac{x\trans a y}{f(x)\trans a f(y)}\qquad\frac{x\trans\tau y}{f(x)\trans c 0}$$
As in the previous example, the argument of $f$ has to be $\aleph$-liquid. The third rule is not rooted branching bisimulation safe, because $x$ occurs $\aleph$-liquid both in the source and in the left-hand side of the positive premise with label $\tau$, violating restriction 3(c). We have $f(aa0)\notbis{b}f(a\tau a0)$, since $f(a\tau a0)\trans a f(\tau a0) \trans c 0$, while $f(aa0)$ can only do an $a$-transition to $f(a0)$, and $f(a0)\ntrans\alpha$ for $\alpha\in\{c,\tau\}$.
\end{example}

\begin{example}\label{ex:4}
We extend $P$ with the following rules: 
$$\eta\trans a 0\qquad\zeta\trans b 0\qquad\eta\trans\tau\zeta\qquad\zeta\trans\tau\eta\qquad
\nu\trans a 0\qquad\nu\trans b 0$$
$$\frac{x\trans\tau y}{f(x)\trans\tau f(y)}\qquad\frac{x\trans a y\quad x\trans b z}{f(x)\trans c 0}$$
Again, the argument of $f$ is $\aleph$-liquid. The last rule is not rooted branching bisimulation safe, because $x$ has an $\aleph$-liquid occurrence in the source, and two $\aleph$-liquid occurrences in the left-hand sides of the premises, violating restriction 3(c). Clearly, $\tau\nu\bis{rb}\tau\eta$. However, $f(\tau\nu)\notbis{b}f(\tau\eta)$, since $f(\tau\nu)\trans\tau f(\nu)\trans c 0$, while $f(\tau\eta)$ only exhibits an infinite sequence of $\tau$-transitions: $f(\tau\eta)\trans\tau f(\eta)\trans\tau f(\zeta)\trans\tau f(\eta)\trans\tau\cdots$.
\end{example}

\begin{example}
In the TSS from Example \ref{ex:4}, we replace the last rule with the following rules:
$$f(x)\trans\tau g(x)\qquad \frac{x\trans a y\quad x\trans b z}{g(x)\trans c 0}$$
The argument of $f$ is again $\aleph$-liquid, and the argument of $g$ must be $\Lambda$-frozen, as otherwise the second rule would violate restriction 3(c). The first rule above is not rooted branching bisimulation safe, because $x$ occurs $\aleph$-liquid (hence $\Lambda$-liquid) in the source and $\Lambda$-frozen in the right-hand side of the conclusion, violating restriction 3(a). We have $f(\tau\nu)\notbis{b}f(\tau\eta)$, since $f(\tau\nu)\trans\tau f(\nu)\trans\tau g(\nu)\trans c 0$, while $f(\tau\eta)$ can only perform $\tau$-transitions.
\end{example}

\begin{example}
In the TSS from Example \ref{ex:4}, we replace the last rule with the following rules:
$$\frac{x\trans a y\quad x\trans b z}{g(x)\trans c 0}\qquad\frac{g(x)\trans c y}{f(x)\trans c 0}$$
As in the previous example, the argument of $f$ must be $\aleph$-liquid, and the argument of $g$ $\Lambda$-frozen. The last rule above is not rooted branching bisimulation safe, because $x$ occurs $\aleph$-liquid in the source and $\Lambda$-frozen in the left-hand side of the premise, violating restriction 3(a). We have $f(\tau\nu)\notbis{b}f(\tau\eta)$, since $f(\tau\nu)\trans\tau f(\nu)\trans c 0$, while $f(\tau\eta)$ can only perform $\tau$-transitions.
\end{example}


\section{Related Work}
\label{sec:related}

The first congruence formats for branching and rooted branching bisimulation were presented in \cite{Blo95}, and reformulated in \cite{vGl05}. Those formats, which are contained in the GSOS format \cite{BIM95}, 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{Blo95,vGl05}. However, our formats generalise the result of simplifying the formats of \cite{Blo95,vGl05} by requiring all operators to be principal.

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

The format of \cite{Blo95,vGl05} for rooted branching bisimulation 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}.

In \cite{Fok00} a format for rooted branching bisimulation was proposed that generalises the simplified format of \cite{Blo95,vGl05}. Given that it applies to TSSs with predicates, it is incomparable with our current rooted branching bisimulation format. However, predicates can easily be encoded in terms of transitions, and when disregarding predicates, our current format is more general than the format of \cite{Fok00}. Still, the format of \cite{Fok00} strictly contains the intersection of our format with the GSOS format, and all applications of our work discussed in Sect.\ \ref{sec:applications} fall within that intersection.

In \cite{FvGdW05} we apply the techniques of the current paper to derive congruence formats for $\eta$- and rooted $\eta$-bisimulation. These formats differ from the ones of the current paper only in restriction 2 of Def.\ \ref{def:rooted_bra_bisimulation_safe}. There it is required that right-hand sides of premises occur only $\aleph$-liquid in $u$, whereas here we merely require $\Lambda$-liquidity. That the rooted branching bisimulation format is essentially more general than the rooted $\eta$-bisimulation format is illustrated by the action refinement example of Sec.\ \ref{sec:refinement}. BPA$^{\it tick}_{\delta}$ with action refinement falls outside the rooted $\eta$-bisimulation format, due to the fact that the second argument of sequential composition needs to be $\aleph$-liquid in order for the second action refinement rule to be rooted $\eta$-bisimulation safe. Indeed, this operator fails to be compositional for rooted $\eta$-bisimulation \cite{GlWe96}.


\bibliographystyle{plain}
\begin{thebibliography}{10}

\bibitem{BK84}
{\sc J.A. Bergstra \& J.W. Klop} (1984):
\newblock {\em Process algebra for synchronous communication.}
\newblock {\sl Information and Control} 60(1/3), pp. 109--137.

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

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

\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{BolG96}
{\sc R.N. Bol \& J.F. Groote} (1996):
\newblock {\em The meaning of negative premises in transition system specifications.}
\newblock {\sl Journal of the ACM} 43(5), pp. 863--914.

\bibitem{DNVa95}
{\sc R. De Nicola \& F.W. Vaandrager} (1995):
\newblock {\em Three logics for branching bisimulation.}
\newblock {\sl Journal of the ACM} 42(2), pp. 458--487.

\bibitem{Fok00}
{\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{FvG96}
{\sc W.J. Fokkink \& R.J.~van Glabbeek} (1996):
\newblock {\em Ntyft/ntyxt rules reduce to ntree rules.}
\newblock {\sl Information and Computation} 126(1), pp. 1--10.

\bibitem{FvGdW03}
{\sc W.J. Fokkink, R.J.~van Glabbeek \& P.~de Wind} (2006):
\newblock {\em Compositionality of {H}ennessy-{M}ilner logic by structural operational semantics.}
\newblock {\sl Theoretical Computer Science} 354(3), pp.\ 421--440.
% \newblock Extended abstract appeared in: {\sl Proc.\ FCT'03}, LNCS 2751, Springer, 2003, pp.\ 412--422.

\bibitem{FvGdW05}
{\sc W.J. Fokkink, R.J.~van Glabbeek \& P.~de Wind} (2005):
\newblock {\em Divide and congruence applied to $\eta$-bisimulation.}
\newblock In {\sl Proc.\ SOS'05}, To appear, ENTCS. Elsevier.

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

\bibitem{vGl04}
{\sc R.J. van Glabbeek} (2004):
\newblock {\em The meaning of negative premises in transition system specifications {II}.}
\newblock {\sl Journal of Logic and Algebraic Programming} 60/61, pp. 229--258.

\bibitem{vGl05}
{\sc R.J.~van Glabbeek} (2005):
\newblock {\em On cool congruence formats for weak bisimulations (extended abstract).}
\newblock In {\sl Proc.\ ICTAC'05}, LNCS 3722, pp.\ 331--346. Springer.

\bibitem{GlWe96}
{\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{Gro93}
{\sc J.F. Groote} (1993):
\newblock {\em Transition system specifications with negative premises.}
\newblock {\sl Theoretical Computer Science} 118(2), pp. 263--299.

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

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

\bibitem{Kle56}
{\sc S.C. Kleene}:
\newblock {\em Representation of events in nerve nets and finite automata.}
\newblock In (C.~Shannon and J.~McCarthy, eds.) {\sl Automata Studies}, pp.\ 3--41.
\newblock Princeton University Press, 1956.

\bibitem{LL91}
{\sc K.G. Larsen \& X.~Liu} (1991):
\newblock {\em Compositionality through an operational semantics of contexts.}
\newblock {\sl Journal of Logic and Computation} 1(6), pp. 761--795.

\bibitem{Plo04}
{\sc G.D. Plotkin} (2004):
\newblock {\em A structural approach to operational semantics.}
\newblock {\sl Journal of Logic and Algebraic Programming} 60/61, pp. 17--139.
\newblock Originally appeared in 1981.

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

\end{thebibliography}

\appendix

\section{Modal Characterisation of Branching Bisimulation}

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

\begin{proof}
($\Rightarrow$) Suppose $p\bis{b}q$, and $p\models\phi$ for some $\phi\in\IO{b}$. We prove $q\models\phi$, by structural induction on $\phi$. The reverse implication ($q\models\phi$ implies $p\models\phi$) 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_1\diam{\hat\tau}\phi_2)$. Then for some $n$ there are $p_0,\ldots,p_n\in\mathds{P}$ with $p_0=p$, \plat{$p_i\trans{\tau}p_{i+1}$} for $i\in\{0,\ldots,n-1\}$, and $p_n\models\phi_1\diam{\hat\tau}\phi_2$. We apply induction on $n$.
\begin{description}
\item
[$\boldsymbol{n=0}$] Then $p\models\phi_1$, so by induction on formula size, $q\models\phi_1$. Furthermore, either (1) $p\models\phi_2$ or (2) there is a $p'\in\mathds{P}$ with \plat{$p\trans{\tau}p'$} and $p'\models\phi_2$. In case (1), by induction on formula size, $q\models\phi_2$, so $q\models\eps(\phi_1\diam{\hat\tau}\phi_2)$. In case (2), since $p\bis{b}q$, by Def.~\ref{def:bb} either (2.1) $p'\bis{b}q$ or (2.2) \plat{$q\epsarrow q'\trans{\tau}q''$} with $p\bis{b}q'$ and $p'\bis{b}q''$. In case (2.1), by induction on formula size, $q\models\phi_2$. In case (2.2), by induction on formula size, $q'\models\phi_1$ and $q''\models\phi_2$. In both cases, $q\models\eps(\phi_1\diam{\hat\tau}\phi_2)$.
\item
[$\boldsymbol{n>0}$] Since \plat{$p\trans{\tau}p_1$}, and $p\bis{b}q$, according to Def.~\ref{def:bb} there are two possibilities.
\begin{enumerate}
\item
Either $p_1\bis{b}q$. Since $p_1\models\eps(\phi_1\diam{\hat\tau}\phi_2)$, by induction on $n$, $q\models\eps(\phi_1\diam{\hat\tau}\phi_2)$.
\item
Or \plat{$q\epsarrow q'\trans{\tau}q''$} with $p_1\bis{b}q''$. Since $p_1\models\eps(\phi_1\diam{\hat\tau}\phi_2)$, by induction on $n$, $q''\models\eps(\phi_1\diam{\hat\tau}\phi_2)$. Hence $q\models\eps(\phi_1\diam{\hat\tau}\phi_2)$.
\end{enumerate}
\end{description}
\item
$\phi=\eps(\phi_1\diam{a}\phi_2)$. Then for some $n$ there are $p_0,\ldots,p_n\in\mathds{P}$ with $p_0=p$, \plat{$p_i\trans{\tau}p_{i+1}$} for $i\in\{0,\ldots,n-1\}$, and $p_n\models\phi_1\diam{a}\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 \plat{$p\trans{a}p'$} and $p'\models\phi_2$. Since $p\bis{b}q$, by Def.~\ref{def:bb} \plat{$q\epsarrow q'\trans{a}q''$} with $p\bis{b}q'$ and $p'\bis{b}q''$. By induction on formula size, $q'\models\phi_1$ and $q''\models\phi_2$. Hence $q\models\eps(\phi_1\diam{a}\phi_2)$.
\item
[$\boldsymbol{n>0}$] Since \plat{$p\trans{\tau}p_1$}, and $p\bis{b}q$, according to Def.~\ref{def:bb} there are two possibilities.
\begin{enumerate}
\item
Either $p_1\bis{b}q$. Since $p_1\models\eps(\phi_1\diam{a}\phi_2)$, by induction on $n$, $q\models\eps(\phi_1\diam{a}\phi_2)$.
\item
Or \plat{$q\epsarrow q'\trans{\tau}q''$} with $p_1\bis{b}q''$. Since $p_1\models\eps(\phi_1\diam{a}\phi_2)$, by induction on $n$, $q''\models\eps(\phi_1\diam{a}\phi_2)$. Hence $q\models\eps(\phi_1\diam{a}\phi_2)$.
\end{enumerate}
\end{description}
\end{itemize}
We conclude that $p\sim_{\IO{b}}q$.

\vspace{2mm}
\noindent
($\Leftarrow$)
We prove that $\sim_{\IO{b}}$ is a branching bisimulation relation. The relation is clearly symmetric. Let $p\sim_{\IO{b}}q$. Suppose \plat{$p\trans{\alpha}p'$}. If $\alpha=\tau$ and $p'\sim_{\IO{b}}q$, then the first condition of Def.~\ref{def:bb} is fulfilled. So we can assume that either (i) $\alpha\not=\tau$ or (ii) $p'\not\sim_{\IO{b}}q$. We define two sets:
\[
\begin{array}{lcl}
Q' &=& \{q'\in\mathds{P}\mid q\epsarrow q'\wedge p\not\sim_{\IO{b}}q'\} \\
Q'' &=& \{q''\in\mathds{P}\mid\exists q'\in\mathds{P}:q\epsarrow q'\trans\alpha q''\wedge p'\not\sim_{\IO{b}}q''\}
\end{array}
\]
For each $q'\in Q'$, let $\phi_{q'}$ be a formula in $\IO{b}$ such that $p\models\phi_{q'}$ and $q'\not\models\phi_{q'}$. (Such a formula always exists because $\IO{b}$ 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{b}$ 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{b}$, $p\models\phi$ and $p'\models\psi$. We distinguish two cases.
\begin{enumerate}
\item
$\alpha\not=\tau$. Since $p\models\eps(\phi\diam\alpha\psi)\in\!\IO{b}$ and $p\!\sim_{\IO{b}}\! q$, also $q\models\eps(\phi\diam\alpha\psi)$. Hence \plat{$q\epsarrow q'\trans\alpha q''$} with $q'\models\phi$ and $q''\models\psi$. By the definition of $\phi$ and $\psi$ it follows that $p\sim_{\IO{b}}q'$ and $p'\sim_{\IO{b}}q''$.
\item
$\alpha=\tau$ and $p'\not\sim_{\IO{b}}q$. Let $\tilde\phi\in\IO{b}$ such that $p'\models\tilde\phi$ and $p,q\not\models\tilde\phi$. Since $p\models\eps(\phi\diam{\hat\tau}(\tilde\phi\wedge\psi))\in\IO{b}$ and $p\sim_{\IO{b}}q$, also $q\models\eps(\phi\diam{\hat\tau}(\tilde\phi\wedge\psi))$. So \plat{$q\epsarrow q'$} with $q'\models\phi\diam{\hat\tau}(\tilde\phi\wedge\psi)$. By definition of $\phi$ it follows that $p\sim_{\IO{b}}q'$. Thus $q'\not\models\tilde\phi$, so $q'\trans\tau q''$ with $q''\models\tilde\phi\wedge\psi$. By the definition of $\psi$ it follows that $p'\sim_{\IO{b}}q''$.
\end{enumerate}
Both cases imply that the second condition of Def.~\ref{def:bb} is fulfilled. We therefore conclude that $\sim_{\IO{b}}$ is a branching bisimulation relation. \qed
\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{rb}$ is a modal characterisation of rooted branching bisimulation equivalence.

\end{document}
