\documentclass{entcs}
\usepackage[fleqn]{amsmath}
\headheight 10pt
\headsep 20pt
\footskip 20pt
\setlength{\topmargin}{-30pt}
\addtolength{\textheight}{25pt} 
\font\sc=cmcsc10 

\volume{Express}
\def\firstheadline{~\hfill~}
\def\firstfootline{~\hfill~}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% THE NEXT LINES DEFINE THE THEOREM ENVIRONMENTS from entcsmacros %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{theorem}{\vspace{-\lastskip}\par\addvspace{.6pc plus
    .2pc minus .1pc}\begin{thm}}{\end{thm}\par\addvspace{.6pc plus
    .2pc minus .1pc}}
\newenvironment{lemma}{\vspace{-\lastskip}\par\addvspace{.6pc plus
    .2pc minus .1pc}\begin{lem}}{\end{lem}\par\addvspace{.6pc plus
    .2pc minus .1pc}}
\newenvironment{corollary}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc}\begin{cor}}{\end{cor}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{definition}{\vspace{-\lastskip}\par \addvspace{.6pc
    plus .2pc minus .1pc}\begin{defn}\rm}{\end{defn}\par\addvspace{.6pc
    plus .2pc minus .1pc}}
\newenvironment{remark}{\vspace{-\lastskip}\par\addvspace{.6pc plus
    .2pc minus .1pc}\begin{rem}\rm}{\end{rem}\par\addvspace{.6pc plus
    .2pc minus .1pc}}
\newenvironment{proof}{\begin{pf}}{\qed\end{pf}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \newcommand{\Acts}[1][A]{\ensuremath{\mathalpha{#1}}}
  \newcommand{\act}[1]{\ensuremath{\mathalpha{#1}}}
    \newcommand{\acta}[1][]{\ensuremath{\act{a_{#1}}}}
  \newcommand{\sact}{\act{\tau}}
  \newcommand{\States}[1][S]{\ensuremath{\mathalpha{#1}}}
  \newcommand{\state}[1]{\ensuremath{\mathalpha{#1}}}
    \newcommand{\states}[1][]{\state{s_{#1}}}
    \newcommand{\statet}[1][]{\state{t_{#1}}}
    \newcommand{\stateu}[1][]{\state{u_{#1}}}
  \newcommand{\statemap}[1][\sigma]{\ensuremath{\mathalpha{#1}}}
  \newcommand{\brelsym}[1][\mathcal{R}]{\ensuremath{#1}}
  \newcommand{\brel}[1][{\brelsym}]{\ensuremath{\mathrel{#1}}}
   \newdimen\boxwdplusemdimen
   \def\arrow#1{{
     \boxwdplusemdimen=1em%
     \setbox0=\hbox{$\scriptstyle#1$}%
     \advance\boxwdplusemdimen by \wd0\relax%
     \ifdim\boxwdplusemdimen<16.11119pt%
       \boxwdplusemdimen=16.11119pt%
     \fi%
     \buildrel{#1}\over%
       {\setbox1=\hbox to \boxwdplusemdimen{\rightarrowfill}%
     \ht1=0.3em\relax\box1}%
   }}
   \makeatletter
   \def\twoheadrightarrowfill{$\m@th\smash-\mkern-7mu%
     \cleaders\hbox{$\mkern-2mu\smash-\mkern-2mu$}\hfill
     \mkern-7mu\mathord\twoheadrightarrow$}
   \makeatother
   \def\darrow#1{{
     \boxwdplusemdimen=1em%
     \setbox0=\hbox{$\scriptstyle#1$}%
     \advance\boxwdplusemdimen by \wd0\relax%
     \ifdim\boxwdplusemdimen<16.11119pt%
       \boxwdplusemdimen=16.11119pt%
     \fi%
     \buildrel{#1}\over%
       {\setbox1=\hbox to \boxwdplusemdimen{\twoheadrightarrowfill}%
     \ht1=0.3em\relax\box1}%
   }}
  \newcommand{\step}[1]{\ensuremath{\mathbin{\arrow{#1}}}}
  \newcommand{\stepsym}{\ensuremath{\mathalpha{\rightarrow}}}
  \newcommand{\ssteps}{\ensuremath{\mathbin{\darrow{}}}}
  \newcommand{\sstepssym}{\ensuremath{\mathbin{\twoheadrightarrow}}}
  \newcommand{\bisim}{%
    \setbox0=\hbox{\kern-.1ex{$\leftrightarrow$}\kern-.1ex}
    \setbox1=\vbox{\hbox{\raise .1ex \box0}\hrule}%
    \ensuremath{\mathrel{\hbox{\kern.1ex\box1\kern.1ex}}}
  }
  \newcommand{\bbisim}{%
    \setbox0=\hbox{\kern-.1ex{$\leftrightarrow$}\kern-.1ex}
    \setbox1=\vbox{\hbox{\raise .1ex \box0}\hrule}%
    \ensuremath{\mathrel{\hbox{\kern.1ex\box1\kern.1ex}_{b}}}
  }
  \newcommand{\wbbisimd}{%
    \setbox0=\hbox{\kern-.1ex{$\leftrightarrow$}\kern-.1ex}
    \setbox1=\vbox{\hbox{\raise .1ex \box0}\hrule}%
    \ensuremath{\mathrel{\hbox{\kern.1ex\box1\kern.1ex}^{\Delta_1}_{b}}}
  }
  \newcommand{\bbisimd}{%
    \setbox0=\hbox{\kern-.1ex{$\leftrightarrow$}\kern-.1ex}
    \setbox1=\vbox{\hbox{\raise .1ex \box0}\hrule}%
    \ensuremath{\mathrel{\hbox{\kern.1ex\box1\kern.1ex}^{\Delta_0}_{b}}}
  }
  \newcommand{\rbbisimd}{%
    \setbox0=\hbox{\kern-.1ex{$\leftrightarrow$}\kern-.1ex}
    \setbox1=\vbox{\hbox{\raise .1ex \box0}\hrule}%
    \ensuremath{\mathrel{\hbox{\kern.1ex\box1\kern.1ex}^{\Delta}_{b}}}
  }
  \newcommand{\bbisimsym}{\ensuremath{\mathalpha{\bbisim}}}
  \newcommand{\bbisimdsym}{\ensuremath{\mathalpha{\bbisimd}}}
  \newcommand{\wbbisimdsym}{\ensuremath{\mathalpha{\wbbisimd}}}
  \newcommand{\rbbisimdsym}{\ensuremath{\mathalpha{\rbbisimd}}}
  \newcommand{\N}{\ensuremath{\mathalpha{\omega}}}
  \newcommand{\bstate}[1]{\state{#1^\flat}}
  \newcommand{\astate}[1]{\state{#1^\sharp}}
  \newcommand{\bbd}{\mbox{BB$^\Delta$}}
  \newcommand{\bbdsc}{\ensuremath{\brel[\hat{\mathcal{R}}]}}
  \newcommand{\bbdscsym}{\ensuremath{\brelsym[\hat{\mathcal{R}}]}}
  \newcommand{\IFF}{iff}
  \newcommand{\all}[1]{\ensuremath{\mathalpha{\forall{#1}}}}
  \newcommand{\is}[1]{\ensuremath{\mathalpha{\exists{#1}}}}
  \newcommand{\Frm}[1][\Phi]{\ensuremath{\mathalpha{#1}}}
  \newcommand{\frm}[1][\varphi]{\ensuremath{\mathalpha{#1}}}
  \newcommand{\true}{\ensuremath{\mathalpha{\top}}}
  \newcommand{\compl}{\ensuremath{\mathalpha{\neg}}}
  \newcommand{\Meet}[1][]{\ensuremath{\bigwedge_{#1}}}
  \newcommand{\until}[1][\acta]{\ensuremath{\mathbin{\langle{#1}\rangle}}}
  \newcommand{\Div}{\ensuremath{\mathalpha{\Delta}}}
  \newcommand{\sat}{\ensuremath{\mathrel{\models}}}
  \newcommand{\equivalidsym}{\ensuremath{\mathalpha{\sim}}}
  \newcommand{\equivalid}{\ensuremath{\mathrel{\equivalidsym}}}
  \newcommand{\relcomp}{\ensuremath{\mathbin{;}}}
\newcommand{\runtil}[1][]{\ensuremath{\mathbin{#1}}}
\newcommand{\rDiv}{\ensuremath{\mathalpha{\Delta'}}}
\newcommand{\requivalidsym}{\ensuremath{\mathalpha{\sim'}}}
\newcommand{\requivalid}{\ensuremath{\mathrel{\requivalidsym}}}
\newcommand{\opt}[1]{\mbox{\tiny\rm(}#1\mbox{\tiny\rm)}} % optional action
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}}      % no vertical space
\newcommand{\C}{\ensuremath{\mathcal{C}}}
\newcommand{\cc}{\equiv_c}
\newcommand{\ccd}{\equiv_c^\Delta}
\newcommand{\ccsym}{\ensuremath{\mathalpha{\cc}}}
\newcommand{\ccdsym}{\ensuremath{\mathalpha{\ccd}}}

\def\lastname{van Glabbeek, Luttik \& Tr\v{c}ka}
\begin{document}
\begin{frontmatter}
  \title{Branching Bisimulation with Explicit Divergence}
  \author{Rob van Glabbeek\thanksref{rvg}}
  \address{National ICT Australia, Sydney, Australia}
  \address{School of Computer Science and Engineering,
           Univ.\ of New South Wales, Sydney}
  \author{Bas Luttik\thanksref{spl}}
  \address{Dept.\ of Math.\ and Comput.\ Sci.\\
           Technische Universiteit Eindhoven,
           The Netherlands}
  \address{CWI, The Netherlands}
  \author{Nikola Tr\v{c}ka\thanksref{nt}}
  \address{Dept.\ of Math.\ and Comput.\ Sci.\\
           Technische Universiteit Eindhoven,
           The Netherlands}
  \thanks[rvg]{Email: \texttt{rvg@cs.stanford.edu}}
  \thanks[spl]{Email: \texttt{s.p.luttik@tue.nl}}
  \thanks[nt]{Email: \texttt{n.trcka@tue.nl}}
\begin{abstract} 
  We consider the relational characterisation of branching
  bisimulation with explicit divergence. We prove that it is an
  equivalence relation and that it coincides with the
  original definition of branching bisimulation with explicit
  divergence in terms of coloured traces. We also establish a
  correspondence with an action-based modal logic with until modality and
  explicit divergence.
\end{abstract}
\begin{keyword}
  Branching bisimulation, divergence, coloured traces.
\end{keyword}
\end{frontmatter}

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

\emph{Branching bisimulation with explicit divergence} ($\bbd$)
\cite{GW96}, is the coarsest semantic equivalence on labelled
transition systems with silent moves that is a congruence for parallel
composition as found in process algebras like CCS, CSP or ACP, and
only equates processes satisfying the same CTL$^*$ formulas without
the nexttime operator \cite{CTLd}.
It is also the finest equivalence in the \emph{linear time --
branching time spectrum} of \cite{Gla93}.

The original definition of $\bbd$, in terms of \emph{coloured
traces}, stems from \cite{GW96}. In \cite{Gla93},
$\bbd$ is defined in terms of a modal and a relational
characterisation, which are claimed to coincide with each other and
with the original notion from \cite{GW96}. Of these three definitions
of $\bbd$, the relational characterisation from \cite{Gla93} is
the most concise one, in the sense that it requires the least amount
of auxiliary concepts. Moreover, this definition is most in the style
of the standard definitions of other kinds of bisimulation, found
elsewhere in the literature. For these reasons, it is tempting to take
it as standard definition.

Although it is not hard to establish that the modal characterisation from
\cite{Gla93} is correct, in the sense that it defines an equivalence
that coincides with $\bbd$ of \cite{GW96}, it is not at all trivial
to establish that the same holds for the relational characterisation
from \cite{Gla93}. If fact, it is non-trivial that this relation
is an equivalence, and that it satisfies the so-called
\emph{stuttering property}. Once these properties have been
established, it follows that the notion coincides with $\bbd$ of
\cite{GW96}.

In this paper we establish that the relational characterisation of
$\bbd$ from \cite{Gla93} yields an equivalence relation that has the
stuttering property and hence coincides with $\bbd$.
We also explore other relational characterisations of $\bbd$.
Finally we establish agreement between of the relational and modal
characterisation from \cite{Gla93}, and also provide a
different modal characterisation of $\bbd$, in the style of \cite{DV95}.


  \section[Relational characterisations of BB]
          {Relational characterisations of $\bbd$}

  We presuppose a set $\Acts$ of \emph{actions} with a special element
  $\sact\in\Acts$.
  Furthermore, we presuppose a \emph{labelled transition system}
    $(\States,\stepsym)$
  with labels from $\Acts$, i.e., $\States$ is a set and
  $\stepsym\subseteq\States\times\Acts\times\States$ is a
  \emph{transition relation} on $\States$.
  Let $\states,\state{s'}\in\States$ and $\acta\in\Acts$.
  We write $\states\step{\acta}\state{s'}$ for
    $(\states,\acta,\state{s'})\in\stepsym$;
  we abbreviate the statement
   `$\states\step{\acta}\state{s'}$
      or ($\acta=\sact$ and $\states=\state{s'}$)'
  by \plat{$\states\step{\opt{\acta}}\state{s'}$};
  and we denote by $\sstepssym$ the
  reflexive-transitive closure of the binary relation $\step{\sact}$
  on $\States$.

  \begin{definition}\cite{Gla93} \label{def:bbisimd}
    A symmetric binary relation $\brelsym$ on $\States$ is a
    \emph{branching bisimulation with explicit divergence} if it
    satisfies the following two conditions for all
    $\states,\statet\in\States$ and $a\in\Acts$:
    \begin{enumerate}
    \renewcommand{\theenumi}{T}
    \renewcommand{\labelenumi}{(\theenumi)}
    \item \label{cnd:stepsim}
      if $\states\brel\statet$ and $\states\step{\acta}\state{s'}$ for
      some state $\state{s'}$,
      then there exist states $\state{t'}$ and $\state{t''}$
      such that
        \plat{$\statet\ssteps{}\state{t''}\step{\opt{\acta}}\state{t'}$},
        $\states\brel\state{t''}$
      and
        $\state{s'}\brel\state{t'}$; and
  \renewcommand{\theenumi}{D}
  \renewcommand{\labelenumi}{(\theenumi)}
  \item \label{cnd:rvgdivsim}
    if $\states\brel\statet$
    and there is an infinite sequence of states
      $(\states[k])_{k\in\N}$
    such that
      $\states=\states[0]$,
      $\states[k]\step{\sact}\states[k+1]$
    and
      $\states[k]\brel\statet$ for all $k\in\N$,
    then there exists an infinite sequence of states
      $(\statet[l])_{l\in\N}$
    such that
      $\statet=\statet[0]$,
      $\statet[l]\step{\sact}\statet[l+1]$ for all $l\in\N$,
    and
      $\states[k]\brel\statet[l]$ for all $k,l\in\N$.
    \end{enumerate}
    We write $\states\rbbisimd\statet$ if there exists a branching
    bisimulation with explicit divergence $\brelsym$ such that
    $\states\brel\statet$.
  \end{definition}

\noindent
The relation $\bbisimsym$, defined as above but without clause (D), is
the relational characterisation of \emph{branching bisimulation equivalence},
given in \cite{Gla93}. As shown in \cite{GW96,Gla93,Bas96}, it yields
the same concept of branching bisimulation equivalence as the original
definition of \cite{GW96}. In \cite{Gla93} it was claimed that the
notion $\rbbisimd$ defined above coincides with \emph{branching
bisimulation equivalence with explicit divergence} as defined
earlier in \cite{GW96}. In this paper we will substantiate this claim.
On the way to this end, we will show that $\rbbisimd$ is an equivalence
relation, has the so-called \emph{stuttering property}, and can
equivalently be defined by replacing (\ref{cnd:rvgdivsim}) by any of
the following alternatives:
  \begin{enumerate}
   \renewcommand{\theenumi}{D$_0\hspace{-1pt}$}
   \renewcommand{\labelenumi}{(\theenumi)}
   \addtocounter{enumi}{1}
    \item \label{cnd:divsim}
      if $\states\brel\statet$
      and there is an infinite sequence of states
        $(\states[k])_{k\in\N}$
      such that
         $\states=\states[0]$,
         $\states[k]\step{\sact}\states[k+1]$
      and
         $\states[k]\brel\statet$ for all $k\in\N$,
      then there exists a state $\state{t'}$
      such that
        $\statet\step{\sact}\state{t'}$
      and
        $\states[k]\brel\state{t'}$ for some $k\in\N$.
   \renewcommand{\theenumi}{D$'_1\hspace{-1pt}$}
   \item \label{cnd:newdivsimshort}
       if $\states\brel\statet$
       and there is an infinite sequence of states
         $(\states[k])_{k\in\N}$
       such that
          $\states=\states[0]$
      and
          $\states[k]\step{\sact}\states[k+1]$ for all $k\in\N$,
      then there exists a state $\state{t'}$
      such that
        $\statet\step{\sact}\state{t'}$
      and
        $\states[k]\brel\state{t'}$ for some $k\in\N$.
   \renewcommand{\theenumi}{D$_1\hspace{-1pt}$}
   \item \label{cnd:newdivsim}
       if $\states\brel\statet$
       and there is an infinite sequence of states
         $(\states[k])_{k\in\N}$
       such that
          $\states=\states[0]$
       and
          $\states[k]\step{\sact}\states[k+1]$ for all $k\in\N$,
       then there exist an infinite sequence of states
         $(\statet[l])_{l\in\N}$
       and a mapping
         $\statemap\!:\N\!\rightarrow\!\N$
       such that
         $\statet=\statet[0]$,
         $\statet[l]\step{\sact}\statet[l+1]$
       and
         $\states[\statemap(l)]\brel\statet[l]$ for all $l\!\in\!\N$.
  \end{enumerate}
  We write $\states\bbisimd\statet$, respectively
  $\states\wbbisimd\statet$, if there exists a symmetric binary
  relation $\brelsym$ satisfying (\ref{cnd:stepsim})
  and (\ref{cnd:divsim}), respectively (\ref{cnd:newdivsim}), such
  that $\states\brel\statet$.
  Note that (\ref{cnd:divsim}) is a weaker requirement than either
  (\ref{cnd:rvgdivsim}) or (\ref{cnd:newdivsimshort}); hence
  $\rbbisimdsym \subseteq \bbisimdsym$ and
  $\wbbisimdsym \subseteq \bbisimdsym$.
  Condition (\ref{cnd:divsim}) appears in a definition of
  divergence-sensitive stuttering simulation in \cite{Nej03}.
  Condition (\ref{cnd:newdivsim}) is a technically convenient
  reformulation of (\ref{cnd:newdivsimshort}) that shows more clearly
  how the condition preserves \emph{divergence} (infinite sequences of
  $\sact$-transitions).

  \section{Equivalence proof}

  Our goal is now to prove that $\rbbisimdsym$ is an equivalence
  relation. To this end, we first show that $\wbbisimdsym$ is an
  equivalence relation. In fact, we have carefully chosen condition
  (\ref{cnd:newdivsim}) to enable a direct proof of this fact.  Using
  this, we obtain $\wbbisimdsym \subseteq \rbbisimdsym$.  Then, we
  define the notion of \emph{stuttering closure} and use it to
  establish $\bbisimdsym \subseteq \wbbisimdsym$.  Together with the
  observation $\rbbisimdsym \subseteq \bbisimdsym$ made above, the
  cycle of inclusions yields that the relations $\rbbisimdsym$,
  $\bbisimdsym$ and $\wbbisimdsym$ coincide. Therefore,
  $\rbbisimdsym$ is an equivalence relation.  We have not been able to
  find a less roundabout way to obtain this result.
  The material needed for the equivalence proof also yields that
  $\rbbisimdsym$ has the stuttering property.

  \subsection[]{$\wbbisimdsym$ is an equivalence relation}

The proofs below are rather straightforward. Nevertheless, the
proof strategy employed for both Lemma~\ref{lem:relunion}
and~\ref{lem:relcomp} would fail for $\rbbisimdsym$ and $\bbisimdsym$.
It is for this reason that we present all detail.

  \begin{lemma} \label{lem:relunion}
  \mbox{}
  \begin{enumerate}
  \renewcommand{\theenumi}{\roman{enumi}}
  \renewcommand{\labelenumi}{(\theenumi)}
  \item
    If relations $\brelsym_i$ satisfies {\rm (\ref{cnd:stepsim})} for
    $i\in I$, then so does their union $\bigcup_{i\in I}\brelsym_i$.
  \item \label{lem:relunion:item:newdivsim}
    If relations $\brelsym_i$ satisfies {\rm (\ref{cnd:newdivsim})} for
    $i\in I$, then so does their union $\bigcup_{i\in I}\brelsym_i$.
  \end{enumerate}
  \end{lemma}
  \noindent
  {\bf Proof.}
  Let $\brelsym=\bigcup_{i\in I}\brelsym_i$.
  \begin{enumerate}
  \renewcommand{\theenumi}{\roman{enumi}}
  \renewcommand{\labelenumi}{(\theenumi)}
  \item Suppose that $\brelsym_i$ satisfies
    (\ref{cnd:stepsim}) for $i\!\in\! I$.
    To prove that $\brelsym$ also satisfies (\ref{cnd:stepsim}),
    suppose that
      $\states\brel\statet$
    and
      $\states\step{\acta}\state{s'}$ for some state $\state{s'}$.
    Then $\states\brel_i\statet$ for some $i\in I$.
    Since $\brelsym_i$ satisfies
    (\ref{cnd:stepsim}), it follows that there are states
    $\state{t'}$ and $\state{t''}$ such that
      \plat{$\statet\ssteps{}\state{t''}\step{\opt{\acta}}\state{t'}$},
      $\states\brel_i\state{t''}$ 
    and
      $\state{s'}\brel_i\state{t'}$,
    and hence $\states\brel\state{t''}$ and
    $\state{s'}\brel\state{t'}$.
   \item Suppose that $\brelsym_i$ satisfies
     (\ref{cnd:newdivsim}) for $i\!\in\! I$.
     To prove that $\brelsym$ satisfies (\ref{cnd:newdivsim}), suppose
     that $\states\brel\statet$ and that there is an infinite sequence
     of states $(\states[k])_{k\in\N}$ such that
       $\states=\states[0]$
     and
       $\states[k]\step{\sact}\states[k+1]$.
     From $\states\brel\statet$ it follows that
     $\states\brel_i\statet$ for some $i\!\in\! I$.
     By (\ref{cnd:newdivsim}) there exist an infinite sequence of states
       $(\statet[l])_{l\in\N}$
     and a mapping
       $\statemap:\N\rightarrow\N$
     such that
       $\statet=\statet[0]$,
       $\statet[l]\step{\sact}\statet[l+1]$
     and
       $\states[\statemap(l)]\brel_i\statet[l]$ for all $l\in\N$,
     and from the latter it follows that
       $\states[\statemap(l)]\brel\statet[l]$.
  \qed
  \end{enumerate}

  \begin{lemma} \label{lem:isync}
    Let $\brelsym$ be a binary relation that satisfies
    {\rm (\ref{cnd:stepsim})}.
    If $\states\brel\statet$ and $\states\ssteps{}\state{s'}$,
    then there is a state $\state{t'}$ such that
      $\statet\ssteps{}\state{t'}$
    and
      $\state{s'}\brel\state{t'}$.
  \end{lemma}
  \begin{proof}
    Let $\states[0],\dots,\states[n]$ be states such that
      $\states=
         \states[0]\step{\sact}\cdots\step{\sact}\states[n]
           =\state{s'}$.
    By (\ref{cnd:stepsim}) and a straightforward
    induction on $n$ there exist states
      $\statet[0],\dots,\statet[n]$
    such that
      $\statet=
         \statet[0]\ssteps{}\cdots\ssteps{}\statet[n]
           =\state{t'}$
    and $\states[i]\brel\statet[i]$ for all $i\leq n$.
  \end{proof}

  \begin{lemma} \label{lem:relcomp}
  \mbox{}
  \begin{enumerate}
  \renewcommand{\theenumi}{\roman{enumi}}
  \renewcommand{\labelenumi}{(\theenumi)}
  \item
    If $\brelsym_1$ and $\brelsym_2$ both satisfy
    {\rm (\ref{cnd:stepsim})}, then so does their composition
    $\brelsym_1\relcomp\brelsym_2$.
  \item
    If $\brelsym_1$ and $\brelsym_2$ both satisfy
    {\rm (\ref{cnd:newdivsim})}, then so does their composition 
    $\brelsym_1\relcomp\brelsym_2$.
  \end{enumerate}
  \end{lemma}
  \noindent
  {\bf Proof.}
    Let $\brelsym=\brelsym_1\relcomp\brelsym_2$.
  \begin{enumerate}
  \renewcommand{\theenumi}{\roman{enumi}}
  \renewcommand{\labelenumi}{(\theenumi)}
  \item To prove that $\brel$ satisfies
    (\ref{cnd:stepsim}), suppose $\states\brel\stateu$ and
    $\states\step{\acta}\state{s'}$.
    Then there exists a state $\statet$ such that
        $\states\brel_1\statet$ and $\statet\brel_2\stateu$.
    Since $\brelsym_1$ satisfies (\ref{cnd:stepsim}), there exist
    states $\state{t'}$ and $\state{t''}$ such that
        \plat{$\statet\ssteps{}\state{t''}\step{\opt{\acta}}\state{t'}$},
        $\states\brel_1\state{t''}$
    and
        $\state{s'}\brel_1\state{t'}$.
    By Lemma \ref{lem:isync} there is a state $\state{u''}$
    such that
      $\stateu\ssteps{}\state{u''}$
    and
      $\state{t''}\brel_2\state{u''}$.
    We now distinguish two cases:
    \begin{enumerate}
    \item Suppose that $\acta=\sact$ and $\state{t''}=\state{t'}$.
      Then $\stateu\ssteps{}\state{u''}\step{\opt{\acta}}\state{u''}$,
      from 
        $\states\brel_1\state{t''}$ and $\state{t''}\brel_2\state{u''}$
      it follows that
        $\states\brel\state{u''}$,
      and from
        $\state{s'}\brel_1\state{t'}$ and $\state{t'}\brel_2\state{u''}$
      it follows that
        $\state{s'}\brel\state{u''}$.
    \item Suppose that $\statet''\step{\acta}\state{t'}$.
      Then there exist states $\state{u'''}$ and $\state{u'}$ such
      that $\state{u''}\ssteps{}\state{u'''}\step{\opt{\acta}}\state{u'}$,
        $\state{t''}\brel_2\state{u'''}$
      and
        $\state{t'}\brel_2\state{u'}$.
      So, \plat{$\state{u}\ssteps{}\state{u'''}\step{\opt{\acta}}\state{u'}$},
      from
        $\states\brel_1\state{t''}$ and $\state{t''}\brel_2\state{u'''}$
      it follows that
        $\states \brel_1\relcomp\brel_2 \state{u'''}$,
      and from
        $\state{s'}\brel_1\state{t'}$ and $\state{t'}\brel_2\state{u'}$
      it follows that
        $\state{s'}\brel\state{u'}$.
    \end{enumerate}
  \item To prove that $\brel$ satisfies (\ref{cnd:newdivsim}),
    suppose that
        $\states\brel\stateu$
    and that there is an infinite sequence of states 
        $(\states[k])_{k\in\N}$
    such that
        $\states=\states[0]$,
        $\states[k]\step{\sact}\states[k+1]$ for all $k\in\N$.
    As before, there exists a state $\statet$ such that
        $\states\brel_1\statet$ and $\statet\brel_2\stateu$.
    From $\states\brel_1\statet$ it follows that there exist an
    infinite sequence of states
      $(\statet[l])_{l\in\N}$
    and a mapping
      $\statemap:\N\rightarrow\N$
    such that
      $\statet=\statet[0]$,
      $\statet[l]\step{\sact}\statet[l+1]$
    and
      $\states[\statemap(l)]\brel\statet[l]$ for all $l\in\N$.
    Hence, since $\statet\brel_2\stateu$, it follows that there exist
    an infinite sequence of states
      $(\stateu[m])_{m\in\N}$
    and a mapping
      $\statemap[\rho]:\N\rightarrow\N$
    such that
      $\stateu=\stateu[0]$,
      \plat{$\stateu[m]\step{\sact}\stateu[m+1]$}
    and
      $\statet[{\statemap[\rho](m)}]\brel_2\stateu[m]$ for all $m\in\N$.
    Clearly,
      $\states[\statemap({\statemap[\rho]}(m))]\brel\stateu[m]$
    for all $m\in\N$.
  \qed
  \end{enumerate}

  \begin{theorem} \label{theo:wbbisimdeq}
    $\wbbisimd$ is an equivalence relation.
  \end{theorem}
  \begin{proof}
    The diagonal on $\States$ (i.e., the binary relation
    $\{(\states,\states)\mid\states\in\States\}$) is a symmetric
    relation that satisfies (\ref{cnd:stepsim}) and
    (\ref{cnd:newdivsim}), so $\wbbisimd$ is reflexive.
    Furthermore, that $\wbbisimd$ is symmetric is immediate from the
    required symmetry of the witnessing relation.

    To prove that $\wbbisimd$ is transitive, suppose
    $\states\wbbisimd\statet$ and $\statet\wbbisimd\stateu$.
    Then there exist symmetric binary relations $\brelsym_1$ and
    $\brelsym_2$ satisfying (\ref{cnd:stepsim}) and
    (\ref{cnd:newdivsim}) such that
      $\states\brel_1\statet$ and $\statet\brel_2\stateu$.
    The relation
      $\brelsym={(\brel_1\relcomp\brel_2)\cup(\brel_2\relcomp\brel_1)}$
    is clearly symmetric and, by Lemmas \ref{lem:relunion} and
    \ref{lem:relcomp}, satisfies (\ref{cnd:stepsim}) and
    (\ref{cnd:newdivsim}).
    Hence, since $\states\brel\stateu$, it follows that
    $\states\wbbisimd\stateu$.
  \end{proof}

\subsection[]{$\wbbisimdsym$ is included in $\rbbisimdsym$}

  \begin{lemma} \label{lem:wbbisimdlargest}
    The relation $\wbbisimdsym$ satisfies {\rm (\ref{cnd:stepsim})} and
    {\rm (\ref{cnd:newdivsim})}.
  \end{lemma}
  \begin{proof}
    By definition, $\wbbisimdsym$ is the union of all symmetric relations
    satisfying (\ref{cnd:stepsim}) and (\ref{cnd:newdivsim}), so, using
    Lemma~\ref{lem:relunion}, $\wbbisimdsym$ itself
    satisfies (\ref{cnd:stepsim}) and (\ref{cnd:newdivsim}).
  \end{proof}
    \noindent
    In fact, $\wbbisimdsym$ is the largest symmetric binary relation
    satisfying (\ref{cnd:stepsim}) and (\ref{cnd:newdivsim}).

  \begin{lemma} \label{lem:wbbisimdrvgdivsim}
    The relation $\wbbisimdsym$ satisfies {\rm (\ref{cnd:rvgdivsim})}.
  \end{lemma}
  \begin{proof}
    Suppose that
      $\states\wbbisimd\statet$
    and that there is an infinite sequence of states
      $(\states[k])_{k\in\N}$
    such that
      $\states=\states[0]$,
      $\states[k]\step{\sact}\states[k+1]$
    and
      $\states[k]\wbbisimd\statet$ for all $k\in\N$.
    According to Lemma~\ref{lem:wbbisimdlargest}, the relation
    $\wbbisimdsym$ satisfies (\ref{cnd:newdivsim}), so there exist an
    infinite sequence of states
      $(\statet[l])_{l\in\N}$
    and a mapping
      $\statemap:\N\rightarrow\N$
    such that
      $\statet=\statet[0]$,
      $\statet[l]\step{\sact}\statet[l+1]$
    and
      $\states[\statemap(l)]\wbbisimd\statet[l]$ for all $l\in\N$.
    By Theorem~\ref{theo:wbbisimdeq}, $\wbbisimdsym$ is an equivalence
    relation, so it follows from 
      $\states[k]\wbbisimd\statet$,
      $\states[\statemap(l)]\wbbisimd\statet$
    and
      $\states[\statemap(l)]\wbbisimd\statet[l]$
    that
      $\states[k]\wbbisimd\statet[l]$ for all $k,l\in\N$.
    Hence $\wbbisimdsym$ satisfies (\ref{cnd:rvgdivsim}).
  \end{proof}

  \begin{theorem}
    $\wbbisimdsym\subseteq\rbbisimdsym$.
  \end{theorem}
  \begin{proof}
    By Theorem~\ref{theo:wbbisimdeq}, the relation $\wbbisimdsym$ is symmetric.
    By Lemma~\ref{lem:wbbisimdlargest}, it satisfies (\ref{cnd:stepsim}), and
    by Lemma~\ref{lem:wbbisimdrvgdivsim} it satisfies
    (\ref{cnd:rvgdivsim}).  So $\wbbisimdsym$ is a branching
    bisimulation with explicit divergence, and hence
    $\states\wbbisimd\statet$ implies $\states\rbbisimd\statet$.
  \end{proof}

\subsection[]{Stuttering closure}

  \begin{definition} \label{df:stuttering}
    A binary relation $\brelsym$
    has the \emph{stuttering property} if, whenever
    $\statet[0]\step{\sact}\cdots\step{\sact}\statet[n]$,
    $\states\brel\statet[0]$ and
    $\states\brel\statet[n]$, then
    $\states\brel\statet[i]$ for all $i=0,\dots,n$.
  \end{definition}

  \noindent
  The following converts any binary relation $\brelsym$ on $\States$
  into a larger relation $\bbdscsym$ that has the stuttering property.

  \begin{definition}
    Let $\brelsym$ be a binary relation on $\States$.
    The \emph{stuttering closure} $\bbdscsym$ of $\brelsym$ is defined by
    \begin{equation*}
      \bbdscsym =
        \{(\states,\statet)
             \mid \is{\bstate{s},\astate{s},\bstate{t},\astate{t}\in\States}.\
                    \bstate{s}\ssteps{}\state{s}\ssteps{}\astate{s}\ \&\
                    \bstate{t}\ssteps{}\state{t}\ssteps{}\astate{t}\ \&\
                    \bstate{s}\brel\astate{t}\ \&\
                    \astate{s}\brel\bstate{t}
        \}
    \enskip.
    \end{equation*}
  \end{definition}

  \noindent
  Clearly $\brelsym \subseteq \bbdscsym$.
  We establish a few basic properties of the stuttering closure.

  \begin{lemma} \label{lem:stuttering}
    The stuttering closure $\bbdscsym$ of a binary relation $\brelsym$
    has the \emph{stuttering property}.
  \end{lemma}
  \begin{proof}
    Suppose that
      $\statet[0]\step{\sact}\cdots\step{\sact}\statet[n]$,
      $\states\bbdsc\statet[0]$
    and
      $\states\bbdsc\statet[n]$.
    Then, on the one hand, there exist states $\astate{s}$ and
    $\bstate{t_0}$ such that
      $\states\ssteps{}\astate{s}$,
      $\bstate{t_0}\ssteps{}\statet[0]$
    and
      $\astate{s}\brel\bstate{t_0}$,
    and on the other hand there exist states $\bstate{s}$ and
    $\astate{t_n}$ such that
      $\bstate{s}\ssteps{}\states$,
      $\statet[n]\ssteps{}\astate{t_n}$
    and
      $\bstate{s}\brel\astate{t_n}$.
    Now, since
      $\bstate{s}\ssteps{}\states\ssteps{}\astate{s}$
    and
      $\bstate{t_0}\ssteps{}\statet[i]\ssteps{}\astate{t_n}$
       for all $i=0,\dots,n$,
    it follows that $\states\bbdsc\statet[i]$.
  \end{proof}

  \begin{lemma} \label{lem:bbdscsym}
    The stuttering closure $\bbdsc$ of a symmetric binary relation
    $\brelsym$ is symmetric.
  \end{lemma}
  \begin{proof}
    Suppose $\states\bbdsc\statet$; then there exist states
    $\bstate{s}$, $\astate{s}$, $\bstate{t}$ and $\astate{t}$ such
    that
      $\bstate{s}\ssteps{}\states\ssteps{}\astate{s}$,
      $\bstate{t}\ssteps{}\statet\ssteps{}\astate{t}$,
      $\bstate{s}\brel\astate{t}$
    and
      $\astate{s}\brel\bstate{t}$.
    Since $\brel$ is symmetric, it follows that
      $\bstate{t}\brel\astate{s}$
    and
      $\astate{t}\brel\bstate{s}$.
    Hence $\statet\bbdsc\states$.
  \end{proof}

  \begin{lemma} \label{lem:bbdscsync}
    Let $\bbdscsym$ be the stuttering closure of $\brelsym$.
    If $\brelsym$ satisfies {\rm (\ref{cnd:stepsim})} and
    $\states\bbdsc\statet$, then there exists $\state{t'}$ such
    that $\statet\ssteps{}\state{t'}$ and $\state{s}\brel\state{t'}$.
  \end{lemma}
  \begin{proof}
    Suppose $\states\bbdsc\statet$; then there exist states
    $\bstate{s}$, $\astate{s}$, $\bstate{t}$ and $\astate{t}$ such
    that
      $\bstate{s}\ssteps{}\states\ssteps{}\astate{s}$,
      $\bstate{t}\ssteps{}\statet\ssteps{}\astate{t}$,
      $\bstate{s}\brel\astate{t}$
    and
      $\astate{s}\brel\bstate{t}$.
    From $\bstate{s}\brel\astate{t}$ and
    $\bstate{s}\ssteps{}\states$
    it follows by Lemma~\ref{lem:isync} that there exists
    $\state{t'}$ such that $(\statet\ssteps{}\!)\,\astate{t}\ssteps{}t'$ and
    $\states\brel\state{t'}$.
  \end{proof}

  \begin{lemma} \label{lem:bbdscstepsim}
    If $\brelsym$ satisfies {\rm (\ref{cnd:stepsim})}, then so does
    its stuttering closure $\bbdscsym$.
  \end{lemma}
  \begin{proof}
    Suppose that $\states\bbdsc\statet$ and that
    $\states\step{\acta}\state{s'}$ for some $\state{s'}$.
    Then by Lemma~\ref{lem:bbdscsync} there exists $\state{t^{\dagger}}$
    such that $\statet\ssteps{}\state{t^{\dagger}}$ and
    $\states\brel\state{t^{\dagger}}$.
    Hence, since $\states\step{\acta}\state{s'}$, it follows by
    (\ref{cnd:stepsim}) that there exist states $\state{t''}$ and
    $\state{t'}$ such that
    \begin{equation*}
      (\statet\ssteps{}\!)\,
      \state{t^{\dagger}}\ssteps{}\state{t''}\step{\opt{\acta}}\state{t'},\
      \states\brel\state{t''}\
    \text{and}\
      \state{s'}\brel\state{t'}
    \enskip.
    \end{equation*}
    Now, $\states\brel\state{t''}$ and $\state{s'}\brel\state{t'}$
    respectively imply $\states\bbdsc\state{t''}$ and
    $\state{s'}\bbdsc\state{t'}$.
  \end{proof}

\subsection[]{Closing the cycle of inclusions}

  \begin{lemma} \label{lem:bbdscnewdivsim}
    If $\brelsym$ satisfies  {\rm (\ref{cnd:stepsim})} and\
    {\rm (\ref{cnd:divsim})}, then $\bbdscsym$ satisfies
    {\rm (\ref{cnd:newdivsimshort})}.
  \end{lemma}

  \begin{proof}
    Suppose that $\states\bbdsc\statet$ and there exists an infinite
    sequence of states $(\states[k])_{k\in\N}$ such that
      $\states=\states[0]$
    and
      $\states[k]\step{\sact}\states[k+1]$ for all $k\in\N$.
    We have to show that there exists a state $\state{t'}$ such that
    $\statet\step{\sact}\state{t'}$ and $\states[k]\bbdsc\state{t'}$
    for some $k\in\N$.

    As $\states\bbdsc\statet$, by Lemma~\ref{lem:bbdscsync}
    there exist $\statet[0],\dots,\statet[n]$ such that
      $\statet=\statet[0]
                 \step{\sact}\cdots\step{\sact}
               \statet[n]$
    and
      $\states\brel\statet[n]$.
    By Lemma~\ref{lem:stuttering},
    $\states\bbdsc\statet[i]$ for all $i=0,\dots,n$,
    so if $n>0$, then we can take $\state{t'}=\statet[1]$.
    We proceed with the assumption that $n=0$; so
    $\states\brel\statet$. If $\states[k]\brel\statet$ for all
    $k\!\in\!\N$, then a state $\state{t'}$ with the desired properties
    exists by condition~(\ref{cnd:divsim}).
    The case that remains is where there is a $k_0\in\N$ such that
    $\states[k]\brel\statet$ for all $k\leq k_0$
    while $\states[k_0+1]$ and $\state{t}$ are \emph{not} related
    by $\brel$.
    Since $\states[k_0]\brel\statet$ and
    $\states[k_0]\step{\sact}\states[k_0+1]$, by
    condition~(\ref{cnd:stepsim}) of Definition~\ref{def:bbisimd}
    there exist states
      $\statet[0],\dots,\statet[m],\statet[m+1]$
    such that
      \plat{$\statet=\statet[0]
                 \step{\sact}\cdots\step{\sact}
               \statet[m]\step{\opt{\sact}}\statet[m+1]$},
      $\states[k_0]\brel\statet[m]$
    and
      $\states[k_0+1]\brel\statet[m+1]$.
    Since $\states[k_0+1]$ and $\state{t}$ are not related by
    $\brel$, it follows that $\statet[0]\not=\statet[m+1]$,
    so either $m>0$ or $\statet[m]\step{\sact}\statet[m+1]$.
    In case $m>0$, since
      $\states[k_0]\bbdsc\statet[0]$
    and
      $\states[k_0]\bbdsc\statet[m]$,
    by Lemma~\ref{lem:stuttering} it follows that
    $\states[k_0]\bbdsc\statet[1]$, so we can take
    $\state{t'}=\statet[1]$.
    In case $m=0$ and
      $\statet=\statet[m]\step{\sact}\statet[m+1]$,
    we can take $\state{t'}=\statet[m+1]$.
  \end{proof}

  \begin{lemma} \label{lem:short}
    A binary relation $\brelsym$ satisfies {\rm (\ref{cnd:newdivsim})} iff
    it satisfies {\rm (\ref{cnd:newdivsimshort})}.
  \end{lemma}
  \noindent
  {\bf Proof.}
    The implication from left to right is trivial.
    For the implication from right to left, suppose that $\brelsym$
    satisfies (\ref{cnd:newdivsimshort}) and that
    $\states\brel\statet$, and consider an infinite sequence of states
    $(\states[k])_{k\in\N}$ such that
      $\states=\states[0]$
    and
      $\states[k]\step{\sact}\states[k+1]$ for all $k\in\N$. We construct
    an infinite sequence of states
      $(\statet[l])_{l\in\N}$
    and a mapping
      $\statemap\!:\N\!\rightarrow\!\N$
    such that
      $\statet=\statet[0]$,
      $\statet[l]\step{\sact}\statet[l+1]$
    and
      $\states[\statemap(l)]\brel\statet[l]$ for all $l\!\in\!\N$.

    The infinite sequence $(\statet[l])_{l\in\N}$ and the mapping
    $\statemap:\N\rightarrow\N$ can be defined simultaneously by
    induction on $l$:
    \begin{enumerate}
      \item We define $\statet[0]=\statet$ and $\statemap(0)=0$;
        it then clearly holds that
          $\states[\statemap(0)]\brel\statet[0]$.
      \item Suppose that $\states[\statemap(l)]\brel\statet[l]$.
        Then, since $(\states[\statemap(l)+k])_{k\in\N}$ is an
        infinite sequence such that
          $\states[\statemap(l)+k]\step{\sact}\states[\statemap(l)+k+1]$
        for all $k\in\N$, by (\ref{cnd:newdivsim}) there exists
        $\state{t'}$ such that $\statet[l]\step{\sact}\state{t'}$ and
        $\states[\statemap(l)+k']\brel\state{t'}$ for some
        $k'\in\N$; we define $\statet[l+1]=\state{t'}$ and
        $\statemap(l+1)=k'$.
  \qed
    \end{enumerate}

  \begin{theorem}
     $\bbisimdsym\subseteq\wbbisimdsym$.
  \end{theorem}
  \begin{proof}
    Suppose that $\states\bbisimd\statet$.
    Then there exists a binary relation $\brelsym$ satisfying
    (\ref{cnd:stepsim}) and (\ref{cnd:divsim}),
    such that $\states\brel\statet$.
    By Lemma~\ref{lem:bbdscsym} the stuttering closure $\bbdsc$ of
    $\brelsym$ is symmetric, by Lemma~\ref{lem:bbdscstepsim} it
    satisfies (\ref{cnd:stepsim}), and by
    Lemmas~\ref{lem:bbdscnewdivsim} and~\ref{lem:short} it
    satisfies (\ref{cnd:newdivsim}).
    Moreover, $\states\bbdsc\statet$.
    Hence, $\states\wbbisimd\statet$.
  \end{proof}

  \begin{corollary} \label{cor:bbisimdeqwbbisimd}
    $\rbbisimdsym=\bbisimdsym=\wbbisimdsym$.
  \end{corollary}

  \begin{corollary} \label{cor:bbisimdeq}
    The relation $\rbbisimdsym$ is an equivalence relation.
  \end{corollary}

  \noindent
  Recall that the proof strategy employed in
  Lemma~\ref{lem:relunion}(\ref{lem:relunion:item:newdivsim})
  to show that any union of binary relations satisfying
  (\ref{cnd:newdivsim}) also satisfies (\ref{cnd:newdivsim}),
  fails with (\ref{cnd:rvgdivsim}) or (\ref{cnd:divsim}) instead of
  (\ref{cnd:newdivsim}).
  In fact, it is easy to show that these results do not even hold.
  Therefore, we could not directly infer from the definition of
  $\rbbisimdsym$ that it is itself a branching bisimulation with
  explicit divergence. But now it follows, for
    $\rbbisimdsym=\wbbisimdsym$ satisfies (\ref{cnd:stepsim}) and
  (\ref{cnd:newdivsim}) by Lemma~\ref{lem:wbbisimdlargest}, and
  hence also the weaker condition (\ref{cnd:divsim}). It  satisfies
  (\ref{cnd:rvgdivsim}) by Lemma~\ref{lem:wbbisimdrvgdivsim}.

  \begin{corollary} \label{cor:bbisimdbrel}
    $\rbbisimdsym$ is the largest symmetric relation satisfying
    {\rm (\ref{cnd:stepsim})} and {\rm (\ref{cnd:divsim})}. It even
    satisfies {\rm (\ref{cnd:rvgdivsim})}, {\rm (\ref{cnd:newdivsim})}
    and {\rm (\ref{cnd:newdivsimshort})}. It therefore is the largest
    branching bisimulation with explicit divergence.
  \end{corollary}

  \noindent
  The following corollary is another consequence, which we need in the
  next section.

  \begin{corollary} \label{cor:bbisimdstuttering}
    The relation $\rbbisimdsym$ has the \emph{stuttering property}.
  \end{corollary}
  \begin{proof}
    Since $\rbbisimdsym$ satisfies (\ref{cnd:stepsim})
    and (\ref{cnd:divsim}), its stuttering
    closure $\widehat\bisim_b^{\Delta}$ satisfies (\ref{cnd:stepsim})
    by Lemma~\ref{lem:bbdscstepsim} and  (\ref{cnd:newdivsim})
    by Lemmas~\ref{lem:bbdscnewdivsim} and~\ref{lem:short}.
    Moreover, $\widehat\bisim_b^{\Delta}$ is symmetric by
    Lemma~\ref{lem:bbdscstepsim}. Therefore
    $\widehat\bisim_b^{\Delta}$ is included in $\wbbisimdsym$ (cf.\
    the proof of Lemma~\ref{lem:wbbisimdlargest}). As
    $\rbbisimdsym\subseteq\widehat\bisim_b^{\Delta}\subseteq\wbbisimdsym$
    we find $\rbbisimdsym=\widehat\bisim_b^{\Delta}$.
    Thus, by Lemma~\ref{lem:stuttering}, $\rbbisimdsym$ has the
    stuttering property.
  \end{proof}

  \begin{remark}
    Since $\rbbisimdsym=\bbisimdsym$, we can replace the second
    condition of Definition~\ref{def:bbisimd} by any
    \emph{interpolant} of (\ref{cnd:rvgdivsim}) and
    (\ref{cnd:divsim}), i.e., any condition that is implied by
    (\ref{cnd:rvgdivsim}) and implies (\ref{cnd:divsim}), and end up
    with the same equivalence.
    For instance, we could replace it by the condition of
    Gerth, Kuiper, Peled \& Penczek~\cite{GKPP99}:
    \begin{quotation}\noindent
      if $\states\brel\statet$
      and there is an infinite sequence of states
        $(\state{s_k})_{k\in\N}$
      such that
         $\states=\state{s_0}$,
         $\state{s_k}\step{\sact}\state{s_{k+1}}$
      and
         $\state{s_k}\brel\statet$ for all $k\in\N$,
      then there exists a state $\state{t'}$ such that
        $\statet\step{\sact}\state{t'}$ and
        $\state{s_k}\brel\state{t'}$ for some $k>0$.
    \end{quotation}
  \end{remark}

\section[Defining BB in terms of coloured traces]
        {Defining $\bbd$ in terms of coloured traces}

A \emph{path} from a state $\states$ is an alternating sequence
$\states[0],a_1,\states[1],a_2,s_2,\dots,a_n,s_n$ of states and
actions, such that $\states=\states[0]$ and
$\states[k-1]\step{a_k}\states[k]$ for $k=1,\dots,n$.

\begin{definition}\label{colourings}
A \emph{colouring} is an equivalence relation of $S$.
Given a colouring $\C$ and a state $s\in S$, the \emph{colour} $\C(s)$
of $s$ is the equivalence class containing $s$.

For $\pi = s_0,a_1,s_1,\dots,a_n,s_n$ a path from $s$, let $\C(\pi)$
be the alternating sequence of colours and actions obtained from
$\C(s_0),a_1,\C(s_1),\ldots,a_n,\C(s_n)$ by contracting all
subsequences $C,\tau,C,\tau,\dots,\tau,C$ to $C$. The sequence
$\C(\pi)$ is called a \emph{$\C$-coloured trace} of $s$.
A colouring $\C$ is \emph{consistent} if two states of the
same colour always have the same $\C$-coloured traces.

A state $s$ is \emph{$\C$-divergent} if there exist an infinite
sequence of states
      $(\states[k])_{k\in\N}$
    such that
      $\states=\states[0]$,
      $\states[k]\step{\sact}\states[k+1]$
    and
      $\C(\states[k])=\C(s)$ for all $k\in\N$.
A consistent colouring is said to \emph{preserve divergence} if no
$\C$-divergent state has the same colour as a nondivergent state.

We write $s\cc t$ if there exists a consistent colouring $\C$ with
$\C(s)=\C(t)$, and $s\ccd t$ if there exists a consistent, divergence
preserving colouring $\C$ with $\C(s)=\C(t)$.
\end{definition}

\noindent
In \cite{GW96} it is shown that $\ccsym = \bbisimsym$.
Here we show that $\ccdsym = \rbbisimdsym$.

\begin{lemma}\label{BB2}
Let $\C$ be a colouring such that two states with the same colour have
the same $\C$-coloured traces of length three (i.e.\ colour - action - colour).
Then $\C$ is consistent.\qed
\end{lemma}

\begin{proof}
Suppose $\C(s_0)=\C(t_0)$ and $C_0, a_1, C_1, \dots, a_n, C_n$ is a
coloured trace of $s_0$. Then, for $i=1,\dots,n$, there are states $s_i$
and paths $\pi_i$ from $s_{i-1}$ to $s_{i}$, such that
$\C(\pi_i)=C_{i-1},a_i,C_{i}$. With induction on $i$, for $i=1,\dots,n$
we find states $t_i$ with $C(s_i)=C(t_i)$ and paths $\rho_i$
from $t_{i-1}$ to $t_{i}$ such that $\C(\rho_i)=C_{i-1},a_i,C_{i}$.
Namely, the assumption about $\C$ allows us to find $\rho_i$ given
$t_{i-1}$, and then $t_i$ is defined as the last state of $\rho_i$.
Concatenating all the paths $\rho_i$ yields a path $\rho$
from $t_0$ with $\C(\rho)=C_0, a_1, C_1,\dots, a_n, C_n$.
\end{proof}

\begin{theorem}
$\ccdsym = \rbbisimdsym$.
\end{theorem}

\begin{proof}
``$\subseteq$'':
Let $\C$ be a consistent colouring that preserves divergence.
It suffices to show that $\C$ is a branching bisimulation with explicit
divergence.

Suppose $s ~\C~ t$, i.e.\ $\C(s)=\C(t)$, and $s \step{a}s'$ for some
state $s'$. In case $a=\tau$ and $\C(s')=\C(s)$ we have $s' ~\C~ t$
and condition (\ref{cnd:stepsim}) is satisfied. So suppose $a\neq\tau$
or $\C(s')\neq\C(s)$. Then $s$, and therefore also $t$, has a coloured
trace $\C(s),a,\C(s')$. This implies that there are states
$t_0,\dots,t_n$ for some $n\geq 0$ and $t'$ with $t=t_0\step\tau t_1
\step\tau \cdots \step\tau t_n \step{\opt{a}} t'$ such that
$\C(t_i)=\C(s)$ for $i=0,...,n$ and $\C(t')=\C(s')$. Hence
(\ref{cnd:stepsim}) is satisfied.

Now suppose $s ~\C~ t$ and there is an infinite sequence of states
      $(\states[k])_{k\in\N}$
    such that
      $\states=\states[0]$,
      $\states[k]\step{\sact}\states[k+1]$
    and
      $\states[k]~\C~\statet$ for all $k\in\N$.
Then $\C(\states[k])=\C(s)$ for all $k\in\N$.
Hence $s$, and therefore also $t$, is $\C$-divergent.
Thus there exists an infinite sequence of states
      $(\statet[l])_{l\in\N}$
    such that
      $\statet=\statet[0]$,
      $\statet[l]\step{\sact}\statet[l+1]$
    and
      $\C(\statet[l])=\C(t)$ for all $l\in\N$.
It follows that
      $\states[k]~\C~\statet[l]$ for all $k,l\in\N$.
Hence also (\ref{cnd:rvgdivsim}) is satisfied.

``$\supseteq$'': It suffices to show that $\rbbisimdsym$ is a
consistent, divergence preserving colouring.  By
Corollary~\ref{cor:bbisimdeq} it is an equivalence relation.  We also
use that it satisfies (\ref{cnd:stepsim}) and (\ref{cnd:rvgdivsim})
(Corollary~\ref{cor:bbisimdbrel}) and
has the stuttering property (Corollary~\ref{cor:bbisimdstuttering}).
We invoke Lemma~\ref{BB2} for proving consistency.

Suppose that $\states$ and $\statet$ have the same colour, i.e.,
$s\rbbisimd t$, and let $C,\acta,D$ be a $\rbbisimdsym$-coloured trace
of $s$. Then $\acta\neq\sact$ or $C\neq D$, and there are states
$\state{s''}$ and $\state{s'}$ with
$\states\ssteps\state{s''}\step{\acta}\state{s'}$, such that
$\state{s''},\state{s}\in C$ and $\state{s'}\in D$. As $\rbbisimdsym$
satisfies (\ref{cnd:stepsim}), by Lemma~\ref{lem:isync} there is a
state $\state{t^\dagger}$ with $\statet\ssteps\state{t^\dagger}$ and
$\state{s''}\rbbisimd \state{t^\dagger}$. 
Therefore there exist states $\state{t''}$ and $\state{t'}$ such that
  $(\statet \ssteps)\,
      \state{t^\dagger}\ssteps\state{t''}\step{\opt{\acta}}\state{t'}$,
  $\state{s''}\rbbisimd\state{t''}$ and
  $\state{s'}\rbbisimd{}\state{t'}$.
As $\rbbisimdsym$ has the stuttering property and
$\state{t''}\rbbisimd\state{s''}\rbbisimd\states\rbbisimd\statet$, 
all states on the $\sact$-path from $t$ to $t''$ have the same colour
as $\states$. Hence  $C,\acta,D$ is a $\rbbisimdsym$-coloured trace of
$\statet$.

Now suppose $\states$ and $\statet$ have the same colour and $\states$
is $\rbbisimd$-divergent. Then there is an infinite sequence of states
      $(\states[k])_{k\in\N}$
such that
      $\states=\states[0]$,
      $\states[k]\step{\sact}\states[k+1]$
    and
      $\states[k]\rbbisimd\states\rbbisimd\statet$ for all $k\in\N$.
As $\rbbisimd$ satisfies (\ref{cnd:rvgdivsim}), this implies
that there exists an infinite sequence of states
      $(\statet[l])_{l\in\N}$
    such that
      $\statet=\statet[0]$,
      $\statet[l]\step{\sact}\statet[l+1]$
    and
      $\states[k]\rbbisimd\statet[l]$ for all $k,l\in\N$.
It follows that
      $\statet[l]\rbbisimd \statet$ for all $l\in\N$,
and hence $\statet$ is $\rbbisimd$-divergent.
\end{proof}

  \section[Modal characterisations of BB]
          {Modal characterisations of $\bbd$}
          
  The class of formulas $\Frm$ of \emph{Hennessy-Milner logic with
  until, explicit divergence and infinite conjunctions} is
  generated by the following grammar:\vspace{-1ex}
  \begin{multline*}
    \frm\ ::=\
      \compl\frm\ \mid\
      \textstyle{\Meet\Frm[\Psi]}\ \mid\
      \frm\until[\acta]\frm\ \mid\
      \Div\frm ~~~~~~~~
        \text{($\acta\in\Acts$,
               $\varphi\in\Frm$ and
               $\Frm[\Psi]\subseteq\Frm$).}
  \end{multline*}
In case the cardinality $|S|$ of the set of states of our labelled
transition system is less than some infinite cardinal $\kappa$, we may
require that $|\Frm[\Psi]|<\kappa$ in conjunctions, thus obtaining a
\emph{set} of formulas rather than a proper class.

  We define when a formula $\frm$ is \emph{valid} in a state $\states$
  (notation: $\states\sat\frm$) inductively as follows:
  \begin{enumerate}
  \renewcommand{\theenumi}{\roman{enumi}}
  \renewcommand{\labelenumi}{(\theenumi)}
  \item $\states\sat\compl\frm$ \IFF{} $\states\not\sat\frm$;
  \item $\states\sat\Meet\Frm[\Psi]$
          \IFF{} $\states\sat\frm$ for all $\frm\in\Frm[\Psi]$;
  \item $\states\sat\frm\until[\acta]\frm[\psi]$
          \IFF{}
        there exist a sequence of states
        $\states[0],\dots,\states[n],\states[n+1]$ ($n\geq 0$)
        such that
          $\states=\states[0]
             \step{\sact}\cdots\step{\sact}\states[n]
             \step{\opt{\acta}}\states[n+1]$,
          $\states[i]\sat\frm$ for all $i=0,\dots,n$
        and $\states[n+1]\sat\frm[\psi]$;
  \item $\states\sat\Div\frm$
          \IFF{}
        there exists an infinite sequence $(\states[k])_{k\in\N}$ of
        states such that
          $\states=\states[0]$,
          $\states[k]\step{\sact}\states[k+1]$
        and
          $\states[k]\sat\frm$
            for all $k\in\N$.
  \end{enumerate}
The until modality above stems from {De Nicola \& Vaandrager} \cite{DV95}.
However, instead of our modality $\until[\tau]$ they use
$\until[\epsilon]$, whose validity is defined by
  \begin{enumerate}
  \item[(iii)] $\states\sat\frm\until[\epsilon]\frm[\psi]$
          \IFF{}
        either $\states\sat\frm[\psi]$, or
        there is a sequence of states
        $\states[0],\dots,\states[n],\states[n+1]$ ($n\geq 0$)
        such that
          $\states=\states[0]
             \step{\sact}\cdots\step{\sact}\states[n]
             \step{\sact}\states[n+1]$,
          $\states[i]\sat\frm$ for all $i=0,\dots,n$
        and $\states[n+1]\sat\frm[\psi]$.
  \end{enumerate}
Using this modality yields an equally expressive language as ours,
since\vspace{-1.5ex}
$$\begin{array}{l@{~~\Leftrightarrow~~}l}
\states\sat\varphi \until[\epsilon] \psi &
\states\sat\psi \vee \varphi \until[\tau] \psi
~~~~~~\mbox{and}\\[-1ex]
\states\sat\varphi \until[\tau] \psi &
\states\sat\varphi \wedge \varphi \until[\epsilon] \psi\;.\vspace{-1ex}
\end{array}$$
  Validity induces an equivalence on states; we define
  $\equivalidsym\subseteq\States\times\States$ by\vspace{-1ex}
  \begin{equation*}
    \states\equivalid\statet\quad
  \text{iff}\quad
    \all{\frm\in\Frm}.\
      {\states\sat\frm}\Longleftrightarrow{\statet\sat\frm}
  \enskip.
  \end{equation*}

  \begin{lemma} \label{lem:bbisimdstepssim}
    If $\states\rbbisimd\statet$ and
      $\states=\states[0]
                 \step{\sact}\cdots\step{\sact}
               \states[n]
                 \step{\opt{\acta}}
               \states[n+1]$,
    then there exist
      $\statet[0],\dots,\statet[m],\statet[m+1]$
    such that
      \plat{$\statet=\statet[0]
                 \step{\sact}\cdots\step{\sact}
               \statet[m]\!
                 \step{\opt{\acta}}
               \statet[m+1]$,
      $\states[n+1]\rbbisimd\statet[m+1]$}
    and
      for all $0\leq i\leq m$
        there exists $0\leq j \leq  n$
    such that $\states[j]\rbbisimd\statet[i]$.
  \end{lemma}
  \begin{proof}
    First note that by (\ref{cnd:stepsim}),
    Corollary~\ref{cor:bbisimdstuttering} and a straightforward
    induction on $n$ there exist 
      $\statet[0],\dots,\statet[m]$
    such that
      $\statet=\statet[0]\step{\sact}\cdots\step{\sact}\statet[m]$
    and for all $0\leq i \leq m$ there exists $0\leq j \leq n$ such
    that
      $\states[j]\rbbisimd\statet[i]$.

    Now, if $\acta=\sact$ and $\states[n]=\states[n+1]$, then the
    sequence $\statet[0],\dots,\statet[m],\statet[m+1]$ with
    $\statet[m+1]=\statet[m]$ satisfies the lemma.
    Otherwise, it follows from $\states[n]\rbbisimd\statet[m]$ by
    (\ref{cnd:stepsim}) and Corollary~\ref{cor:bbisimdstuttering} that
    there exist
      $\state{t_0'},\dots,\state{t_k'},\state{t_{k+1}'}$ ($k\geq 0$)
    such that
      $\statet[m]=\state{t_0'}
         \step{\sact}\cdots\step{\sact}\state{t_k'}
           \step{\opt{\acta}}\state{t_{k+1}'}$,
    $\states[n]\rbbisimd\state{t_i'}$ for all $0\leq i \leq k$ and
    $\states[n+1]\rbbisimd\state{t_{k+1}'}$; then
    the sequence
      $\statet[0],\dots,\statet[m],
       \state{t_{1}'},\dots,\state{t_{k}'},\state{t_{k+1}'}$
    satisfies the lemma.
  \end{proof}

  \begin{theorem} \label{theo:modchar}
    For all states $\states$ and $\statet$:
      $\states\rbbisimd\statet$
    \IFF{}
      $\states\equivalid\statet$.
  \end{theorem}
  \begin{proof}
    To establish the implication from left to right,
    we prove by structural induction on $\frm$ that if
    $\states\rbbisimd\statet$ and $\states\sat\frm$, then
    $\statet\sat\frm$. We only treat the cases
      $\frm=\frm[\psi]\until[\acta]\frm[\chi]$
    and
      $\frm=\Div\frm[\psi]$;
    the other two cases are trivial.
    \begin{enumerate}
    \item Suppose $\frm=\frm[\psi]\until[\acta]\frm[\chi]$ and
      $\states\sat\frm$.
      Then there exist a sequence of states
        $\states[0],\dots,\states[n],\states[n+1]$ ($n\geq 0$)
      such that
        \plat{$\states=\states[0]
           \step{\sact}\cdots\step{\sact}
              \states[n]\step{\opt{\acta}}\states[n+1]$},
        $\states[i]\sat\frm[\psi]$ for all $i=0,\dots,n$
        and $\states[n+1]\sat\frm[\chi]$.
      By Lemma~\ref{lem:bbisimdstepssim}, there exists a sequence of
      states $\statet[0],\dots,\statet[m],\statet[m+1]$ such that
        \plat{$\statet=\statet[0]
                   \step{\sact}\cdots\step{\sact}
                 \statet[m]
                   \step{\opt{\acta}}
                 \statet[m+1]$},
      $\states[n+1]\rbbisimd\statet[n+1]$
      and for all $i$ ($0\leq i\leq m$)
        there exists $j$ ($0\leq j \leq  n$)
      such that $\states[j]\rbbisimd\statet[i]$.
      From the latter, by the induction hypothesis, it follows that
      $\statet[i]\sat\frm[\psi]$ for all $0\leq i \leq m$.
      From $\states[n+1]\rbbisimd\statet[m+1]$, by the induction
      hypothesis, it follows that $\statet[m+1]\sat\frm[\chi]$.
      Hence, $\statet\sat\frm$.
    \item Suppose $\frm=\Div\frm[\psi]$ and suppose
      $\states\sat\frm$. Then there exists an infinite sequence
      $(\states[k])_{k\in\N}$ such that $\states=\states[0]$,
      $\states[k]\step{\sact}\states[k+1]$ and
      $\states[k]\sat\frm[\psi]$ for all $k\in\N$.
      From Corollary~\ref{cor:bbisimdbrel} it follows that
      $\rbbisimdsym$ satisfies (\ref{cnd:newdivsim}), so
      there exist an infinite sequence of
      states $(\statet[l])_{l\in\N}$ and a mapping
        $\statemap:\N\rightarrow\N$
      such that
        $\statet=\statet[0]$,
        $\statet[l]\step{\sact}\statet[l+1]$
      and
        $\states[\statemap(l)]\rbbisimd\statet[l]$ for all $l\in\N$.
      By the induction hypothesis $\statet[l]\sat\frm[\psi]$ for all
      $l\in\N$, and hence $\statet\sat\frm$.
    \end{enumerate}
    For the implication from right to left, we prove that $\equivalid$
    is a branching bisimulation with explicit divergence.

    Clearly, $\equivalid$ is symmetric.

    To establish condition~(\ref{cnd:stepsim}) of
    Definition~\ref{def:bbisimd}, suppose that
    $\states\equivalid\statet$ and $\states\step{\acta}\state{s'}$,
    and define sets $T''$ and $T'$ as follows:
    \begin{gather*}
      \States[T'']=\{\state{t''}\in\States
            \mid\statet\ssteps{}\state{t''}\ \&\
            \states\not\equivalid\state{t''}
          \};\ \text{and}\\
      \States[T']=\{\state{t'}\in\States
            \mid\exists{\state{t''}\in\States}.\
                  \statet\ssteps{}\state{t''}\step{\opt{\acta}}\state{t'}\
                \&\
                  \state{s'}\not\equivalid\state{t'}
         \}
    \enskip.
    \end{gather*}
    For each $\state{t''}\in\States[T'']$ let
    $\frm[{\varphi_{\state{t''}}}]$
    be a formula such that
      $\states\sat\frm[{\varphi_{\state{t''}}}]$ and
      $\state{t''}\not\sat\frm[{\varphi_{\state{t''}}}]$,
    and let
      $\frm[\varphi]
         =\Meet\{\frm[\varphi_{\state{t''}}]\mid\state{t''}\in
         \States[T'']\}$.
    Similarly, for each $\state{t'}\in\States[T']$ let
    $\frm[{\psi_{\state{t'}}}]$ be a formula such that
    $\state{s'}\sat\frm[{\psi_{\state{t'}}}]$ and
    $\state{t'}\not\sat\frm[{\psi_{\state{t'}}}]$,
    and let
      $\frm[\psi]
         =\Meet\{\frm[\psi_{\state{t'}}]
                   \mid \state{t'}\in\States[T']\}$.
    Note that $\states\sat\frm[\varphi]\until[\acta]\frm[\psi]$, and
    hence, since $\states\equivalid\statet$, also
      $\statet\sat\frm[\varphi]\until[\acta]\frm[\psi]$.
    So, there exists a sequence of states
    $\statet[0],\dots,\statet[n],\statet[n+1]$ such that
      $\statet=\statet[0]
                 \step{\sact}\cdots\step{\sact}
               \statet[n]
                 \step{\opt{\acta}}
               \statet[n+1]$,
      $\statet[i]\sat\frm[\varphi]$ for all $i=0,\dots,n$
    and
      $\statet[n+1]\sat\frm[\psi]$.
    From $\statet[n]\sat\frm[\varphi]$ it follows that
      $\statet[n]\not\in\States[T'']$,
    so $\states\equivalid\statet[n]$;
    from $\statet[n+1]\sat\frm[\psi]$ it follows that
      $\statet[n+1]\not\in\States[T']$,
    so $\state{s'}\equivalid\statet[n+1]$.
    Thereby, condition~(\ref{cnd:stepsim}) of
    Definition~\ref{def:bbisimd} is established.

    To establish condition~(\ref{cnd:rvgdivsim}) of
    Definition~\ref{def:bbisimd}, suppose that
    $\states\equivalid\statet$ and that there exists an
    infinite sequence $(\states[k])_{k\in\N}$
    such that $\states=\states[0]$,
    $\states[k]\step{\sact}\states[k+1]$ and
    $\states[k]\equivalid\statet$ for all $k\in\N$.
    Define the set $\States[T^\infty]$ by
    \begin{equation*}
      \States[T^\infty]
        = \{\state{t'}\in\States\mid
              \statet\ssteps{}\state{t'}\ \&\
              \states\not\equivalid\state{t'}\}
    \enskip.
    \end{equation*}
    For each $t'\in\States[T^\infty]$ let $\frm[\varphi_{\state{t'}}]$
    be a formula such that $\states\sat\frm[\varphi_{\state{t'}}]$ and
      $\state{t'}\not\sat\frm[\varphi_{t'}]$,
    and let
      $\frm=
         \Meet\{\frm[\varphi_{\state{t'}}]
                  \mid\state{t'}\in\States[T^\infty]\}$.
    Since $\states[0]=\states\sat\frm$ and
    $\states[k]\equivalid\statet\equivalid\states$,
    it follows that $\states[k]\sat\frm$ for
    all $k\in\N$, and therefore $\states\sat\Div\frm$.
    Hence, $\statet\sat\Div\frm$, so there exists an infinite
    sequence $(\statet[\ell])_{\ell\in\N}$ such that $\statet=\statet[0]$,
    $\statet[\ell]\step{\sact}\statet[\ell+1]$ and
    $\statet[\ell]\sat\frm$ for all $\ell\in\N$.
    From the latter it follows that
    $\statet[\ell]\not\in\States[T^\infty]$,
    so $\states\equivalid\statet[\ell]$, for all $\ell\in\N$, and
    hence $\states[k]\equivalid\states\equivalid\statet[\ell]$ for all
    $k,\ell\in\N$.
  \end{proof}

  The modal logic for $\bbd$ proposed in \cite{Gla93} has,
  instead of our until modalities, for every $\acta\in\Acts$ a binary
  modality $\runtil[\acta]$, and, instead of our divergence modality,
  a unary modality $\rDiv$; the validity of these modalities is
  defined by
  \begin{enumerate}
  \addtocounter{enumi}{2}
  \item $\states\sat\frm\runtil[\acta]\frm[\psi]$
          \IFF{}
        there exist states $\state{s'}$ and $\state{s''}$ such that
          $\states\ssteps\state{s''}\step{\opt{\acta}}\state{s'}$,
          $\state{s''}\sat\frm$ and $\states'\sat\frm[\psi]$;
  \item $\states\sat\rDiv\frm$
          \IFF{}
        there exists an infinite sequence $(\states[k])_{k\in\omega}$
        of states such that $\states\ssteps\states[0]$,
          $\states[k]\step{\sact}\states[k+1]$ and
        $\states[k]\sat\frm$ for all $k\in\omega$.
  \end{enumerate}
  We denote by $\requivalidsym$ the equivalence induced on states by
  validity in the modal logic of \cite{Gla93}.
  Below we shall establish that $\requivalidsym$ coincides with
  $\rbbisimd$, using the following modal stuttering property.
  \begin{lemma} \label{lem:modalstuttering}
    Let $\frm$ be a formula of the modal logic of \cite{Gla93}.
    If  $\states\sat\frm$ and $\stateu\sat\frm$, then
    $\statet\sat\frm$ for all states $\statet$ such that
    $\states\ssteps\statet\ssteps\stateu$.
  \end{lemma}
  \begin{proof}
    Suppose that $\states$, $\statet$ and $\stateu$ are states such
    that $\states\sat\frm$, $\stateu\sat\frm$ and
    $\states\ssteps\statet\ssteps\stateu$; we prove that
    $\statet\sat\frm$ with induction on $\frm$.

    First, we consider two special cases:
    \begin{enumerate}
    \item A \emph{downward formula} is a formula of the form
        $\frm[\psi]\runtil[\acta]\frm[\chi]$ 
      or
        $\rDiv\frm[\psi]$.
      If $\frm$ is a downward formula, then it is clear from the
      definition of validity that if $\stateu\sat\frm$, then also
      $\statet\sat\frm$.
    \item An \emph{upward formula} is the negation of a downward
      formula.
      Suppose that $\frm$ is an upward formula, say
      $\frm=\compl\frm[\psi]$ with $\frm[\psi]$ a downward formula,
      and $\states\sat\frm$; then $\states\not\sat\frm[\psi]$, so by
      the previous case and contraposition it follows that
      $\statet\not\sat\frm[\psi]$, and therefore
      $\statet\sat\frm$.
    \end{enumerate}
    Since by De Morgan's laws we can assume that $\frm$ is
    composed from downward and upward formulas by means of (infinite)
    conjunctions and disjunctions, it remains to consider the cases
    where $\frm$ is a conjunction or a disjunction.

    Suppose that $\frm=\Meet\Frm[\Psi]$.
    From $\states\sat\frm[\Psi]$ and $\stateu\sat\frm[\Psi]$ it
    follows that $\states\sat\frm[\psi]$ and $\stateu\sat\frm[\psi]$
    for all $\frm[\psi]\in\Frm[\Psi]$, so by the induction hypothesis,
    $\statet\sat\frm[\psi]$ for all $\frm[\psi]\in\Frm[\Psi]$.
    Hence, $\statet\sat\frm$.
    The proof for the case where $\frm$ is a disjunction is similar.
  \end{proof}

  \begin{corollary}
    For all states $\states$ and $\statet$: $\states\rbbisimd\statet$
    \IFF{} $\states\requivalid\statet$.
  \end{corollary}
  \begin{proof}
    ``Only if'':
    Note that the modalities from the modal logic of \cite{Gla93} can
    be expressed in our modal logic:\vspace{-1.5ex}
    $$\begin{array}{l@{~~\Leftrightarrow~~}l}
        \states\sat{\frm\runtil[\acta]\frm[\psi]} &
        \states\sat{\true\until[\sact](\varphi\until[\acta]\psi)}
      ~~~~~~\mbox{and}\\[-1ex]
        \states\sat{\rDiv\frm} &
        \states\sat{\true\until[\sact](\Div\frm)}\;.\vspace{-1ex}
    \end{array}$$
    So, $\equivalidsym\subseteq\requivalidsym$ and hence, by
    Theorem~\ref{theo:modchar}, it follows that, for all states
    $\states$ and $\statet$, if $\states\rbbisimd\statet$, then
    $\states\requivalid\statet$.

    ``If'': The proof is similar to the proof for the implication from
    right to left of Theorem~\ref{theo:modchar}.
    Again, it is clear that $\requivalidsym$ is symmetric, and
    condition~(\ref{cnd:stepsim}) can be established as in the proof
    of Theorem~\ref{theo:modchar}, with
    $\frm\runtil[\acta]\frm[\psi]$ instead of
    $\frm\until[\acta]\frm[\psi]$.

    To establish condition~(\ref{cnd:rvgdivsim}) of
    Definition~\ref{def:bbisimd}, suppose that
    $\states\requivalid\statet$ and that there exists an
    infinite sequence $(\states[k])_{k\in\N}$
    such that $\states=\states[0]$,
    $\states[k]\step{\sact}\states[k+1]$ and
    $\states[k]\requivalid\statet$ for all $k\in\N$.
    Let $\States[T^{\infty}]$ and $\frm$ be defined
    as in the proof of Theorem~\ref{theo:modchar}.
    Since $\states[0]=\states\sat\frm$ and
      $\states[k]\requivalid\statet\requivalid\states$,
    it follows that $\states[k]\sat\frm$ for
    all $k\in\N$, and therefore $\states\sat\rDiv\frm$.
    Hence, $\statet\sat\rDiv\frm$, so there exists an infinite
    sequence $(\statet[\ell])_{\ell\in\N}$ and $m\in\N$ such that
    $\statet=\statet[0]$,
    $\statet[\ell]\step{\sact}\statet[\ell+1]$ and
    $\statet[\ell]\sat\frm$ for all $\ell\geq m$.
    From $s\requivalid\statet$ we furthermore obtain $t=t_0\sat\frm$.
    Since $\statet[0]\sat\frm$ and $\statet[m]\sat\frm$, it
    follows by Lemma~\ref{lem:modalstuttering} that
    $\statet[\ell]\sat\frm$ also for all $0 <\ell < m$.
    It follows that $\statet[\ell]\not\in\States[T^\infty]$,
    so $\states\requivalid\statet[\ell]$, for all $\ell\in\N$, and
    hence $\states[k]\requivalid\states\requivalid\statet[\ell]$ for all
    $k,\ell\in\N$.
  \end{proof}
 
% \bibliographystyle{plain}
% \def\sortunder#1{}
% \bibliography{paper}

\begin{thebibliography}{1}

\bibitem{Bas96}
{\sc Twan Basten} (1996):
\newblock {\em Branching bisimulation is an equivalence indeed!}
\newblock {\sl Information Processing Letters} 58(3), pp. 141--147.

\bibitem{DV95}
{\sc Rocco {De Nicola} \& Frits~W. Vaandrager} (1995):
\newblock {\em Three logics for branching bisimulation.}
\newblock {\sl J. ACM} 42(2), pp. 458--487.

\bibitem{GKPP99}
{\sc Rob Gerth, Ruurd Kuiper, Doron Peled \& Wojciech Penczek} (1999):
\newblock {\em A partial order approach to branching time logic model checking.}
\newblock {\sl Information and Computation} 150(2), pp. 132--152.

\bibitem{Gla93}
{\sc Rob~van Glabbeek} (1993):
\newblock {\em The linear time - branching time spectrum {II}.}
\newblock In E.~Best, editor: {\sl Proceedings of CONCUR'93}, {\sl {\rm LNCS}} 715, Springer, pp. 66--81.

\bibitem{CTLd}
{\sc Rob van Glabbeek, Bas Luttik \& Nikola Tr\v{c}ka}:
\newblock {\em Computation tree logic and deadlock detection.}
\newblock In preparation.

\bibitem{GW96}
{\sc Rob van Glabbeek \& Peter Weijland} (1996):
\newblock {\em Branching time and abstraction in bisimulation semantics.}
\newblock {\sl J. ACM} 43(3), pp. 555--600.

\bibitem{Nej03}
{\sc Shiva Nejati} (2003):
\newblock {\em Refinement relations on partial specifications.}
\newblock Master's thesis, University of Toronto.

\end{thebibliography}
\end{document}
