\documentclass[10pt,nonatbib,reprint]{sigplanconf}
\newfont{\fsc}{eusm10}
\usepackage{amsmath}
\usepackage{hyperref}
\usepackage{theorem}\theorembodyfont{\rmfamily}
\usepackage{url}
\usepackage{amsmath} % \boldsymbol
\usepackage{dsfont}
\usepackage{epsfig}
\usepackage{amssymb}
\usepackage{color}

\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}} % no vertical space
\newcommand{\nietplat}[1]{#1} % wel 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]{\mathbb{O}_{#1}}
\renewcommand{\phi}{\varphi}
\newcommand{\Red}[1]{\textcolor{red}{#1}}
\newcommand{\Brac}[1]{[#1]}
\newcounter{saveenumi}
\newcommand{\valuation}{closed substitution}
\newcommand{\aL}{\aleph\,\mathord\cap\Lambda}

\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{example}{Example}
\newtheorem{remark}{Remark}

\newenvironment{proof}[1][Proof]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}

\newcommand{\qed}{\nobreak \ifvmode \relax \else
      \ifdim\lastskip<1.5em \hskip-\lastskip
      \hskip1.5em plus0em minus0.5em \fi \nobreak
      \vrule height0.75em width0.5em depth0.25em\fi}

\toappear{\small NICTA is funded by the Australian Government
    through the Department of Communications and the Australian
    Research Council through the ICT Centre of Excellence
    Program.\vspace{2ex}

In: \href{http://dx.doi.org/10.1145/2933575.2933590}{Proc. LICS 2016, pp.\ 778--787}.}

\makeatletter
\def \@copyrightspace {%
  \@float{copyrightbox}[b]%
  \vbox to 1in{%
    \vfill
    \parbox[b]{20pc}{%
      \tiny
      \if \@preprint
        [Copyright notice will appear here
         once 'preprint' option is removed.]\par
      \else
        \@toappear
      \fi}}%
  \end@float}
\makeatother

\begin{document}


\title{Divide and Congruence II: Delay and Weak Bisimilarity}

\authorinfo{Wan Fokkink}
{Vrije Universiteit Amsterdam, The Netherlands}
{w.j.fokkink@vu.nl}
\authorinfo{Rob van Glabbeek}
{NICTA/Data61, CSIRO, Sydney, Australia\newline
University of New South Wales, Sydney, Australia}
{rvg@cs.stanford.edu}

\date{}
\maketitle

\begin{abstract}
{\small
Earlier we presented a method to decompose modal formulas for processes with the internal action $\tau$; congruence formats for branching and $\eta$-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that formulas in the modal characterisation of this semantics are always decomposed into formulas in this modal characterisation. Here the decomposition method is enhanced to deal with modal characterisations that contain a modality $\eps\diam{a}\phi$, to derive congruence formats for delay and weak bisimilarity.
}
\end{abstract}


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

In \cite{BFvG04} a method was developed to generate congruence formats for (concrete) process semantics from their modal characterisation. It crosses the borders between process algebra, structural operational semantics, process semantics, and modal logic. Cornerstone is the work in \cite{LL91} to decompose formulas from Hennessy-Milner logic \cite{HM85} with respect to a structural operational semantics in the De Simone format \cite{Sim85}. It was extended to the ntyft format \cite{Gro93} without lookahead in \cite{BFvG04}, and to the tyft format \cite{GV92} in \cite{FvGdW03}.

An equivalence is a congruence for a term algebra if the equivalence class of any term $f(p_1,\ldots,p_n)$ is determined by the equivalence classes of $p_1,\ldots,p_n$. Being a congruence is an important property, e.g.\ to fit a process semantics into an axiomatic framework. Syntactic formats for structural operational semantics have been developed for several process semantics, to ensure that such a semantics is a congruence; notably for unrooted and rooted weak bisimilarity in \cite{Blo95} and for unrooted and rooted delay bisimilarity in \cite{vGl11}.

Key idea in \cite{BFvG04} is that a congruence format for a process semantics must ensure that the formulas in a modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. This yielded liberal and elegant congruence formats for all known concrete process semantics in a convenient way. In \cite{FvGdW12} this method was extended to weak process semantics, which take into account the internal action $\tau$. As a result, congruence formats for rooted branching and $\eta$-bisimilarity were derived. Two predicates $\aleph$ and $\Lambda$ on arguments of function symbols are used: $\aleph$ marks processes that can execute immediately, and $\Lambda$ processes that have started executing. Formats for unrooted branching and $\eta$-bisimilarity are obtained by imposing one restriction on top of the format for the corresponding rooted semantics: $\Lambda$ holds universally.

The framework from \cite{FvGdW12} covers only a small part of the spectrum of weak semantics \cite{vGl93}. In particular, it does not readily extend to delay and weak bisimilarity \cite{Mil81,Mil89}. The reason is that in these semantics, in contrast to branching and $\eta$-bisimilarity, a process $q$ that mimics an $a$-transition from a process $p$, does not need to be related to $p$ at the moment that $q$ performs the $a$-transition. This implies that in the modal characterisation of delay and weak bisimilarity, a modality $\diam{a}\phi$ stating that an $a$-transition to a process where $\phi$ holds, is always preceded by a modality $\eps$ allowing any number of $\tau$-transitions. As a consequence, devising congruence formats for delay and weak bisimilarity is notoriously difficult, see e.g.\ \cite{Blo95,vGl11}. Here we show how this technical obstacle can be overcome by the semantic notion \emph{delay resistance}, which ensures that modalities $\eps\diam{a}\phi$ are decomposed into formulas that again have this form. Thus congruence formats can be derived for semantics with a modal characterisation containing such modalities. We derive congruence formats for rooted delay and weak bisimilarity. Congruence formats for the unrooted counterparts of these semantics are again obtained by the extra requirement that $\Lambda$ is universal.

We moreover provide syntactic restrictions which imply delay resistance, leading to the first entirely syntactic congruence formats for rooted delay and weak bisimilarity. The congruence formats we obtain are more liberal and elegant than existing congruence formats for these semantics. In particular, in \cite{Blo95} it is stated that the RWB format put forward in that paper has a ``horrible definition'', and that ``negative rules seem incompatible with weak process equivalences.'' Here we show how negative premises can be included in congruence formats for rooted delay and weak bisimilarity.



\section{Preliminaries}
\label{sec:preliminaries}


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

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

Processes can be distinguished by a wide range of semantics, based on e.g.\ branching structure or decorated execution sequences. Weak semantics, classified in \cite{vGl93}, abstract away from $\tau$'s to different degrees. Here we focus on the two weak semantics that are employed most often: delay bisimilarity \cite{Mil81} and weak bisimilarity \cite{Mil89}.

\begin{definition}\label{def:bb}
{\rm
Let $B\subseteq\mathbb{P}\times\mathbb{P}$ be a symmetric relation.
\begin{itemize}
\item
$B$ is a \emph{delay bisimulation} if $pBq$ and \nietplat{$p\trans{\alpha}p'$} implies that either $\alpha = \tau$ and $p'\,B\,q$, or \nietplat{$q\epsarrow \trans{\alpha} q''$} for some $q''$ with $p'Bq''$.
Processes $p,q$ are {\em delay bisimilar}, denoted $p\bis{d}q$, if there exists a delay bisimulation $B$ with $pBq$.

\item
$B$ is a \emph{weak bisimulation} if $pBq$ and \nietplat{$p\trans{\alpha}p'$} implies that either $\alpha = \tau$ and $p'\,B\,q$, or \nietplat{$q\epsarrow \trans{\alpha} \epsarrow q''$} for some $q''$ with $p'Bq''$.
Processes $p,q$ are {\em weakly bisimilar}, denoted $p\bis{w}q$, if there exists a weak bisimulation $B$ with $pBq$.
\end{itemize}
}
\end{definition}
$\bis{d}$ and $\bis{w}$ are equivalence relations. However, they are not congruences for most process algebras. Rooted variants of these semantics, which require for the pair of initial states that a $\tau$-transition needs to be matched by at least one $\tau$-transition, are congruences for basic process algebras, notably for the alternative composition operator.

\begin{definition}\label{def:rbb}
{\rm
Let $R\subseteq\mathbb{P}\times\mathbb{P}$ be a symmetric relation.
\begin{itemize}
\item
$R$ is a \emph{rooted delay bisimulation} if $pRq$ and \nietplat{$p \trans{\alpha} p'$} implies that \nietplat{$q \epsarrow\trans{\alpha}q '$} for some $q'$ with $p'\bis{d}q'$.

Processes $p,q$ are \emph{rooted delay bisimilar},
$p\bis{rd}q$, if there exists a rooted delay bisimulation $R$ with $pRq$.

\item
$R$ is a \emph{rooted weak bisimulation} if $pRq$ and \nietplat{$p \!\trans{\alpha}\! p'$} implies that \nietplat{$q \!\epsarrow\trans{\alpha}\epsarrow\! q '$} for some $q'$ with $p'\bis{w}q'$.

Processes $p,q$ are \emph{rooted weakly bisimilar},
$p\bis{rw}q$, if there exists a rooted weak bisimulation $R$ with $pRq$.
\end{itemize}
}
\end{definition}

\begin{example}\label{ex:weak bisimulations}
Processes $p_0$ and $p_1$ in the LTS below are rooted delay bisimilar but not $\eta$-bisimilar.
In an $\eta$-bisimulation the transition $p_0\trans{b}0$ cannot be mimicked by $p_1$; the only candidate $p_1\trans{\tau}q\trans{b}0$ fails because
$q$ cannot be related to $p_0$, while this would be required for an $\eta$-bisimulation.

\vspace{2mm}

\centerline{\input{delay-not-eta-small.pdf_t}}

\end{example}


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

Hennessy-Milner logic \cite{HM85} is extended with the modal connective $\eps\phi$, expressing that a process can perform zero or more $\tau$-transitions to a state where $\phi$ holds.

\begin{definition}\label{def:formulas}
{\rm\cite{vGl93}
The class $\mathbb{O}$ of \emph{modal formulas} is defined as follows, where $I$ ranges over all index sets:
\[
\mathbb{O} \qquad \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \diam{\alpha}\phi ~|~ \eps\phi\enspace .
\]
}
\end{definition}

\noindent
$p\models\phi$ denotes that $p$ satisfies $\phi$. By definition, $p\models\diam{\alpha}\phi$ if
\nietplat{$p\trans{\alpha}p'$} for some $p'$ with $p'\models\phi$, and $p\models\eps\phi$ if
\nietplat{$p\epsarrow p'$} for some $p'$ with $p'\models\phi$. We use abbreviations $\top$ for the empty
conjunction and $\phi_1\land\phi_2$ for $\bigwedge_{i\in\{1,2\}}\phi_i$.
We write $\phi\equiv\phi'$ if $p\models\phi\Leftrightarrow
p\models\phi'$ for any process $p$ in any LTS.

A modal characterisation of an equivalence on processes consists of a class $C$ of modal formulas such that two processes are equivalent if and only if they satisfy the same formulas in $C$. Hennessy-Milner logic is a modal characterisation of bisimilarity. We now introduce modal characterisations for (unrooted and rooted) delay and weak bisimilarity.

\begin{definition}\label{def:modal-characterisations}
{\rm
Let $a$ range over $A$ and $\alpha$ over $A\cup\{\tau\}$.
The subclasses $\IO{e}$ and $\IO{re}$ of $\mathbb{O}$, for $e\in\{d,w\}$, are defined by:
\begin{align*}
&\IO{d}       && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \eps\phi ~|~ \eps\diam{a}\phi \\
&\IO{rd}      && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \eps\diam{\alpha}\hat\phi ~|~ \hat\phi ~(\hat\phi\in\IO{d}) \\
&\IO{w}       && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \eps\phi ~|~ \eps\diam{a}\eps\phi \\
&\IO{rw}      && \phi ::= \mbox{$\bigwedge$}_{i\in I}\phi_i ~|~ \neg\phi ~|~ \eps\diam{\alpha}\eps\hat\phi ~|~ \hat\phi ~(\hat\phi\in\IO{w}).
\end{align*}
}
\end{definition}

\noindent
For $L\subseteq\mathbb{O}$, we write $p\sim_L q$ if $p$ and $q$ satisfy the same formulas in $L$.
The class $L^\equiv$ denotes the closure of $L$ under $\equiv$.
Trivially, $p\sim_{L}q \Leftrightarrow p\sim_{L^\equiv}q$.

\begin{theorem}\label{thm:characterisation}
$p\bis{e}q\Leftrightarrow p\sim_{\IO{e}}q$ and $p\bis{re}q\Leftrightarrow p\sim_{\IO{re}}q$, for all $p,q\in\mathbb{P}$, where $e\in\{d,w\}$.
\end{theorem}


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

A \emph{signature} is a set $\Sigma$ of function symbols $f$ with arity $\ar(f)$.
Let $V$ be an infinite set of variables $x,y,z$, with $|\Sigma|, |A| \leq |V|$.
A syntactic object is {\em closed} if it does not contain any variables.
The set $\mathbb{T}(\Sigma)$ of terms over $\Sigma$ and $V$ is defined as
usual; $t,u,v,w$ denote terms and $\var(t)$ is the set of variables
that occur in term $t$.
A term is {\em univariate} if it is without multiple occurrences of the same variable.
 A substitution $\sigma$ is a partial function
from $V$ to $\mathbb{T}(\Sigma)$. A closed substitution is a total
function from $V$ to closed terms.

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

\begin{definition}\label{def:TSS}\rm
A (\emph{positive} or \emph{negative}) \emph{literal} is an expression
\nietplat{$t \trans\alpha u$} or \nietplat{$t\ntrans\alpha$}. A
\emph{(transition) rule} is of the form $\frac{H}{\lambda}$ with $H$ a
set of literals called the \emph{premises}, and $\lambda$ a literal
called the \emph{conclusion}; the term at the left-hand
side of $\lambda$ is called the \emph{source}.
$H^+$ denotes the positive premises and $H^{s-}$ the \emph{stable}
negative premises in $H$: those \nietplat{$t \ntrans\alpha$} for which
also $t \ntrans\tau$ is in $H$.
A rule $\frac{\emptyset}{\lambda}$ is also written $\lambda$.
A rule is {\em standard} if it has a positive conclusion.
A {\em transition system specification (TSS)}
consists of a signature $\Sigma$ and a set $R$ of rules over $\Sigma$.
A TSS is {\em standard} if all its rules are.
\end{definition}

\begin{definition}\label{def:proof}
{\rm
Let $P=(\Sigma,R)$ be a TSS. An {\em irredundant proof} from $P$ of a rule $\frac{H}{\lambda}$ is a well-founded tree with the nodes labelled by literals and some of the leaves marked ``hypothesis'', such that the root has label $\lambda$, $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 $\frac{K}{\mu}$ is a substitution instance of a rule in $R$.
}
\end{definition}
\noindent
The proof of $\frac{H}{\lambda}$ is called irredundant \cite{BFvG04} because $H$ must equal (instead of include)
the set of labels of the hypotheses. Irredundancy is crucial for the preservation under provability of our congruence formats.
Namely, in a `redundant' proof one can freely add any premises to the derived rule.

Literals \nietplat{$t \trans{\alpha} u$} and \nietplat{$t\ntrans{\alpha}$} are said to \emph{deny} each other.

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

\subsection{Syntactic restrictions on transition rules}\label{sec:ntytt}

We present terminology for syntactic restrictions on rules
from \cite{BFvG04,Gro93,GV92}.
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. An \emph{xynft rule} is ntyft and the left-hand sides of its positive premises are variables.

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 \emph{decent} rule has no lookahead and no free variables.
A TSS in \emph{ready simulation format} consists of ntyft and ntyxt rules without lookahead.


\subsection{Patience rules}\label{sec:predicates}

Let $\Gamma$ be a unary predicate on arguments of function symbols. If $\Gamma(f,i)$, then argument $i$ of $f$ is {\em $\Gamma$-liquid}; otherwise it is {\em $\Gamma$-frozen}. An occurrence of $x$ in $t$ is {\em $\Gamma$-liquid} if $t=x$ or $t=f(t_1,\ldots,t_{\ar(f)})$ and the occurrence is $\Gamma$-liquid in $t_i$ with $\Gamma(f,i)$; otherwise the occurrence is {\em $\Gamma$-frozen}.

Sect.~\ref{sec:decomposition} presents a method for
decomposing modal formulas that gives a special treatment to arguments
of function symbols that are deemed \emph{patient}; we will use a
predicate $\Gamma$ to mark the arguments that get this special treatment.

\begin{definition}\label{def:patience_rule}
{\rm\cite{Blo95,Fok00}
A standard ntyft rule is a {\em patience rule} for argument $i$ of $f$
if it is of the form
{\small
\[
\frac{x_i\trans{\tau}y}{f(x_1,\ldots,x_{\ar(f)})\trans{\tau}f(x_1,\ldots,x_{i-1},y,x_{i+1},\ldots,x_{\ar(f)})}
\]
}

\noindent
Given a predicate $\Gamma$, the rule above is a {\em $\Gamma$-patience rule} if $\Gamma(f,i)$.
A TSS is \emph{$\Gamma$-patient} if it contains all $\Gamma$-patience rules.
A standard ntytt rule is {\em $\Gamma$-patient} if it is
irredundantly provable from the $\Gamma$-patience rules; else it is {\em $\Gamma$-impatient}.
}
\end{definition}

\noindent
Typically, in process algebra, there are patience rules for both arguments of the merge operator
and for the first argument of sequential composition, as they can contain running processes,
but not for the arguments of alternative composition or for the second argument of sequential composition.


\subsection{Ruloids}\label{sec:ruloids}

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

First $P$ is converted to a standard TSS $P^\dagger$ in decent ntyft format.
In this conversion from \cite{GV92}, free variables in a rule are
replaced by arbitrary closed terms, and if the source is of the form $x$, then
this variable is replaced by a term $f(x_1,\ldots,x_{\ar(f)})$
for each function symbol $f$ in the signature of $P$,
where the variables $x_1,\ldots,x_{\ar(f)}$ are fresh.

Next, using a construction from \cite{FvG96}, left-hand sides of
positive premises are reduced to variables. Roughly
the idea is, given a premise \nietplat{$f(t_1,\ldots,t_n)\trans{\alpha}y$}
in a rule $r$, and another 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 term as left-hand side have disappeared.
This yields an intermediate standard TSS $P^\ddagger$ in xynft format, of which all the
rules are irredundantly provable from $P$. In fact, the rules of $P^\ddagger$ are exactly the
xynft rules irredundantly provable from $P^\dagger$.
The motivation for this transformation step is that for TSSs in xynft format the semantic phrase
``for each set $N$ of closed negative literals with $\frac{N}{\nu}$ irredundantly provable
from $P$'' in the second clause of Def.~\ref{def:wsp} of a well-supported proof
can be replaced by a syntactic phrase: ``for each closed substitution instance
$\frac{N}{\nu}$ of a rule in $R$''.

Finally, non-standard rules with a negative
conclusion \nietplat{$t\ntrans\alpha$} are introduced.  The motivation is
that instead of the notion of well-founded provability of
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 non-standard rule
$\frac{H}{f(x_1,\ldots,x_n)\ntrans{\alpha}}$ is obtained by picking
one premise from each xynft rule in $P^\ddagger$ with a conclusion of the form
\nietplat{$f(x_1,\ldots,x_n)\trans{\alpha}t$}, and including the denial of
each of the selected premises as a premise in $H$.

The resulting TSS, which is in decent ntyft format, is denoted by $P^+$.
The above construction implies that if $P$ is $\Gamma$-patient, then so is $P^+$.
In \cite{BFvG04} it was established, for all closed literals $\mu$, that $P\vdash_{\it ws}\mu$
if and only if $\mu$ is irredundantly provable from $P^+$. By definition,
the \emph{$P$-ruloids} are the (decent) nxytt rules irredundantly provable from $P^+$.

There is a well-supported proof from a TSS $P$ of a transition \nietplat{$\rho(t) \trans{a}q$}
if and only if there is a derivation of this transition that uses at the root a $P$-ruloid with source $t$.
This result underlies the decomposition method in Sect.~\ref{sec:decomposition}.

\begin{proposition}\label{prop:ruloid}\cite{BFvG04}
Let $P=(\Sigma,R)$ be a standard TSS in ready simulation format,
$t\in\mathbb{T}(\Sigma)$ and $\rho: V \rightarrow \mathbb{T}(\Sigma)$ a closed substitution.
Then $P\vdash_{\it ws}\rho(t)\trans\alpha q$ if and only if there
are a $P$-ruloid $\frac{H}{t\trans\alpha u}$ and a {\valuation}
$\rho'$ such that $P\vdash_{\it ws}\rho'(\mu)$ for all $\mu\in H$,
$\rho'(t)=\rho(t)$ and $\rho'(u)=q$.
\end{proposition}

\subsection{Linear proofs}\label{sec:linearity}

\begin{definition}\rm
An irredundant proof of a rule $\frac{H}{\lambda}$ is called \emph{linear}
if no two hypotheses in the proof tree of Def~\ref{def:proof} are labelled with the same positive premise.
\end{definition}
Clearly, each ntytt rule provable from a TSS is a substitution instance of an ntytt rule that has a
linear proof.
In Def.~\ref{def:wsp} it does not make any difference whether in clause 2 we quantify over rules
$\frac{N}{\nu}$ that are provable (as in \cite{vGl04,BFvG04,FvGdW03}), irredundantly provable (as in
\cite{FvGdW12}), or linearly provable.

In Sect.~\ref{sec:ruloids} a non-standard TSS $P^+$ is constructed out of a given TSS $P$ in ready
simulation format, via the intermediate stages $P^\dagger$ and $P^\ddagger$.
Here $P^\ddagger$ consists of all xynft rules irredundantly provable from $P^\dagger$.
With $\hat P^\ddagger$ we denote the TSS consisting of all xynft rules linearly provable from $P^\dagger$.
The TSS $P^+$ is obtained by augmenting $P^\ddagger$ with non-standard rules;
with $\hat P^+$ we denote the corresponding augmentation of $\hat P^\ddagger$.
For the construction of the non-standard rules in the augmentation, it makes no
difference whether we start from $P^\ddagger$ or $\hat P^\ddagger$, since the difference disappears
when abstracting from the right-hand sides of positive literals.
Thus, $\hat P^+ \subseteq P^+$ and each rule in $P^+$ is a substitution instance of a rule in $\hat P^+$.
Hence, an ntytt rule is irredundantly provably from $\hat P^+$ iff it is irredundantly provable from $P^+$.

A \emph{linear} $P$-ruloid has a linear proof from $\hat P^+$.
Clearly, each $P$-ruloid is a substitution instance of a linear $P$-ruloid.
So Prop.~\ref{prop:ruloid} still holds if we only consider linear ruloids.


\subsection{Decomposition of modal formulas}\label{sec:decomposition}

In \cite{FvGdW12} it was shown how one can decompose formulas from $\mathbb{O}$.
To each term $t$ and formula $\phi\in\mathbb{O}$, a set $t^{-1}(\phi)$ of decomposition mappings
$\psi:V\rightarrow\mathbb{O}$ is assigned. Each $\psi\in t^{-1}(\phi)$ guarantees that
for any {\valuation} $\rho$,
$\rho(t)\models\phi$ if $\rho(x)\models\psi(x)$ for all $x\in\var(t)$. Vice versa, whenever
$\rho(t)\models\phi$, there is a decomposition mapping $\psi \in t^{-1}(\phi)$ with
$\rho(x)\models\psi(x)$ for all $x \in \var(t)$.


\begin{definition}\label{def:decomposition} \cite{FvGdW12}
{\rm
Let $P=(\Sigma,R)$ be a $\Gamma$-patient standard TSS in ready simulation format. We define
$\cdot^{-1}:\mathbb{T}(\Sigma)\times\mathbb{O}\rightarrow\mbox{\fsc
  P}(V\rightarrow\mathbb{O})$ as the function that for each
$t\in\mathbb{T}(\Sigma)$ and $\varphi\in\mathbb{O}$ returns the
set $t^{-1}(\varphi)\in\mbox{\fsc P}(V\mathbin{\rightarrow}\mathbb{O})$
of decomposition mappings $\psi:V\mathbin{\rightarrow}\mathbb{O}$
generated by following five conditions. In the remainder of this definition, $t$ is a univariate term.

\begin{enumerate}
\item\label{dec1}
$\psi\in t^{-1}(\bigwedge_{i\in I}\phi_i)$ iff there are $\psi_i\in t^{-1}(\phi_i)$ for each $i\in I$ such that
$\psi(x)=\bigwedge_{i\in I}\psi_i(x)$ for all $x\in V$.

\item\label{dec2}
$\psi\in t^{-1}(\neg\phi)$ iff there is a function $h:t^{-1}(\phi)\rightarrow\var(t)$ such that
$\psi(x)$ equals either $\bigwedge_{\chi\in h^{-1}(x)}\neg\chi(x)$ if $x\in\var(t)$, or $\top$ if $x\notin\var(t)$.

\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)$ such that $\psi(x)$ equals either
\[
\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
\]
if $x\in\var(t)$, or $\top$ if $x\notin\var(t)$.

\item\label{dec4}
$\psi\in t^{-1}(\eps\phi)$ iff one of the following holds.
\begin{enumerate}
\item  
\label{4a}
There is a $\chi\in t^{-1}(\phi)$ such that
$\psi(x)$ equals either $\eps\chi(x)$ if $x$ occurs $\Gamma$-liquid in $t$, or $\chi(x)$ otherwise.

\item
\label{4b}
There is a $\Gamma$-impatient $P$-ruloid $\frac{H}{t\trans{\tau}u}$ and a
$\chi\in u^{-1}(\eps\phi)$ such that $\psi(x)$ equals either
\[
  \displaystyle{\eps\Big(\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\Big)}
\]
if $x$ occurs $\Gamma$-liquid in $t$, or
\[
  \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}
\]
if $x$ occurs $\Gamma$-frozen in $t$, or $\top$ if $x\notin\var(t)$.
\end{enumerate}

\item\label{dec6}
$\psi\in\sigma(t)^{-1}(\phi)$ for a non-injective substitution $\sigma:\var(t)\rightarrow V$
iff there is a $\chi\in t^{-1}(\phi)$ such that
$\psi(x)=\bigwedge_{z\in\sigma^{-1}(x)}\chi(z)$ for all $x\in V$.
\end{enumerate}
}
\end{definition}

\begin{theorem}\label{thm:decomposition} \cite{FvGdW12}
Let $P=(\Sigma,R)$ be a $\Gamma$-patient complete standard TSS in ready
simulation format. For any term $t\in\mathbb{T}(\Sigma)$, {\valuation}
$\rho$, and $\phi\in\mathbb{O}$:\vspace*{-1.5mm}
\[
\rho(t)\models\phi\ \Leftrightarrow
\ \exists\psi\in t^{-1}(\phi)\ \forall x\in \var(t):\rho(x)\models\psi(x)\enspace .
\]
\end{theorem}

\section{Delay resistant TSSs}\label{sec:delay-resistance}

\newcommand{\ndr}{negative delay resistant}
\newcommand{\pdr}{positive delay resistant}
\newcommand{\dra}{delay resistant}
\newcommand{\dr}{delay resistant}

In the next section the decomposition method from Sec.~\ref{sec:decomposition} is applied to obtain
congruence formats for (rooted) delay and weak bisimilarity.
However, Def.~\ref{def:decomposition} needs to be refined in the case $t^{-1}(\eps\phi)$,
because in the modal logics for delay and weak bisimilarity, occurrences of subformulas
$\diam{\beta}\phi'$ are always preceded by $\eps$, while in Def.~\ref{def:decomposition}
this is not always the case. The refinement of Def.~\ref{def:decomposition}, which is presented in
Def.~\ref{def:decomposition-dr}, is only valid for so-called {\dra} TSSs.

Def.~\ref{def:delay-resistant} of delay resistance is inspired by a requirement in the
RDB and RWB cool formats, see \cite[Def.~15(3)]{vGl11}.
It is crafted in such a way that Prop.~\ref{prop:delay-resistance} holds:\vspace{-2pt}
if for a premise \nietplat{$x \trans\beta y$} in a ruloid \nietplat{$r=\frac{H}{t\trans{\alpha}u}$}\vspace{-3pt}
the execution of $\beta$ is delayed by a $\tau$-step, i.e.\  for some $\sigma$ we
have \nietplat{$\sigma(x) \trans\tau \trans\beta \sigma(y)$},
then the conclusion $\sigma(t) \trans{\alpha} \sigma(u)$ of the $\sigma$-instance of
$r$ is unaffected, or merely delayed by a $\tau$-step as well.

\vspace*{-1mm}

\begin{example}
Consider the rooted delay bisimilar processes $p_0$ and $p_1$ from Ex.~\ref{ex:weak bisimulations}.
The ruloid $r$ may apply when substituting $p_0$ for $x$ and $b$ for $\beta$, given that \nietplat{$p_0 \trans b 0$}.
If instead of $p_0$ we substitute $p_1$ for $x$, to safeguard congruence, it is necessary
that the (possibly delayed) conclusion of $r$ can still be derived, even though we only have
\plat{$p_1 \trans \tau q \trans b 0$}.
\end{example}

\noindent
In Def.~\ref{def:positive} we allow two possible implementations of this idea.
Each premise $x {\trans\beta} y$ of $r$ is either \emph{delayable} (Def.~\ref{def:delayable}),
in which case $\sigma(x)\! \trans\tau \trans\beta \!\sigma(y)$ induces $\sigma(t)\! \trans\tau\trans{\alpha} \!\sigma(u)$
by two ruloids that can be used in place of $r$; or
\emph{$\tau$-pollable}, meaning that $r$ remains valid if this premise
is replaced by \nietplat{$x \trans\tau z$} for a fresh variable $z$, so
that the premise \nietplat{$\sigma(x) \trans\tau \sigma(z)$} takes over the role of $\sigma(x) \trans\beta \sigma(y)$.
Def.~\ref{def:positive} and Prop.~\ref{prop:delay-resistance} allow only finitely many delayable positive premises, but infinitely
many $\tau$-pollable ones.

\vspace*{-1mm}

\begin{definition}\rm\label{def:delayable}
A premise $w \trans\beta y$ of an ntytt rule $r=\frac{H}{t\trans\alpha u}$ is
\emph{delayable} in a TSS $P$ if
  there are ntytt rules $\frac{ H_1}{t \trans{\tau} v}$ and $\frac{ H_2}{v \trans{\alpha} u}$, linearly
  provable from $P$, with {$H_1\subseteq (H\mathbin\setminus \{w \mathbin{\trans{\beta}} y\})\linebreak[3]\cup\{w \trans{\tau} z\}$}
  and \nietplat{$H_2\subseteq (H\setminus \{w \trans{\beta} y\})\cup\{z \trans{\beta} y\}$}
  for some term $v$ and fresh variable $z$.
\end{definition}

\noindent
Suppose that $\frac{H}{t\trans\alpha u}$ in Def.~\ref{def:delayable} is a ruloid, so that $w$ is a variable $x$.
The intuition behind this definition is that the argument $x$ of $t$
may not be able to perform a $\beta$-transition to a term $y$ immediately, but only after
a $\tau$-transition to $z$. The ruloid $\frac{H_1}{t \trans{\tau} v}$ then
allows $t$ to postpone its $\alpha$-transition to $u$, by first performing a $\tau$-transition to $v$.
The ruloid $\frac{H_2}{v \trans{\alpha} u}$\vspace{1pt} guarantees that the postponed $\beta$-transition
from $z$ to $y$ still gives rise to an $\alpha$-transition from $v$ to $u$.

Linearity is needed to make sure that in the construction of ruloids,
distinct delayable positive premises are never collapsed to a single non-delayable premise.

Def.~\ref{def:positive} requires that each positive premise is delayable (i.e., in the finite set $H^d$),
$\tau$-pollable, or redundant.

\vspace*{-1mm}

\begin{definition}\rm\label{def:positive}
An ntytt rule \nietplat{$\frac{ H}{t\trans{\alpha}u}$}
is \emph{\pdr} w.r.t.\ a TSS $P$ if there exists a finite set $H^d \subseteq H^+$ of delayable positive premises such that
  for each set $M \subseteq H^+\setminus H^d$ there is a rule
  \nietplat{$r_M=\frac{H_M}{t\trans{\alpha}u}$}, linearly provable from $P$, where
  $H_M \subseteq (H\setminus M) \cup M_\tau$ with
  $M_\tau\mathbin=\{w \trans{\tau} z_y \mid (w \trans{\beta} y) \mathbin\in M,~ z_y~\mbox{fresh}\}$.
\end{definition}
The intuition behind Def.~\ref{def:negative} is closely related to Def.~\ref{def:delayable}.
If a ruloid $\frac{H}{t\trans\alpha u}$ has a premise $x\ntrans\gamma$, we want it not to apply in case
$\sigma(x) \trans\tau \trans\gamma$, even if $\sigma(x)\ntrans\gamma$.
We therefore require that for each premise \nietplat{$x\ntrans\gamma$} there must also be a premise $x\ntrans\tau$. We make an
exception for redundant premises \nietplat{$x\ntrans\gamma$}.

\vspace*{-1mm}

\begin{definition}\rm\label{def:negative}
A rule \nietplat{$\frac{H}{t\trans{\alpha}u}$}
is \emph{\ndr} w.r.t.\ a TSS $P$ if there is a rule \nietplat{$\frac{H'}{t\trans{\alpha}u}$}, linearly provable from $P$,
with $H' \subseteq H^+ \cup H^{s-}$.
\end{definition}

\vspace*{-3mm}

\begin{definition}\rm\label{def:delay-resistant}
An ntytt rule \nietplat{$\frac{ H}{t\trans{\alpha}u}$}
is \emph{delay resistant} w.r.t.\ a TSS $P$ if it is {\pdr} as well as \ndr.
A standard TSS $P$ in ready simulation format is \emph{delay resistant} if all its linear ruloids
with a positive conclusion are delay resistant w.r.t.\ $\hat P^+$.
\end{definition}

\noindent
The following proposition is key to the notion of delay resistance. It will allow us to adapt the definition
of modal decomposition for {\dra} TSSs, so that it becomes applicable for generating congruence formats
for weak semantics, like delay and weak bisimilarity, with a modal characterisation in which
$\diam{\beta}\phi$ is always preceded by $\eps$.

\vspace*{-1mm}

\begin{proposition}\label{prop:delay-resistance}
Let $P$ be a {\dra} standard TSS in ready simulation format.
Let \nietplat{$\frac{H}{t\trans{\alpha}u}$}\vspace*{-1mm} be a $P$-ruloid and $\rho$ a {\valuation} with
\nietplat{$P \vdash_{\it ws} \rho(x) \epsarrow\trans\beta \rho(y)$}\vspace*{-0.5mm} for each premise \nietplat{$x\trans\beta y$} in $H^+$ and
$P \vdash_{\it ws} \rho(x)\!\ntrans\gamma$ for each premise \nietplat{$x\!\ntrans\gamma$}\vspace*{-0.5mm} in $H^{s-}$.
Then \nietplat{$P \vdash_{\it ws} \rho(t) \epsarrow\trans\alpha \rho(u)$}.
\end{proposition}

\noindent
For {\dra} TSSs case \ref{4b} of Def.~\ref{def:decomposition},
$t^{-1}(\eps\phi)$, needs to be adapted, to ensure that in the modal logics for delay and weak bisimilarity,
occurrences of subformulas $\diam{\beta}\phi''$ are always preceded by $\eps$. Moreover, case \ref{4a}
is provided with the restriction that $\phi$ is not of the form $\diam{\alpha}\phi'$.
Else decompositions of formulas $\eps\diam{\alpha}\phi'$ in $\IO{d}$ would
be defined in terms of formulas $\chi\in t^{-1}(\diam{\alpha}\phi')$, while $\diam{\alpha}\phi'$ is not in $\IO{d}$.
Instead, if $\phi$ is of the form $\diam{\alpha}\phi'$, cases \ref{dec3} and \ref{dec4}
of Def.~\ref{def:decomposition} are combined, as can be seen in case 4b(ii) below.

\begin{definition}\rm\label{def:decomposition-dr}
Let $P$ be a {\dra} $\Gamma$-patient standard TSS
in ready simulation format. We define 
$\cdot^{-1}_{\rm dr}:\mathbb{T}(\Sigma)\times\mathbb{O}\rightarrow\mbox{\fsc
  P}(V\rightarrow\mathbb{O})$ exactly as $\cdot^{-1}$ in
Def.~\ref{def:decomposition}, except for case \ref{dec4}:
$t^{-1}_{\rm dr}(\eps\phi)$ (with $t$ univariate).
\pagebreak[3]

\begin{enumerate}
\item[4.]
\label{dec-delay}
$\psi\in t^{-1}_{\rm dr}(\eps\phi)$ iff one of the following holds.

\begin{enumerate}
\item\label{4a-delay}
$\phi$ is not of the form $\diam{\alpha}\phi'$, and there is a $\chi\in t^{-1}_{\rm dr}(\phi)$ such that
$\psi(x)$ equals either $\eps\chi(x)$ if $x$ occurs $\Gamma$-liquid in $t$, or $\chi(x)$ otherwise.

\item
\begin{enumerate}
\item[(i)]\label{4bi}
There is a $\Gamma$-impatient $P$-ruloid $\frac{H}{t\trans{\tau}u}$ and a $\chi\in u^{-1}_{\rm dr}(\eps\phi)$,
\item[(ii)]\label{4bii}
or $\phi$ is of the form $\diam{\alpha}\phi'$, and there is a $P$-ruloid $\frac{H}{t\trans{\alpha}u}$\vspace*{0.5mm} and a
$\chi\in u^{-1}_{\rm dr}(\phi')$,\vspace{1.5mm}
\end{enumerate}
such that $\psi(x)$ equals either
\[
  \displaystyle{\eps\Big(\chi(x)\ \land\
          \!\!\!\!\!\bigwedge_{x\trans{\beta}y\in H^+}\!\!\!\!\!\eps\diam{\beta}\chi(y)
          \ \land\ \!\!\!\!\! \bigwedge_{x\ntrans{\gamma}\in
           H^{s-}}\!\!\!\!\!\!\neg\diam{\gamma}\top\Big)}
\]
if $x$ occurs $\Gamma$-liquid in $t$, or
\[
  \displaystyle{\chi(x)\ \land\ \!\!\!\!\!\bigwedge_{x\trans{\beta}y\in H^+}\!\!\!\!\!\eps\diam{\beta}\chi(y)
                \ \land\ \!\!\!\!\!\! \bigwedge_{x\ntrans{\gamma}\in H^{s-}}\!\!\!\!\!\neg\diam{\gamma}\top}
\]
if $x$ occurs $\Gamma$-frozen in $t$, or $\top$ if $x\notin\var(t)$.
\end{enumerate}
\end{enumerate}
\end{definition}
\marginpar{\hfill\rotatebox{90}{
\begin{tabular}{l}
Erratum, 11 March 2017: With case 4b(i) as formulated here, Prop.~\ref{prop:rooted_delay_preservation} does not hold.\\
``$\chi\in u^{-1}_{\rm dr}(\eps\phi)$'' should be ``$\chi\in u^{-1}_{\rm dr}(\eps\phi')$ in case $\phi$
is of the form $\diam\tau\phi'$, and $\chi\in u^{-1}_{\rm dr}(\eps\phi)$ otherwise''.
\end{tabular}}~~\mbox{}}

\noindent
The counterpart of Thm.~\ref{thm:decomposition} for {\dra} TSSs is:

\begin{theorem}\label{thm:dr-decomposition}
Let $P=(\Sigma,R)$ be a {\dra} $\Gamma$-patient complete standard TSS in ready simulation format.
For any $t\mathbin\in\mathbb{T}(\Sigma)$, {\valuation} $\rho$, and $\phi\mathbin\in\mathbb{O}$:
\[
\rho(t)\models\phi\ \Leftrightarrow
\ \exists\psi\in t^{-1}_{\rm dr}(\phi)\ \forall x\in \var(t):\rho(x)\models\psi(x)\enspace .
\]
\end{theorem}


\section{Congruence results}\label{sec:congruence}

A behavioural equivalence $\sim$ is a {\em congruence} for a function symbol
$f$ if $p_i\sim q_i$ for all $i\in\{1,\ldots,\ar(f)\}$
implies that $f(p_1,\ldots,p_{\ar(f)})\sim f(q_1,\ldots,q_{\ar(f)})$.
We apply the decomposition method from the previous section to derive congruence formats
for delay bisimulation and rooted delay bisimulation semantics. The idea behind the construction of these formats is that 
a formula from the characterising logic of the equivalence
under consideration must always be decomposed into formulas from this same logic.
The delay bisimulation format guarantees that a formula from $\IO{d}$ is always decomposed into
formulas from $\IO{d}^\equiv$ (Prop.~\ref{prop:rdelay-rdelay}).
Likewise, the rooted delay bisimulation format guarantees that a formula from $\IO{rd}$ is always
decomposed into formulas from $\IO{rd}^\equiv$ (Prop.~\ref{prop:rooted_delay_preservation}).
This implies the desired congruence results (Thm.~\ref{thm:delay-congruence} resp.\ Thm.~\ref{thm:rooted-delay-congruence}).
These results are transposed to (rooted) weak bisimilarity
by adding one condition to the congruence format for (rooted) delay bisimilarity.

\subsection{Congruence format for rooted delay bisimilarity}\label{sec:formats}

We recall the notion of a rooted branching bisimulation safe rule, which underlies
the rooted branching bisimulation format from \cite{FvGdW12}. The congruence format
for rooted delay bisimilarity is obtained by additionally requiring delay resistance.

We assume two predicates on arguments of function symbols from \cite{Fok00,FvGdW12}.
The predicate $\Lambda$ marks arguments that contain processes that
have started executing (but may currently be unable to execute).
The predicate $\aleph$ marks arguments that contain
processes that can execute immediately.
For example, in process algebra, $\Lambda$ and $\aleph$ hold for the arguments of the
merge $t_1\|t_2$, and for the first argument of sequential composition $t_1{\cdot}t_2$;
they can contain processes that started to execute in the past, and these processes
can continue their execution immediately. On the other hand, $\Lambda$ and $\aleph$
typically do not hold for the second argument of sequential composition; it contains a process
that did not yet start to execute, and cannot execute immediately (in absence of the empty process).
$\Lambda$ does not hold and $\aleph$ holds for the arguments of
alternative composition $t_1+t_2$; they contain processes that did not yet
start to execute, but that can start executing immediately.

\begin{definition}\label{def:rooted_branching_bisimulation_safe}\rm\cite{FvGdW12}\,
An ntytt rule $r=\frac{H}{t\trans\alpha u}$ is {\em rooted branching bisimulation safe}
w.r.t.\ $\aleph$ and $\Lambda$ if it satisfies the following conditions.
Let $x\in\var(t)$.
\begin{enumerate}
\item \label{rhs}
Right-hand sides of positive premises occur only $\Lambda$-liquid in $u$.
\item \label{Lambda}
If $x$ occurs only $\Lambda$-liquid in $t$, then $x$ occurs only $\Lambda$-liquid in $r$.
\item \label{aleph}
If $x$ occurs only $\aleph$-frozen in $t$, then $x$ occurs only $\aleph$-frozen in $H$.
\item \label{main}
If $x$ has exactly one $\aleph$-liquid occurrence in $t$, which is also $\Lambda$-liquid,
then $x$ has at most one $\aleph$-liquid occurrence in $H$, which must be in a positive premise.
If moreover this premise is labelled $\tau$, then $r$ must be $\aL$-patient.
\setcounter{saveenumi}{\theenumi}
\end{enumerate}
\end{definition}

\begin{definition}\rm\label{def:rooted_delay_bisimulation_format}
A standard TSS $P$ is in {\em rooted delay bisimulation format} if it
is in ready simulation format and \dr,
and, for some $\aleph$ and $\Lambda$, it is $\aL$-patient and all its rules are
rooted branching bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.

This TSS is in {\em delay bisimulation format} if $\Lambda$ is universal.
\end{definition}

\begin{proposition}{\rm\cite{FvGdW12}}
\label{prop:preservation_bra_bisimulation_safe}
Let $P$ be a standard TSS in ready simulation format, in which each transition rule is
rooted branching bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
Then each $P$-ruloid is rooted branching bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
\end{proposition}


\subsection{Congruence for rooted delay bisimilarity}
\label{sec:congruenceresults}

Consider a standard TSS that is in rooted delay bisimulation format, w.r.t.\ some $\aleph$ and $\Lambda$.
Def.~\ref{def:decomposition-dr} yields decomposition mappings $\psi\mathbin\in
t^{-\!1}_{\rm dr}\hspace{-1pt}(\phi)$, with $\Gamma=\aL$.
If $\phi\in\IO{d}$, then $\psi(x)\in\IO{d}^{\equiv}$ if $x$ occurs only
$\Lambda$-liquid in $t$. (That is why in the delay bisimulation
format, $\Lambda$ must be universal.) If
$\phi\in\IO{rd}$, then $\psi(x)\in\IO{rd}^{\equiv}$ for all variables
$x$. These preservation results induce the promised congruence
results for delay bisimilarity and rooted delay bisimilarity, respectively.

\begin{proposition}\label{prop:rdelay-rdelay}
Let $P$ be a {\dra}, $\aL$-patient standard TSS in ready simulation format,
in which each rule is rooted branching bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
For any term $t$ and variable $x$ that occurs only $\Lambda$-liquid in $t$:
\[
\phi\in\IO{d}\ \Rightarrow\ \forall\psi\in t^{-1}_{\rm dr}(\phi):\psi(x)\in\IO{d}^\equiv\enspace .
\]
\end{proposition}

\begin{proposition}\label{prop:rooted_delay_preservation}
Let $P$ be a {\dra}, $\aL$-patient standard TSS in ready simulation format,
in which each rule is branching delay bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
For any term $t$ and variable $x$:
\[
\phi\in\IO{rd}\ \Rightarrow\ \forall\psi\in t^{-1}_{\rm dr}(\phi):\psi(x)\in\IO{rd}^\equiv\enspace .
\]
\end{proposition}

\begin{theorem}\label{thm:delay-congruence}
If $P$ is a complete TSS in delay bisimulation format, then
$\bis{d}$ is a congruence for $P$.
\end{theorem}

\begin{proof}
By Def.~\ref{def:rooted_delay_bisimulation_format} each rule of $P$
is rooted branching bisimulation safe w.r.t\ some $\aleph$ and the
universal predicate $\Lambda$, and $P$ is \dr, $\aL$-patient and in
ready simulation format.
Let $\rho,\rho'$ be {\valuation}s and $t$ a term with
$\rho(x) \bis{d} \rho'(x)$ for all $x\in\var(t)$.

Let $\rho(t)\models\phi \in \IO{d}$.
By Thm.~\ref{thm:dr-decomposition}, taking $\Gamma=\aL$, there is a $\psi
\in t^{-1}_{\rm dr}(\phi)$ with $\rho(x) \models \psi(x)$ for all $x\in\var(t)$.
Since $x$ occurs $\Lambda$-liquid in $t$ (because $\Lambda$ is universal),
by Prop.~\ref{prop:rdelay-rdelay}, $\psi(x) \in\IO{d}^\equiv$ for all $x\in\var(t)$.
By Thm.~\ref{thm:characterisation}, $\rho(x) \bis{d} \rho'(x)$
implies $\rho(x) \sim_{\IO{d}^\equiv} \rho'(x)$ for all $x \in \var(t)$.
So $\rho'(x)\models\psi(x)$ for all $x \in \var(t)$. Therefore, by Thm.~\ref{thm:dr-decomposition},
$\rho'(t)\models\phi$.  Likewise, $\rho'(t)\models\phi \in \IO{d}$ implies $\rho(t)\models\phi$.
So $\rho(t) \sim_{\IO{d}} \rho'(t)$. Hence, by
Thm.~\ref{thm:characterisation}, $\rho(t) \bis{d} \rho'(t)$.
\qed
\end{proof}

\begin{theorem}\label{thm:rooted-delay-congruence}
If $P$ is a complete TSS in rooted delay bisimulation format, then
$\bis{rd}$ is a congruence for $P$.
\end{theorem}

\noindent
The proof of Thm.~\ref{thm:rooted-delay-congruence} is similar to the one of Thm.~\ref{thm:delay-congruence},
except that Prop.~\ref{prop:rooted_delay_preservation} is applied instead of
Prop.~\ref{prop:rdelay-rdelay}; therefore $x$ need not occur $\Lambda$-liquid in $t$,
so that universality of $\Lambda$ can be dropped.


\subsection{Rooted weak bisimilarity as a congruence}
\label{sec:weak-congruence}

We now proceed to derive a congruence format for rooted weak bisimilarity.
It is obtained from the congruence format from \cite{FvGdW12} for rooted $\eta$-bisimilarity by
additionally requiring delay resistance. The format for rooted $\eta$-bisimilarity in turn is obtained
by strengthening condition \ref{rhs} in the definition of rooted branching bisimulation safeness.


\begin{definition}\label{def:rooted_eta_bisimulation_safe} 
{\rm\cite{FvGdW12}
An ntytt rule $\frac{H}{t\trans\alpha u}$ is {\em rooted $\eta$-bisimu\-lation safe}
w.r.t.\ $\aleph$ and $\Lambda$ if it satisfies conditions
\ref{Lambda}--\ref{main} of Def.~\ref{def:rooted_branching_bisimulation_safe}, together with:
\begin{itemize}
\item[$\ref*{rhs}'$.] Right-hand sides of positive premises occur only $\aL$-liquid in $u$.
\end{itemize}
}
\end{definition}

\begin{definition}\label{def:weak_bisimulation_format}
{\rm
A standard TSS is in {\em rooted weak bisimulation format} if it is
in ready simulation format and \dr,
and, for some $\aleph$ and $\Lambda$, it is $\aL$-patient and contains
only rules that are rooted $\eta$-bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.

This TSS is in {\em weak bisimulation format} if $\Lambda$ is universal.
}
\end{definition}

\begin{proposition}{\rm\cite{FvGdW12}}
\label{prop:preservation_eta_bisimulation_safe}
Let $P$ be a TSS in ready simulation format, in which each rule is
rooted $\eta$-bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
Then each $P$-ruloid is rooted $\eta$-bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
\end{proposition}

\begin{proposition}\label{prop:rweak-rweak}
Let $P$ be a {\dra}, $\aL$-patient standard TSS in ready simulation format,
in which each rule is rooted $\eta$-bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
For any term $t$ and variable $x$ that occurs only $\Lambda$-liquid in $t$:\vspace*{-1.5mm}
\[
\phi\in\IO{w}\ \Rightarrow\ \forall\psi\in t^{-1}_{\rm dr}(\phi):\psi(x)\in\IO{w}^\equiv\enspace .
\]
\end{proposition}

\vspace*{-4.5mm}

\begin{proposition}\label{prop:rooted_weak_preservation}
Let $P$ be a {\dra}, $\aL$-patient standard TSS in ready simulation format,
in which each rule is rooted $\eta$-bisimulation safe w.r.t.\ $\aleph$ and $\Lambda$.
For any term $t$ and variable $x$:\vspace*{-1.5mm}
\[
\phi\in\IO{rw}\ \Rightarrow\ \forall\psi\in t^{-1}_{\rm dr}(\phi):\psi(x)\in\IO{rw}^\equiv\enspace .
\]
\end{proposition}

\vspace*{-3.5mm}

\begin{theorem}
If $P$ is a complete TSS in weak bisimulation format, then
\mbox{}$\bis{w}$ is a congruence for $P$.
\end{theorem}

\vspace*{-3.5mm}

\begin{theorem}
\label{thm:rooted-weak-congruence}
If $P$ is a complete TSS in rooted weak bisimulation format, then
$\bis{rw}$ is a congruence for $P$.
\end{theorem}

\vspace*{-1mm}


\subsection{Counterexamples}
\label{sec:counterexamples}

In \cite{FvGdW12} it was shown that none of the syntactic requirements of the rooted branching bisimulation format
in Def.~\ref{def:rooted_branching_bisimulation_safe} can be omitted, and that the presence of $\aL$-patience rules is crucial.
Here we present examples to show that none of the requirements that make up delay resistance is redundant.

All TSSs in this section are standard, complete, in ready-simulation format and $\aL$-patient, and their rules are rooted $\eta$-bisimulation safe.

\vspace*{-1.5mm}

\begin{example}
\label{exa:negative}
Let $f$ be a unary function with an $\aleph$-liquid, $\Lambda$-frozen argument, defined by
$\frac{x\ntrans{a}}{f(x)\trans{b}0}$. This rule is \pdr, but not \ndr.

$p_0,p_1,q,0$ are constants with $p_0\trans{\tau}p_0$, $p_0\trans{a}0$, $p_1\trans{\tau}q$ and $q\trans{a}0$.
Note that $p_0\bis{rd}p_1$. However, $f(p_0)$ exhibits no transitions, while \nietplat{$f(p_1)\trans{b}0$}.
So \nietplat{$f(p_0)\notbis{rd}f(p_1)$}. Hence $\bis{rd}$ is not a congruence.
\end{example}

\vspace*{-1.5mm}

\begin{example}
Let $f$ be a unary function with an $\aleph$-liquid, $\Lambda$-frozen argument, defined by
$\frac{x\trans{a}y}{f(x)\trans{b}0}$. This TSS is \ndr, but not \pdr.

Consider the LTS from Ex.~\ref{exa:negative}.
We have $f(p_0)\trans{b}0$, while $f(p_1)$ does not exhibit any transitions.
So $f(p_0)\notbis{rd}f(p_1)$. Hence $\bis{rd}$ is not a congruence.
\end{example}

\noindent
The following example shows that the requirement that $H^d$ is finite
in Def.~\ref{def:positive} of positive delay resistance is essential.

\vspace*{-1mm}

\begin{example}
$A=\{a_k\mid k\in\mathbb{Z}_{>0}\}\cup\{b\}$. Binary functions $f_k$ for $k\in\mathbb{Z}_{>0}$,
with both arguments $\aleph$-liquid and only the second argument $\Lambda$-liquid, are defined by
{\small
$$\frac{x_1\trans{\tau}y}{f_k(x_1,x_2)\trans{\tau}f_\ell(x_1,y)}\mbox{~~(for all $\ell>k$)}$$
$$\frac{x_2\trans{\tau}y}{f_k(x_1,x_2)\trans{\tau}f_k(x_1,y)}~~
\frac{\{x_1\trans{a_\ell}y_\ell\mid\ell>k\}\cup\{x_2\trans{a_k}y_k\}}{f_k(x_1,x_2)\trans{b}0}$$
}$\omega_1$, $\omega_2$, $\omega_3$ are constants with $\omega_2\trans{a_k}0$ and $\omega_3\trans{a_k}0$ for all $k\geq 1$,
$\omega_1\trans{\tau}\omega_3$ and $\omega_2\trans{\tau}\omega_3$. Clearly, $\omega_1\bis{rd}\omega_2$.
The last rule is not \dr. With regard to Def.~\ref{def:positive} it violates the
requirement that $H^d$ needs to be chosen finite.

Prop.~\ref{prop:delay-resistance} is violated: although
$\omega_1\epsarrow\trans{a_\ell}$ for $\ell\geq 1$,\vspace{-2pt}
there is no sequence \nietplat{$f_k(\omega_1,\omega_1)\epsarrow\trans{b}$} for any $k\mathbin\geq 1$.\vspace{-2pt}
Since \nietplat{$f_k(\omega_2,\omega_2)\trans{b}0$} for all $k\geq 1$, $\bis{rd}$ is not a congruence. 
\end{example}


\section{Semi-syntactic criteria for delay resistance} \label{sec:semi}

Delay resistance of a TSS $P$ means that each $P$-ruloid has to satisfy a property, and a
non-trivial TSS has infinitely many ruloids.  We now introduce requirements on the \emph{rules} of
$P$\linebreak that imply delay resistance. This yields \emph{semi-syntactic} congruence formats. They are not
purely syntactic, as one of the conditions requires the existence of linearly provable rules.

\vspace*{-1.5mm}

\begin{definition}\rm
A rule \plat{$\frac{H}{t\trans\alpha u}$}\vspace{1pt} is \emph{negative-stable} if for every
premise $w\ntrans\alpha$ in $H\!$, also \nietplat{$w\ntrans\tau$} is in $H\!$.
\end{definition}

\noindent
The difference with Def.~\ref{def:negative} is that here the requirement also applies to redundant
premises \plat{$w\ntrans\alpha$}.
\vspace*{-1.5mm}

\begin{definition}\rm
An ntytt rule is \emph{manifestly delay resistant} w.r.t.\ a TSS $P$ if it is negative-stable, as well as
positive delay resistant w.r.t.\ $P$ where the rules $r_M$ from Def.~\ref{def:positive} and
$\frac{ H_1}{t \trans{\tau} v}$ from Def.~\ref{def:delayable} are, up to bijective renaming of variables,
rules of $P\!$, rather than just linearly provable from~$P\!$.
\end{definition}

\vspace*{-5mm}

\begin{theorem}\label{thm:manifest}
Let $P$ be a standard TSS in decent ntyft format, in which each rule is manifestly delay
resistant w.r.t.\ $P$. Then $P$ is delay resistant.
\end{theorem}


\section[Delay resistance w.r.t.\ Lambda]{Delay resistance w.r.t.\ $\Lambda$}\label{sec:Lambda}

The notion ``{\dr} w.r.t.\ $\Lambda$'' relaxes the notion of delay resistance: the conditions of
Defs.~\ref{def:delayable},~\ref{def:positive} and~\ref{def:negative} need to be checked only for
(sets of) premises that contain a variable that occurs only $\Lambda$-frozen in the source.
This relaxation is possible if the following condition is added to our formats.

\vspace*{-3mm}

\begin{definition}\label{def:smooth}
{\rm
Given a standard ntytt rule $r=\frac{H}{t\trans\alpha u}$, we define the following syntactic condition:
\begin{enumerate}
\setcounter{enumi}{\thesaveenumi}
\setcounter{saveenumi}{\theenumi}
\item \label{smooth}
If $x$ has exactly one occurrence in $t$, which is $\Lambda$-liquid, and an $\aleph$-liquid occurrence in $H$,
then these are the only two occurrences of $x$ in $r$.
\end{enumerate}
}
\end{definition}

\vspace*{-5mm}

\begin{proposition}
Let $P$ be a standard TSS in ready simulation format, in which each rule is rooted branching bisimulation
safe and satisfies condition \ref{smooth} of Def.~\ref{def:smooth} w.r.t.\ $\aleph$ and $\Lambda$.
Then any $P$-ruloid satisfies condition \ref{smooth} of Def.\,\ref{def:smooth} w.r.t.\ $\aleph$ and $\Lambda$.
\end{proposition}

\vspace*{-5mm}

\begin{theorem}\label{thm:delay-resistant}
Let $P$ be a standard TSS in ready simulation format, in which each transition rule is rooted branching bisimulation
safe and satisfies condition \ref{smooth} of Def.~\ref{def:smooth} w.r.t.\ $\aleph$ and $\Lambda$.
Let moreover $P$ be $\aL$-patient and {\dr} w.r.t.\ $\Lambda$. Then $P$ is \dr.\footnote{Using
a notion of \emph{manifest delay resistance w.r.t.\ $\Lambda$ and $P$},
Thms.~\ref{thm:manifest} and~\ref{thm:delay-resistant} can be combined in the obvious way.}
\end{theorem}

\noindent
Hence, by adding condition \ref{smooth} of Def.~\ref{def:smooth}, the delay and weak bisimulation formats do not
require delay resistance at all, since with $\Lambda$ universal there are no $\Lambda$-frozen occurrences.


\section{Syntactic criteria for delay resistance} \label{sec:getting-rid}

We show how delay resistance can be replaced by additional syntactic requirements.

\vspace*{-1.5mm}

\begin{definition}\label{def:strengthened_delay_bisimulation_format}
{\rm
A standard TSS $P\mathbin=(\Sigma,R)$ is in {\em syntactic rooted delay bisimulation format} if,
for some $\aleph$ and $\Lambda$ and predicates $\Delta_\alpha\subseteq\aL$ where $\alpha$ ranges over $A\cup\{\tau\}$:
\begin{enumerate}
\item \label{strengthened-1}
$P$ is in decent nxytt format and $\aL$-patient.
\item \label{strengthened-2}
Each rule in $R$ is rooted branching bisimulation safe and
negative-stable, satisfies condition \ref{smooth} of Def.~\ref{def:smooth} w.r.t.\ $\aleph$ and $\Lambda$,
and has finitely many positive premises.
\item \label{strengthened-3}
If $R$ contains $\frac{H\uplus\{x_i\trans{\beta}y\}}{f(x_1,\ldots,x_{\ar(f)})\trans{\alpha}u}$
where $\neg\Lambda(f,i)$, then:
\begin{enumerate}
\item \label{strengthened-3a}
$\beta=\alpha$;
\item \label{strengthened-3b}
$R$ contains \nietplat{$\frac{H' \cup \{x_i\trans{\tau}y\}}
{f(x_1,\ldots,x_{\ar(f)})\trans{\tau}u}$} for some $H'\subseteq H$; and\vspace{1mm}
\item \label{strengthened-3c}
$y$ has exactly one, $\Delta_\alpha$-liquid occurrence in $u$.
\end{enumerate}
\item \label{strengthened-4}
$R$ contains $\frac{x_i\trans{\alpha}y}{f(x_1,\ldots,x_i,\ldots,x_{\ar(f)})\trans{\alpha}f(x_1,\ldots,y,\ldots,x_{\ar(f)})}$ for all $\Delta_\alpha(f,i)$.
\end{enumerate}
$P$ is in {\em syntactic rooted weak bisimulation format} if its rules
moreover satisfy condition \ref*{rhs}$'$ of Def.~\ref{def:smooth}.
}
\end{definition}

\vspace*{-4mm}

\begin{theorem}\label{thm:syntactic}
If a standard TSS is in syntactic rooted delay bisimulation format, then it is delay resistant.
\end{theorem}

\vspace*{-4mm}

\begin{proof}
Consider a rule $\frac{H\uplus\{x_i\trans\beta y\}}{f(x_1,\dots,x_n)\trans\alpha u}$ of $P$ with $\neg \Lambda(f,i)$.
By condition~\ref{strengthened-3a} of Def.~\ref{def:strengthened_delay_bisimulation_format},
$\beta\mathbin=\alpha$. And by condition~\ref{strengthened-3c} of Def.~\ref{def:strengthened_delay_bisimulation_format},
$y$ has exactly one, $\Delta_\alpha$-liquid occurrence in $u$.
By the combination of Thms.~\ref{thm:manifest} and~\ref{thm:delay-resistant},
it suffices to show that, for some term $v$ and fresh variable $z$, there is a rule
$\frac{H_1}{f(x_1,\dots,x_n) \trans{\tau} v}$ in $R$ with \nietplat{$H_1\subseteq H\cup\{x_i \trans{\tau} z\}$}
and a rule $\frac{ H_2}{v \trans{\alpha} u}$ linearly
provable from $P$ with \nietplat{$H_2\subseteq H\cup\{z \trans{\beta} y\}$}.
Let $v$ be obtained by substituting $z$ for $y$ in $u$.
The first of these rules exists by condition~\ref{strengthened-3b} of
Def.~\ref{def:strengthened_delay_bisimulation_format},\vspace{-1pt} substituting $z$ for $y$.
The second is the rule $\frac{z \trans{\beta}y}{v \trans{\alpha}u}$,
which can be derived by condition~\ref{strengthened-4} of Def.~\ref{def:strengthened_delay_bisimulation_format}.
Here we use that $\beta=\alpha$ and $y$ has exactly one, $\Delta_\alpha$-liquid occurrence in $u$.
\qed
\end{proof}

\noindent
The introduction of predicates $\Delta_\alpha\subseteq\aL$ is of practical importance.
If in Def.~\ref{def:strengthened_delay_bisimulation_format} one would replace the occurrences of $\Delta_\alpha$ by $\aL$,
then for instance the \emph{encapsulation} operator $\partial_H$, which blocks all actions in the set $H$, would violate
condition \ref{strengthened-4} of Def.~\ref{def:strengthened_delay_bisimulation_format}. Namely, the argument of $\partial_H$ is
$\aL$-liquid, but there is no rule $\frac{x\trans a y}{\partial_H(x)\trans a\partial_H(y)}$ if $a\in H$.
Actually, in many applications $\Delta_\alpha$ can be empty, as a rule that tests an $\aleph$-liquid, $\Lambda$-frozen
argument of the source in practice tends to have a single $y$ as right-hand side of the conclusion, so that
condition \ref{strengthened-3c} of Def.~\ref{def:strengthened_delay_bisimulation_format}
is trivially satisfied; a notable example is the rule $\frac{x_1\trans\alpha y}{x_1+x_2\trans\alpha y}$ for alternative composition.

\vspace*{-1.5mm}

\begin{corollary}\label{cor:strenghtened}
If a complete standard TSS $P$ is in syntactic rooted delay (resp.\ weak) bisimulation format,
then $\bis{rd}$ (resp.\ $\bis{rw}$) is a congruence for $P$.
\end{corollary}

\vspace*{-3mm}


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

We revisit some applications of our congruence formats that were considered in \cite{FvGdW12}:
the basic process algebra BPA$_{\varepsilon\delta\tau}$, extended with
binary Kleene star as an example where the predicates $\Delta_\alpha$ from Def.~\ref{def:strengthened_delay_bisimulation_format}
are non-empty, and initial priority which includes negative premises. We also consider a deadlock test outside the
syntactic rooted delay bisimulation format.
In all these cases our formats yield congruence results for $\bis{rd}$ and $\bis{rw}$,
while they are outside the congruence formats for these semantics from \cite{Blo95,vGl11}
(which are within the positive GSOS format \cite{BIM95}).
The TSSs in this section are $\aL$-patient and in decent xynft format.


\paragraph{Basic process algebra}

BPA$_{\varepsilon\delta\tau}$ consists of: actions from an alphabet ${\it Act}\cup\{\tau\}$;
empty process $\varepsilon$; deadlock $\delta$;
alternative composition $t_1+t_2$; sequential composition $t_1\cdot t_2$. Let $\ell$ range over ${\it Act}\cup\{\tau\}$
and $\alpha$ over ${\it Act}\cup\{\tau,\surd\}$. Rules are:\vspace*{-1.5mm}
{\small
$$\frac{~}{\ell\trans\ell \varepsilon}\qquad\frac{~}{\varepsilon\trans\surd\delta}\qquad
\frac{x_1\trans\alpha y}{x_1+x_2\trans\alpha y}\qquad\frac{x_2\trans\alpha y}{x_1+x_2\trans\alpha y}$$\vspace*{-1.5mm}
$$\frac{x_1\trans\ell y}{x_1\cdot x_2\trans\ell y\cdot x_2}\qquad
\frac{x_1\trans\surd y_1~~~x_2\trans\alpha y_2}{x_1\cdot x_2\trans\alpha y_2}$$
}

\vspace*{-1mm}

\noindent
To show that $\bis{rd}$ and $\bis{rw}$ are congruences,
we argue that this TSS satisfies the conditions of Def.~\ref{def:strengthened_delay_bisimulation_format}.
In \cite{FvGdW12} it was shown that it is in rooted $\eta$-bisimulation format, with $\aleph$ and $\Lambda$ defined as follows.
Since the arguments of alternative and sequential composition can all execute immediately,
$\aleph$ holds for all these arguments. Since only the first argument of sequential composition can contain running processes,
it is the only argument for which $\Lambda$ holds.
With regard to condition \ref{strengthened-2} of Def.~\ref{def:strengthened_delay_bisimulation_format},
we need to check that the rules satisfy condition \ref{smooth} of Def.~\ref{def:smooth}:
only the two rules for sequential composition contain a $\Lambda$-liquid occurrence of a variable, $x_1$, in their source;
and in both cases $x_1$ has only one other occurrence in the rule, in the left-hand side of a premise.
Condition \ref{strengthened-3} of Def.~\ref{def:strengthened_delay_bisimulation_format} needs to be verified with regard to the two rules for
alternative composition and the second rule for sequential composition, since in these rules a $\Lambda$-frozen argument of
the source is tested in a premise. Condition \ref{strengthened-3} is satisfied for these rules, where we
can take $\Delta_\gamma=\emptyset$ for all $\gamma$. Hence condition \ref{strengthened-4}
is trivially satisfied. Concluding, by
Cor.~\ref{cor:strenghtened} $\bis{rd}$ and $\bis{rw}$ are congruences for BPA$_{\varepsilon\delta\tau}$.


\paragraph{Binary Kleene star}

$t_1{}^\ast t_2$ 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$_{\varepsilon\delta\tau}$.\vspace*{-1.5mm}
{\small
\[
{\displaystyle\frac{x_1\trans \ell y}{x_1{}^\ast x_2\trans \ell y{\cdot}(x_1{}^\ast x_2)}}
\hspace{1.5cm}{\displaystyle\frac{x_2\trans{\alpha} y}{x_1{}^\ast x_2\trans{\alpha} y}}
\]
}

\vspace*{-1mm}

\noindent
Again, to show that $\bis{rd}$ and $\bis{rw}$ are congruences,
we argue that the resulting TSS satisfies the conditions of Def.~\ref{def:strengthened_delay_bisimulation_format}.
In \cite{FvGdW12} it was shown that it is in rooted $\eta$-bisimulation format,
if we take the arguments of binary Kleene star to be $\Lambda$-frozen and $\aleph$-liquid.
Since these arguments are $\Lambda$-frozen, condition
condition \ref{smooth} of Def.~\ref{def:smooth} is trivially satisfied.
Conditions \ref{strengthened-3}(a,b) of Def.~\ref{def:strengthened_delay_bisimulation_format} are satisfied by both rules, and
the second rule for binary Kleene star trivially satisfies condition \ref{strengthened-3}(c).
In view of this condition with regard to the first rule for binary Kleene star,
we mark the first argument of sequential composition by $\Delta_\ell$ for all $\ell\in {\it Act}\cup\{\tau\}$.
No other arguments are marked by the $\Delta_\gamma$.
Condition \ref{strengthened-4} of Def.~\ref{def:strengthened_delay_bisimulation_format} is satisfied with respect to the $\Delta_\gamma$.
(For this last condition it is essential that the first argument of sequential composition is not marked by $\Delta_\surd$.)
Concluding, by Cor.~\ref{cor:strenghtened} $\bis{rd}$ and $\bis{rw}$ are congruences for BPA$_{\varepsilon\delta\tau}$ with
binary Kleene star.


\paragraph{Initial priority}

Assume an ordering on actions.  $\theta(t)$ executes the transitions of $t$,
except that an initial transition \nietplat{$t\trans {\ell} t_1$} only gives
rise to an initial transition \nietplat{$\theta(t)\trans \ell t_1$}
if there does not exist an initial transition \nietplat{$t\trans{\ell'} t_2$} with $\ell<\ell'$.\vspace*{-1.5mm}
{\small
\[
\frac{x\trans \ell y~~~~~~~~x\ntrans{\ell'}\mbox{ for all } \ell'>\ell}{\theta(x)\trans \ell y}
\hspace{1.5cm}
\frac{x\trans \surd y}{\theta(x)\trans \surd y}
\]
}

\vspace*{-2mm}

\noindent
The argument of initial priority is $\Lambda$-frozen and $\aleph$-liquid.
In \cite{FvGdW12} it was observed that this TSS is in rooted $\eta$-bisimulation format,
irrespective of the ordering on actions.
If $\tau$ is greater than all actions in ${\it Act}$, then
both rules are negative-stable, because instances of the first
rule with a premise $x\ntrans{a}$ for some $a\in {\it Act}$ are guaranteed to also contain
$x\ntrans{\tau}$. In fact it is sufficient to require $\forall\ell:(\exists\ell':\ell'>\ell)\Rightarrow \tau>\ell$.

To show that $\bis{rd}$ and $\bis{rw}$ are congruences,
we argue that the TSS satisfies the conditions of Def.~\ref{def:strengthened_delay_bisimulation_format}.
Condition \ref{smooth} of Def.~\ref{def:smooth} is trivially satisfied by the rules for initial priority, because its argument is $\Lambda$-frozen.
Condition \ref{strengthened-3} of Def.~\ref{def:strengthened_delay_bisimulation_format} is satisfied by both rules for initial priority,
where we can take $\Delta_\gamma=\emptyset$ for all $\gamma$. In particular, condition \ref{strengthened-3}(b)
is satisfied by the first rule for initial priority, because this rule with $\ell=\tau$ contains no negative
premises. Since the $\Delta_\gamma$ are empty, condition \ref{strengthened-4} of Def.~\ref{def:strengthened_delay_bisimulation_format}
is trivially satisfied. Concluding, if $\tau$ is greater than all actions in ${\it Act}$,
$\bis{rd}$ and $\bis{rw}$ are congruences for BPA$_{\epsilon\delta\tau}$ with initial priority.

If $\tau$ is smaller than some $a$ in ${\it Act}$, then
$\bis{rd}$ and $\bis{rw}$ are not congruences for BPA$_{\epsilon\delta\tau}$ with initial priority.
For example, $\tau\cdot a\bis{rd}(\tau\cdot a)+a$.
However, $\theta(\tau\cdot a)\trans\tau a$ cannot be mimicked by $\theta((\tau\cdot a)+a)$,
as the latter term can only perform an $a$-transition to $\varepsilon$. So $\theta(\tau\cdot a)\notbis{rw}\theta((\tau\cdot a)+a)$.


\paragraph{Deadlock testing}

Finally we give an example outside the format from Def.~\ref{def:strengthened_delay_bisimulation_format}, but
within the more general format of Thm.~\ref{thm:rooted-delay-congruence}. The operator $f$
tests if its argument is a deadlock.\vspace*{-1.5mm}

{\small
\[
\frac{x\trans \alpha y}{f(x)\trans{{\it no}}\delta}
\hspace{2cm}
\frac{x\ntrans\alpha y \mbox{ for all }\alpha}{f(x)\trans{{\it yes}}\delta}
\]
}

\vspace*{-1mm}

\noindent
The argument of $f$ is $\Lambda$-frozen and $\aleph$-liquid. Clearly the first rule violates condition \ref{strengthened-3}
of Def.~\ref{def:strengthened_delay_bisimulation_format}.
\pagebreak[3]

The TSS is in rooted $\eta$-bisimulation format.
For both rules, we can take $H^d:=\emptyset$, while $r_\emptyset$ is the rule itself.\vspace{-1pt}
Furthermore, for the first rule, $r_{\{x\trans \alpha y\}}$ is $\frac{x\trans \tau y}{f(x)\trans{{\it no}}\delta}$.\vspace{1pt}
By Thm.~\ref{thm:manifest} this suffices to conclude that the TSS is delay resistant.
Hence, by Thms.~\ref{thm:rooted-delay-congruence} and \ref{thm:rooted-weak-congruence} $\bis{rd}$ and $\bis{rw}$ are congruences
for BPA$_{\epsilon\delta\tau}$ extended with $f$.

\section{Conclusions} \label{sec:conclusions}

In \cite{vGl11,FvGdW12} a method was presented to generalise any congruence format within ntyft format into a \emph{two-tiered} variant. The two-tiered versions of the congruence formats we presented generalise the formats in \cite{Blo95,vGl11}.
Ulidowski \cite{Uli92,UP02,UY00} proposed congruence formats for weak semantics with a different
treatment of divergence; these formats cover the (non-initial) priority operator, for which $\bis{rw}$ is not a congruence. The
TSSs of BPA$_{\epsilon\delta\tau}$, binary Kleene star and deadlock testing in Sect.\ \ref{sec:applications} are however outside those formats.

This research shows that it is worthwhile to study the interplay of structural operational semantics and modal logic. The modal characterisation of a process semantics turns out to be fundamental for its congruence properties. Admittedly, the whole story is quite technical and intricate. Partly this is because we build on a rich body of earlier work in the realm of structural operational semantics: the notions of well-supported proofs and complete TSSs from \cite{vGl04} (or actually \cite{GRS91} in logic programming); the ntyft format from \cite{Gro93,BolG96}; the transformation to ruloids, which for the main part goes back to \cite{FvG96}; and the work on modal decomposition and congruence formats from \cite{BFvG04} and \cite{FvGdW12}. Moreover, the proofs underlying the technical developments, which have been omitted from this extended abstract, are quite intricate. They are included in the full version of this paper \cite{FvG16}.

However, the bulk of this work can be reused in the context of other weak process semantics. This is witnessed by the fact that the congruence results for rooted delay and weak bisimilarity are obtained in an almost identical fashion, and build upon the congruence proof for rooted branching bisimilarity in \cite{FvGdW12}. The door is now open to derive congruence formats for a wide range of weak semantics. Further work is needed to cover the entire spectrum in \cite{vGl93}. Specifically, it would be interesting to extend the framework to divergence-sensitive semantics. For future research, it would also be interesting to see whether the bridge between modal logic and congruence formats could be employed in the realm of logics and semantics for e.g.\ probabilities and security. As a first step in this direction, in \cite{GF12} the decomposition method for Hennessy-Milner logic was lifted to probabilistic systems.


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

\bibitem{Blo95}
B.\ Bloom.
{\em Structural operational semantics for weak bisimulations.}
{\sl Theor.\ Comput.\ Sci.} 146:25-68, 1995.\vspace*{-0.37mm}

\bibitem{BFvG04}
B.\ Bloom, W.\ Fokkink, R.\ van Glabbeek.
{\em Precongruence formats for decorated trace semantics.}
{\sl ACM TOCL} 5:26-78, 2004.\vspace*{-0.37mm}

\bibitem{BIM95}
B.\ Bloom, S.\ Istrail, A.\ Meyer.
{\em Bisimulation can't be traced.}
{\sl J.\ ACM} 42:232-268, 1995.\vspace*{-0.37mm}

\bibitem{BolG96}
R.\ Bol, J.F.\ Groote.
{\em The meaning of negative premises in transition system specifications.}
{\sl J.\ ACM} 43:863-914, 1996\vspace*{-0.37mm}

\bibitem{Fok00}
W.\ Fokkink.
{\em Rooted branching bisimulation as a congruence.}
{\sl J.\ Comput.\ Syst.\ Sci.} 60:13-37, 2000.\vspace*{-0.37mm}

\bibitem{FvG96}
W.\ Fokkink, R.\ van Glabbeek.
{\em Ntyft/ntyxt rules reduce to ntree rules.}
{\sl Inform.\ Comput.} 126:1-10, 1996.\vspace*{-0.37mm}

\bibitem{FvG16}
W.\ Fokkink, R.\ van Glabbeek.
{\em Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity.}
Technical report 9351, NICTA, 2016.
\url{http://arxiv.org/abs/1604.07530}.\vspace*{-0.37mm}

\bibitem{FvGdW03}
W.\ Fokkink, R.\ van Glabbeek, P.\ de Wind.
{\em Compositionality of {H}ennessy-{M}ilner logic by structural operational semantics.}
{\sl Theor.\ Comput.\ Sci.} 354:421-440, 2006.\vspace*{-0.37mm}

\bibitem{FvGdW12}
W.\ Fokkink, R.\ van Glabbeek, P.\ de Wind.
{\em Divide and congruence: From decomposition of modal formulas to preservation of branching and $\eta$-bisimilarity.}
{\sl Inf.\ Comp.} 214:59-85, 2012.\vspace*{-0.37mm}

\bibitem{GF12}
D.\ Gebler, W.\ Fokkink.
{\em Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics.}
In {\sl CONCUR}, LNCS 7454, pp.\ 395-409.\ Springer, 2012.\vspace*{-0.37mm}

\bibitem{GRS91}
A.\ van Gelder, K.\ Ross, J.S.\ Schlipf.
{\em The well-founded semantics for general logic programs.}
{\em J.\ ACM} 38:620-650, 1991.\vspace*{-0.37mm}

\bibitem{vGl93}
R.\ van Glabbeek.
{\em The linear time-branching time spectrum {II}: The semantics of sequential systems with silent moves.}
In {\sl CONCUR}, LNCS 715, pp.\ 66-81.\ Springer, 1993.\vspace*{-0.37mm}

\bibitem{vGl04}
R.\ van Glabbeek.
{\em The meaning of negative premises in transition system specifications {II}.}
{\sl J.\ Logic Algebr.\ Progr.} 60/61:229-258, 2004.\vspace*{-0.37mm}

\bibitem{vGl11}
R.\ van Glabbeek.
{\em On cool congruence formats for weak bisimulations.}
{\sl Theor.\ Comput.\ Sci.}, 412:3283-3302, 2011.\vspace*{-0.37mm}

\bibitem{Gro93}
J.F.\ Groote.
{\em Transition system specifications with negative premises.}
{\sl Theor.\ Comput.\ Sci.} 118:263-299, 1993.\vspace*{-0.37mm}

\bibitem{GV92}
J.F.\ Groote, F.\ Vaandrager.
{\em Structured operational semantics and bisimulation as a congruence.}
{\sl Inform.\ Comput.} 100:202-260, 1992.\vspace*{-0.37mm}

\bibitem{HM85}
M.\ Hennessy, R.\ Milner.
{\em Algebraic laws for non-determinism and concurrency.}
{\sl J.\ ACM} 32:137-161, 1985.\vspace*{-0.37mm}

\bibitem{LL91}
K.\ Larsen, X.\ Liu.
{\em Compositionality through an operational semantics of contexts.}
{\sl J.\ Logic Comput.} 1:761-795, 1991.\vspace*{-0.37mm}

\bibitem{Mil81}
R.\ Milner.
{\em A modal characterisation of observable machine-behaviour.}
In {\sl CAAP}, LNCS 112, pp.\ 25-34.\ Springer, 1981.\vspace*{-0.37mm}

\bibitem{Mil89}
R.\ Milner.
{\em Communication and Concurrency.} Prentice Hall, 1989.\vspace*{-0.37mm}

\bibitem{Sim85}
R.\ de Simone.
{\em Higher-level synchronising devices in \textsc{Meije}-{SCCS}.}
{\sl Theor.\ Comput.\ Sci.} 37:245-267, 1985.\vspace*{-0.37mm}

\bibitem{Uli92}
I. Ulidowski.
{\em Equivalences on observable processes.}
In {\sl LICS}, pp.\ 148-159, IEEE, 1992.\vspace*{-0.37mm}

\bibitem{UP02}
I. Ulidowski, I. Phillips.
{\em Ordered SOS rules and process languages for branching and eager bisimulations.}
{\sl Inform.\ Comput.}, 178:180-213, 2002.\vspace*{-0.37mm}

\bibitem{UY00}
I. Ulidowski, S. Yuen.
{\em Process languages for rooted eager bisimulation.}
In {\sl CONCUR}, LNCS 1877, pp.\ 275-289, Springer, 2000.

\end{thebibliography}

\end{document}