%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%	             Sizes, first for US letter format			  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentstyle[11pt]{article}		% Fontsize 11 point
\textwidth    		6.5 in		% paper = 8.5x11in
\textheight   		8.58in          %  + foot 30pt = 9.00in
\oddsidemargin		0   pt          % 1 inch margin comes for free
\evensidemargin 	0   pt          % 1 inch margin comes for free
\topmargin      	0   pt          % 4 margins of 1in each
\headheight     	0   pt          % default 12pt = 0.42cm       
\headsep        	0   pt          % default 25pt = 0.88cm       
\unitlength		1   mm		% This is used in pictures

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%		On A4 paper the right margin is 6 mm smaller,		  %%%%
%%%%		whereas the bottom margin is 17.6 mm longer.		  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside}			 \newlength{\shifttop}
\setlength{\shiftside}{-3mm}		 \setlength{\shifttop}{8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 0 for American paper or 1 for A4.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			Theorem-like environments			  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}

\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{th-#1} }{\end{theo}}
\newenvironment{proposition}[1]{\begin{prop} \rm \label{pr-#1} }{\end{prop}}
\newenvironment{lemma}[1]{\begin{lemm} \rm \label{lem-#1} }{\end{lemm}}
\newenvironment{corollary}[1]{\begin{coro} \rm \label{cor-#1} }{\end{coro}}
\newenvironment{example}[1]{\begin{exam} \rm \label{ex-#1} }{\end{exam}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}

\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\th}[1]{Theorem~\ref{th-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Corollary~\ref{cor-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\title}[1]{ \vspace*{5pt}
			\setcounter{footnote}{0}
			\renewcommand{\thefootnote}{\fnsymbol{footnote}}
			\begin{center}
			{\LARGE \bf #1\\ \ \\}
			R.J. van Glabbeek\makebox[0pt][l]{\footnotemark}\\
			\footnotesize
			Computer Science Department, Stanford University\\
			Stanford, CA 94305, USA.\\
			{\tt rvg@cs.stanford.edu}
			\end{center}
			\footnotetext{This work was supported by ONR under
			grant number N00014-92-J-1974.}
			\renewcommand{\thefootnote}{\arabic{footnote}}
			\setcounter{footnote}{0}
			\vspace{5pt}			}
\renewcommand{\abstract}[1]{\begin{list}{}
			{\rightmargin\leftmargin
			\listparindent 1.5em
			\parsep 0pt plus 1pt}
			\small\item #1\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\cdot}{\cup}}		% disjoint union
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}}	% openface letter
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox	% openface character
	[0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\IT}{\mbox{\sf T\hspace{-5.5pt}T}}          % openface T (terms)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\Id}[1]{[\hspace{-1.4pt}[#1]\hspace{-1.2pt}]} % denotation
\newcommand{\In}[1]{\plat{			 	% notation
	\stackrel{\mbox{\tiny $/\hspace{-2.1pt}/$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $\backslash
	\hspace{-2.1pt}\backslash$}}\!\!#1\!\!
	\stackrel{\mbox{\tiny $\backslash\hspace{-1.8pt}\backslash$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $/\hspace{-1.8pt}/$}} }}
\newcommand{\rec}[1]{\plat{			 	% recursion
	\stackrel{\mbox{\tiny $/$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
	\!\!#1\!\!
	\stackrel{\mbox{\tiny $\backslash$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\lto}[1]{\stackrel{#1}{\rightarrow}}	% subtransition
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}}	% transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt}	% no transition
	\stackrel{#1\ }{\longrightarrow}}
\newcommand{\dto}[1]{\stackrel{#1}{\Longrightarrow}}	% abstract transition
\newcommand{\bis}[1]{ \;				% bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt}	% no bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,$}}
\newcommand{\pf}{{\bf Proof:\ }}			% beginning of proof
\newcommand{\rest}{					% restriction operator
        \begin{picture}(2.16,3.2)
        \thinlines
        \put(1.12,-0.48){\line(0,1){3.52}}
	\put(0.8,1.6){\tiny $\backslash$}
        \end{picture} }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%			Abbreviations				          %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}}			    % natural numbers
\newcommand{\IC}{\dc{C}}			    % configuration structures
\newcommand{\IE}{\dl{E}}			    % event structures
\newcommand{\IG}{\dc{G}}			    % graphs
\newcommand{\IP}{\dl{P}}			    % transition space
\newcommand{\IO}{\dc{O}}			    % observations
\newcommand{\pow}{{\cal P}}			    % powerset
\newcommand{\fC}{{\cal C}}			    % function into \IC
\newcommand{\fE}{{\cal E}}			    % function into \IE
\newcommand{\fG}{{\cal G}}			    % function into \IG
\newcommand{\fO}{{\cal O}}			    % function into \IO
\newcommand{\eC}{{\rm C}}			    % conf. structure
\newcommand{\eD}{{\rm D}}			    % conf. structure
\newcommand{\eE}{{\rm E}}			    % event structure
\newcommand{\eF}{{\rm F}}			    % event structure
\newcommand{\eG}{{\rm G}}			    % process graph
\newcommand{\eH}{{\rm H}}			    % process graph
\newcommand{\eP}{{\rm P}}			    % process expression
%\renewcommand{\cite}[1]{[#1]}				% manual citations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\bibliographystyle{plain}		% Actually the vG-style is used here
\title{What is branching time semantics and why to use it?}

\abstract{The concept of branching time in the semantics of concurrent
systems is well known and well understood. Still a formal definition
of what it means for a model or equivalence to respect branching time
has never explicitly be given. This note proposes such a definition.
Additionally the opportunity is taken to voice an old but poorly
understood argument for using branching time semantics instead of
models or equivalences that are fully abstract with respect to some
notion of observability.}

\section*{Introduction}

When comparing models or equivalences for concurrent systems, it is
common practice to distinguish between {\em linear time} and {\em
branching time} semantics (see for instance {\sc De Bakker, Bergstra,
Klop \& Meyer} \cite{BBKM84} or {\sc Pnueli} \cite{Pn85}). In the
former, a process is completely determined by the observable content
of its possible (partial) runs, whereas in the latter also the
information is preserved where two different courses of action diverge
(although branching of identical courses of action may still be
neglected). Standard examples are the processes in Figure \ref{1} and
\ref{2}.
\begin{figure}[htb]
\begin{minipage}{3.2in}
\begin{picture}(80,30)(0,5)
\put(20,30){\circle{1}}
\put(20,29.5){\vector(0,-1){9}}
\put(21,24){$a$}
\put(20,20){\circle{1}}
\put(19.65,19.65){\vector(-1,-1){9.3}}
\put(13,15){$b$}
\put(10,10){\circle{1}}
\put(20.35,19.65){\vector(1,-1){9.3}}
\put(26,15){$c$}
\put(30,10){\circle{1}}
\put(60,30){\circle{1}}
\put(59.65,29.65){\vector(-1,-1){9.3}}
\put(52,25){$a$}
\put(50,20){\circle{1}}
\put(50,19.5){\vector(0,-1){9}}
\put(51,14){$b$}
\put(50,10){\circle{1}}
\put(60.35,29.65){\vector(1,-1){9.3}}
\put(66,25){$a$}
\put(70,20){\circle{1}}
\put(70,19.5){\vector(0,-1){9}}
\put(67,14){$c$}
\put(70,10){\circle{1}}
\end{picture}
\caption{$~a(b+c)~$ vs. $~ab+ac$\label{1}}
\end{minipage}
\hfill
\begin{minipage}{3.2in}
\begin{picture}(80,30)
\put(20,30){\circle{1}}
\put(20,29.5){\vector(0,-1){9}}
\put(21,24){$a$}
\put(20,20){\circle{1}}
\put(19.65,19.65){\vector(-1,-1){9.3}}
\put(13,15){$b$}
\put(10,10){\circle{1}}
\put(10,9.5){\vector(0,-1){9}}
\put(11,4){$c$}
\put(10,0){\circle{1}}
\put(20.35,19.65){\vector(1,-1){9.3}}
\put(26,15){$b$}
\put(30,10){\circle{1}}
\put(30,9.5){\vector(0,-1){9}}
\put(27,4){$d$}
\put(30,0){\circle{1}}
\put(60,30){\circle{1}}
\put(59.65,29.65){\vector(-1,-1){9.3}}
\put(52,25){$a$}
\put(50,20){\circle{1}}
\put(50,19.5){\vector(0,-1){9}}
\put(51,14){$b$}
\put(50,10){\circle{1}}
\put(50,9.5){\vector(0,-1){9}}
\put(51,4){$c$}
\put(50,0){\circle{1}}
\put(60.35,29.65){\vector(1,-1){9.3}}
\put(66,25){$a$}
\put(70,20){\circle{1}}
\put(70,19.5){\vector(0,-1){9}}
\put(67,14){$b$}
\put(70,10){\circle{1}}
\put(70,9.5){\vector(0,-1){9}}
\put(67,4){$d$}
\put(70,0){\circle{1}}
\end{picture}
\caption{$~a(bc+bd)~$ vs. $~abc+abd$\label{2}}
\end{minipage}
\end{figure}
In Figure \ref{1}, both processes have two complete runs, whose observable
content is $ab$ and $ac$ respectively. However, in $a(b+c)$ these runs
diverge after the $a$-step, whereas in $ab+ac$ they diverge at the
onset. This difference can also be described by pointing out that
$a(b+c)$ has a partial run with observable content $a$ that is an
initial part of each of the runs $ab$ and $ac$, whereas $a(b+c)$ has no
such run. Hence the two processes are linear time equivalent, but
not branching time equivalent. Similarly, the two processes of Figure
\ref{2} are identified in linear time semantics but not in branching
time semantics, since only $a(bc+bd)$ has a run $a$ that is an initial
part of both of the runs $abc$ and $abd$.

\begin{figure}[htb]
\begin{minipage}{3.2in}
\begin{picture}(80,30)
\put(20,30){\circle{1}}
\put(20,29.5){\vector(0,-1){9}}
\put(21,24){$a$}
\put(20,20){\circle{1}}
\put(19.65,19.65){\vector(-1,-1){9.3}}
\put(13,15){$b$}
\put(10,10){\circle{1}}
\put(20.35,19.65){\vector(1,-1){9.3}}
\put(26,15){$b$}
\put(30,10){\circle{1}}
\put(60,30){\circle{1}}
\put(59.65,29.65){\vector(-1,-1){9.3}}
\put(52,25){$a$}
\put(50,20){\circle{1}}
\put(50,19.5){\vector(0,-1){9}}
\put(51,14){$b$}
\put(50,10){\circle{1}}
\put(60.35,29.65){\vector(1,-1){9.3}}
\put(66,25){$a$}
\put(70,20){\circle{1}}
\put(70,19.5){\vector(0,-1){9}}
\put(67,14){$b$}
\put(70,10){\circle{1}}
\end{picture}
\caption{$~a(b+b)~$ vs. $~ab+ab$\label{3}}
\end{minipage}
\hfill
\begin{minipage}{3.2in}
\begin{picture}(80,30)
\put(20,30){\circle{1}}
\put(20,29.5){\vector(0,-1){9}}
\put(21,24){$a$}
\put(20,20){\circle{1}}
\put(19.65,19.65){\vector(-1,-1){9.3}}
\put(13,15){$b$}
\put(10,10){\circle{1}}
\put(10.5,10){\vector(1,0){19}}
\put(20,11){$b$}
\put(30,10){\circle{1}}
\put(29.65,10.35){\vector(-1,1){9.3}}
\put(26,15){$b$}
\put(60,30){\circle{1}}
\put(60,29.5){\vector(0,-1){9}}
\put(61,24){$a$}
\put(60,20){\circle{1}}
\put(59.65,19.65){\vector(-1,-1){9.3}}
\put(52,15){$b$}
\put(50,10){\circle{1}}
\put(50.35,9.65){\vector(1,-1){9.3}}
\put(56,5){$b$}
\put(60,0){\circle{1}}
\put(60.35,0.35){\vector(1,1){9.3}}
\put(62,5){$b$}
\put(70,10){\circle{1}}
\put(69.65,10.35){\vector(-1,1){9.3}}
\put(66,15){$b$}
\end{picture}
\caption{$~a(bbb)^{\infty}~$ vs. $~a(bbbb)^{\infty}$\label{4}}
\end{minipage}
\end{figure}
Figure \ref{3} illustrates that in branching time semantics only the
branching of {\em different} courses of action is of importance.
The processes $a(b+b)$ and $ab+ab$ are {\em bisimulation equivalent}
\cite{Mi90ccs}, which is widely considered to be the prime example of
a branching time equivalence. Nevertheless, the two runs with observable
content $ab$ diverge at a different state. One could employ a stricter
notion of branching time, in which also the branching of identical
courses of action would be taken into account. Under such a notion, the
processes of Figure \ref{3} should be distinguished, but the ones of
Figure \ref{4} could safely be identified.

It should be pointed out that branching time is not the definition of
a particular model or semantic equivalence, but a criterion that can
be satisfied by models or equivalences. A model or equivalence that
satisfies this criterion is said to {\em be a branching time model or
equivalence}, to {\em respect branching time}, or to {\em respect the
branching structure} of processes. Call two processes, represented as
labelled transition systems, {\em tree equivalent} if their unfoldings
into trees are isomorphic.  The two processes of Figure \ref{4} for
instance are tree equivalent, whereas the ones of Figure
\ref{1}--\ref{3} are not. Tree equivalence is strictly finer than
bisimulation equivalence and thus certainly preserves the information
on where different courses of action diverge. Hence it constitutes a
second example of a branching time equivalence. Moreover, unlike
bisimulation equivalence, it would still be a branching time
equivalence under the stricter interpretation of branching time
contemplated above.

For processes without silent moves, it is commonly agreed that an
equivalence respects branching time iff it is finer than or equal to
bisimulation equivalence. Hence this yield a candidate for a
formal definition of the concept of a branching time equivalence.
However, in the presence of silent moves, or $\tau$-steps, the
situation is less clear. In {\sc Van Glabbeek \& Weijland} \cite{GW89}
it is argued that {\em branching bisimulation}, that in the absence of
silent moves coincides with plain bisimulation, takes over this r\^ole
of bisimulation in the presence of $\tau$'s. However, this is not
inherent in the definition of the equivalence, and was meant to be a
result rather than a definition. The reasoning of \cite{GW89} is
illustrated in Figures \ref{5} and \ref{6}.
\begin{figure}[htb]
\begin{minipage}{3.2in}
\begin{picture}(80,30)
\put(20,30){\circle{1}}
\put(20,29.5){\vector(0,-1){9}}
\put(21,24){$a$}
\put(20,20){\circle{1}}
\put(19.65,19.65){\vector(-1,-1){9.3}}
\put(13,15){$b$}
\put(10,10){\circle{1}}
\put(20.35,19.65){\vector(1,-1){9.3}}
\put(26,15){$d$}
\put(30,10){\circle{1}}
\put(20,19.5){\vector(0,-1){9}}
\put(21,14){$\tau$}
\put(20,10){\circle{1}}
\put(19.65,9.65){\vector(-1,-1){9.3}}
\put(13,5){$b$}
\put(10,0){\circle{1}}
\put(20.35,9.65){\vector(1,-1){9.3}}
\put(26,5){$c$}
\put(30,0){\circle{1}}

\put(60,30){\circle{1}}
\put(60,29.5){\vector(0,-1){9}}
\put(61,24){$a$}
\put(60,20){\circle{1}}
\put(60.35,19.65){\vector(1,-1){9.3}}
\put(66,15){$d$}
\put(70,10){\circle{1}}
\put(60,19.5){\vector(0,-1){9}}
\put(61,14){$\tau$}
\put(60,10){\circle{1}}
\put(59.65,9.65){\vector(-1,-1){9.3}}
\put(53,5){$b$}
\put(50,0){\circle{1}}
\put(60.35,9.65){\vector(1,-1){9.3}}
\put(66,5){$c$}
\put(70,0){\circle{1}}
\end{picture}
\caption{$~a(b+\tau(b+c)+d)~$ vs. $~a(\tau(b+c)+d)$\label{5}}
\end{minipage}
\hfill
\begin{minipage}{3.2in}
\begin{picture}(80,30)
\put(20,30){\circle{1}}
\put(20,29.5){\vector(0,-1){9}}
\put(21,24){$a$}
\put(20,20){\circle{1}}
\put(19.65,19.65){\vector(-1,-1){9.3}}
\put(13,15){$b$}
\put(10,10){\circle{1}}
\put(20,19.5){\vector(0,-1){9}}
\put(21,14){$\tau$}
\put(20,10){\circle{1}}
\put(19.65,9.65){\vector(-1,-1){9.3}}
\put(13,5){$b$}
\put(10,0){\circle{1}}
\put(20.35,9.65){\vector(1,-1){9.3}}
\put(26,5){$c$}
\put(30,0){\circle{1}}

\put(60,30){\circle{1}}
\put(60,29.5){\vector(0,-1){9}}
\put(61,24){$a$}
\put(60,20){\circle{1}}
\put(60,19.5){\vector(0,-1){9}}
\put(61,14){$\tau$}
\put(60,10){\circle{1}}
\put(59.65,9.65){\vector(-1,-1){9.3}}
\put(53,5){$b$}
\put(50,0){\circle{1}}
\put(60.35,9.65){\vector(1,-1){9.3}}
\put(66,5){$c$}
\put(70,0){\circle{1}}
\end{picture}
\caption{$~a(b+\tau(b+c))~$ vs. $~a\tau(b+c)$\label{6}}
\end{minipage}
\end{figure}
The first process in Figure \ref{5} has a run with observable content
$ab$, that diverges from the run with observable content $ac$ at the same
point where it diverges from the run $ad$. Thus it does not pass
through a state in which it is still possible to continue with a
course of action that involves a $c$, but not possible to continue
with a course of action involving a $d$. Such a run is not present in
the other process. It follows that these processes have a different
branching structure and can not be identified by a branching time
equivalence. As {\sc Milner}'s notion of {\em weak bisimulation}
\cite{Mi90ccs} identifies both processes, it does not respect
branching time. The notion of branching bisimulation on the other hand
gives rise to a finer equivalence that does distinguish the processes
of Figure \ref{5}. The processes of Figure \ref{6} are branching
bisimulation equivalent however, and indeed no argument can be
construed that would indicate disrespect of branching time, the key
argument being that the various runs with observable content $ab$ can be
regarded as the same course of action.

The best definition of a branching time equivalence so far is perhaps
the one implicit in the notion of a {\em consistent colouring},
introduced in \cite{GW89}: An equivalence {\em respects branching
time} if the colouring on processes/states, obtained by giving
equivalent processes the same colour, is {\em consistent} in the sense
of \cite{GW89}. Here a sequence $C_0, a_1, C_1, a_2, C_2, \ldots
, a_k, C_k$ is a {\em concrete coloured trace} of a process
$p_0$ if there is a run $p_0 \goto{a_1} p_1 \goto{a_2} p_2 \goto{}
\cdots \goto{a_k} p_k$, such that process $p_i$ has colour $C_i$;
a {\em coloured trace} of $p$ is a sequence $C_0, a_1, C_1, a_2, C_2,
\ldots , a_k, C_k$ obtained from a concrete coloured trace of $p$ by
replacing any subsequence $C,\tau,C,\tau,...,\tau,C$ by $C$;
and a colouring is consistent if processes with the
same colour have the same set of coloured traces. The idea behind a
consistent colouring is that processes with the same colour have the
same potential of further courses of action. A coloured trace
indicates how these potentials vary (diminish) during a run.
As expected, under this definition branching bisimulation turns out to
be the coarsest branching time equivalence.

Although this definition captures the concept of branching time
reasonably well, it has the disadvantage of being tailored to a
setting with silent moves (through the reduction
$C,\tau,C,\tau,...,\tau,C \leadsto C$). What would be more convincing
would be a definition that in no way refers to internal actions, and
still yields branching bisimulation as the coarsest equivalence
respecting the branching structure of processes. Moreover, it would be
nice to know what precisely the branching structure of a process is.
This is the goal of the present paper. I will formally define the
branching structure of a process, and declare an equivalence to
respect branching time iff it only relates processes with the same
branching structure. This will be the case iff the equivalence is
finer than or equal to branching bisimulation equivalence. Similarly a
model of concurrency respects branching time iff processes that are
represented by the same semantic object have the same branching
structure.

\section{The branching structure of a process}

Let $\IP$ be a class of processes. I assume that for each process
$p\in \IP$ a set ${\it run}(p)$ of (partial) runs is defined, equipped
with a prefix ordering $\leq$, and that with each run (or {\em
execution}) $e\in {\it run}(p)$ is associated its observable content $l(e)$.

\begin{definition}{pomset}({\em Pomset}).
A {\em labelled partial ordered set (elpo)} is a triple $(E,\leq,l)$
with $E$ a set, $\leq$ a partial order on $E$, and $l$ a function with
domain $E$. Two elpos $(E,\leq_E,l_E)$ and $(F,\leq_F,l_F)$ are {\em
isomorphic} if there exists a bijective function $i:E \rightarrow F$
(an {\em isomorphism}) such that, for $e,e' \in E$, $e \leq_E e'
\Leftrightarrow i(e) \leq_F i(e')$ and $l_F(i(e))=l_E(e)$. Of course
isomorphism ($\cong$) is an equivalence relation, and an equivalence
class of isomorphic elpos is called a {\em partial ordered multiset}
or {\em pomset}.
\end{definition}
A first idea of what could be the branching structure of a process $p
\in \IP$, is the pomset with representative $({\it run}(p),\leq,l)$. This I
will call the {\em strict branching structure} of $p$, as it
corresponds with the idea that the branching of all, possibly
indistinguishable, runs is taken into account. In order to
arrive at a less strict definition, one needs to identify certain
runs.

\begin{definition}{congruence}({\em Congruence}).
If $\sim$ is an equivalence relation on a set $E$, then $E/_{\sim}$
denotes the set of equivalence classes of $\sim$ and $[e]_{\sim}$
denotes the equivalence class containing $e \in E$.

A {\em congruence relation} on an elpo $(E,\leq,l)$ is an equivalence
relation $\sim$ on $E$, such that $$e \sim f \Rightarrow l(e)=l(f)~~
\mbox{and} ~~\exists e' (e \leq e' \sim f') \Leftrightarrow \exists f
(e \sim f \leq f').$$ If $\sim$ is a congruence on an elpo
$(E,\leq,l)$, then $\leq_{\sim}$ and $l_{\sim}$ are
defined on $E/_{\sim}$ by $$[e]_{\sim} \leq_{\sim} [f']_{\sim}
\Leftrightarrow \exists e' \in [f']_{\sim} (e \leq e') \left(
\rule{0mm}{5mm} \Leftrightarrow \exists f \in [e]_{\sim} (f \leq f')
\right)~~ \mbox{and} ~~l_{\sim} ([e]_{\sim}) = l(e).$$ Note that these
definitions are independent of the choice of representatives $e \in
[e]_{\sim}$ and $f' \in [f']_{\sim}$.
\end{definition}
This is the intermediate variant of three possible generalizations of
the concept of a congruence from algebras to algebraic structures with
relations. A {\em strong} congruence would even require that $e\sim f
\wedge e'\sim f' \Rightarrow ( e\leq e' \Leftrightarrow f\leq f')$, so
that $\leq_{\sim}$ can simply be defined by $[e]_{\sim} \leq_{\sim}
[e']_{\sim} \Leftrightarrow e \leq e'$. A {\em weak} congruence
on the other hand doesn't require anything for $\leq$, and
$\leq_{\sim}$ needs to be defined by $[e]_{\sim} \leq_{\sim} [e']_{\sim}
\Leftrightarrow \exists f \in [e]_{\sim}, f'\in [e']_{\sim} (f \leq f')$.

\begin{definition}{branching}
The {\em branching structure} of a process $p$ is the isomorphism
class of $({\it run}(p)/_{\sim},\leq_{\sim},l_{\sim})$, where $\sim$ is the
coarsest congruence on $({\it run}(p),\leq,l)$.
An equivalence $\equiv$ on $\IP$ {\em respects the branching structure
of processes} if $p\equiv q \Rightarrow [({\it run}(p)/_{\sim},\leq_{\sim},
l_{\sim})]_{\cong} = [({\it run}(q)/_{\sim},\leq_{\sim},l_{\sim})]_{\cong}$.
\end{definition}
Obviously a coarsest congruence on a pomset exists, as the union of
arbitrary many congruences is again a congruence. The following
observations are meant as tool for deciding whether or not a model or
equivalence respects branching time.

\begin{lemma}{branching}
Two processes $p,q \in \IP$ have the same branching structure iff
there exists congruences $\sim_p$ and $\sim_q$ such that
$({\it run}(p)/_{\sim_p},\leq_{\sim_p},l_{\sim_p}) \cong
({\it run}(q)/_{\sim_q},\leq_{\sim_q},l_{\sim_q})$.
\end{lemma}
\pf
This follows immediately from the following two facts, whose proofs are
straightforward.
\begin{itemize}
\item If $\sim$ is the coarsest and $\sim_1$ any congruence on an
elpo $(E,\leq,l)$, and $\sim_2$ is the coarsest congruence on
$(E/_{\sim_1},\leq_{\sim_1},l_{\sim_1})$, then
$(E/_{\sim_1}/_{\sim_2},{\leq_{\sim_1}}_{\sim_2},{l_{\sim_1}}_{\sim_2})
\cong (E/_{\sim},\leq_{\sim},l_{\sim})$.
\item If $(E,\leq,l) \cong (F,\leq,l)$ and $\sim$ is a congruence on
$(E,\leq,l)$, then there is a congruence $\sim'$ on $(F,\leq,l)$ such
that $(E/_{\sim},\leq_{\sim},l_{\sim}) \cong
(F/_{\sim'},\leq_{\sim'},l_{\sim'})$. Moreover, $\sim'$ is the
coarsest iff $\sim$ is.\hfill $\Box$
\end{itemize}

\begin{proposition}{branching}
Two processes $p,q \in \IP$ have the same branching structure iff
there exists a relation $R \subseteq {\it run}(p) \times {\it run}(q)$
with domain ${\it run}(p)$ and range ${\it run}(q)$, satisfying $$e R
f \Rightarrow l(e)=l(f),~~\exists e' (e \leq e' R f')
\Leftrightarrow \exists f (e R f \leq f')~~ \mbox{and} ~~\exists f' (f
\leq f' R^{-1} e') \Leftrightarrow \exists e (f R^{-1} e \leq e').$$
\end{proposition}
\begin{proof}
``If'': Let $R$ be such a relation. Define $\sim_p$ (and similarly
$\sim_q$) by $$e \sim_p e' \Leftrightarrow e=e_0Rf_1R^{-1}e_1Rf_2
R^{-1}e_2R \ldots Rf_nR^{-1}e_n=e' ~(n \geq 0).$$
It is easy to see that $\sim_p$ is a congruence relation. Moreover,
the function $i:{\it run}(p)\rightarrow {\it run}(q)$ defined by $i([e]_{\sim_p}) =
[f]_{\sim_q}$ for some $f \in {\it run}(q)$ with $eRf$, is well defined and an
isomorphism.\\
``Only if'': Let $i:{\it run}(p)/_{\sim} \rightarrow {\it run}(q)/_{\sim}$ be an
isomorphism. Define $R$ by $eRf \Leftrightarrow i([e]_{\sim}) =
[f]_{\sim}$. Again it is straightforward to check that $R$ has the
required properties.
\end{proof}

\section{The case of labelled transition spaces with and without $\tau$}

In this section I will instantiate the general definition of branching
time from the previous section for equivalences on models of
concurrency that can be regarded as labelled transition spaces.

\begin{definition}{LTS}{}
A {\em labelled transition space (LTS)} is a pair $(\IP,
\rightarrow)$ with $\IP$ a class (of {\em processes}) and
$\rightarrow \subseteq \IP \times Act \times \IP$ for $Act$ a set (of
{\em actions}), such that for $p \in \IP$ and $a \in
Act$ the class $\{q \in \IP \mid p \goto{a} q \}$ is a set.
\end{definition}
{\bf Notation:} Write $p \goto{a} q$ for $(p,a,q) \in
\rightarrow$ and $p \goto{a}$ for $\exists q \in \IP: p
\goto{a} q$.\\[12pt plus 5pt minus 7pt]
The elements of $\IP$ represent the processes we are interested in,
and $p \goto{a} q$ means that process $p$ can evolve into process $q$
while performing the action $a$. I use the word `space' instead
of `system' to emphasize that the elements of an LTS are {\em all}
systems under investigation, and not merely the states of a single
system.

\begin{definition}{run}({\em Run}).
A sequence of transitions $p_0\goto{a_1}p_1\goto{a_2}p_2
\cdots p_{n-1}\goto{a_n}p_n$ for $n \in \IN$ in an LTS
$(\IP,\rightarrow)$ is called a {\em run} of $p_0$.
Let ${\it run}(p)$ be the set of runs of a process $p\in \IP$, and let
$\leq$ be the prefix ordering on runs.
\end{definition}
It remains to determine the observable content of a run.
In case all actions are observable, let\linebreak
$l(p_0\goto{a_1}p_1\goto{a_2}p_2 \cdots p_{n-1}\goto{a_n}p_n) = a_1
a_2 \cdots a_n$. In case $Act = A \!\dcup\! \{\tau\}$, where $\tau$
denotes an internal\linebreak or unobservable 
action, the observable content $l(e)$ of a run $e$ is the same
sequence, but from which all $\tau$'s are removed. This completes the
definition of the branching structure of members of an LTS.

\begin{definition}{back}({\em Back and forth bisimulation}, {\sc De
Nicola, Montanari \& Vaandrager} \cite{DMV90}).
Let $(\IP,\rightarrow)$ be an LTS. Two processes $p,q \in \IP$ are
{\em weakly back and forth bisimilar} if there exists a relation $R
\subseteq {\it run}(p) \times {\it run}(q)$, called a {\em weak back
and forth bisimulation}, satisfying
\begin{list}{\bf --}{\topsep 0pt \parsep 0pt \itemsep 0pt}
\item $\lambda R \lambda$;
\item if $eRf$ and $e\dto{\sigma}e'$ (for $\sigma \in A^*$),
      then there exists an $f'$ such that $f \dto{\sigma}f'$ and $e'Rf'$;
\item if $e'Rf'$ and $e\dto{\sigma}e'$ (for $\sigma \in A^*$),
      then there exists an $f$ such that $f \dto{\sigma}f'$ and $eRf$;
\item if $eRf$ and $f\dto{\sigma}f'$ (for $\sigma \in A^*$),
      then there exists an $e'$ such that $e \dto{\sigma}e'$ and $e'Rf'$;
\item if $e'Rf'$ and $f\dto{\sigma}f'$ (for $\sigma \in A^*$),
      then there exists an $e$ such that $e \dto{\sigma}e'$ and $eRf$.
\end{list}
Here $\lambda$ denotes the empty run and $e \dto{\sigma} e'$ means
$e \leq e' \wedge l(e')=l(e)\sigma$.
\end{definition}

\begin{theorem}{branching}
Let $\IP$ be an LTS. Two processes $p,q \in \IP$ have the same
branching structure iff they are weakly back and forth bisimilar.
\end{theorem}

\begin{proof}
Immediately from \pr{branching}.
\end{proof}
In \cite{DMV90} is has been established that weak back and forth
bisimulation equivalence coincides with branching bisimulation
equivalence. Hence is follows that

\begin{corollary}{branching}
A semantic equivalence on a labelled transition space respects the
branching structure of processes iff it is finer than or equal to
branching bisimulation equivalence.\hfill$\Box$
\end{corollary}
If in \df{branching} the coarsest congruence would be replaced by the
coarsest {\em weak} congruence, the resulting `branching structure'
would have a distinct linear time flavour, as it would be nothing more
than the so-called {\em trace set} of a process. The coarsest {\em
strong} congruence on the other hand would on an LTS be the identity
relation, causing the branching structure to become the {\em strict}
branching structure. On an LTS two processes have the same strict
branching structure iff they are\linebreak tree equivalent, as follows
immediately from the definitions. Silent actions play no special
r\^ole here.

\section{Other models}

Term models, in which a process is represented as an expression in a
system description language, labelled event structures, Petri nets,
process graphs, and many other models of concurrency can be regarded
as labelled transition spaces. Namely, there are canonical definitions
of the transition relations $\goto{a}$ between two terms, event
structures, nets, etc. For these models the definitions of runs and
their visible content from the previous section apply, and hence it
is determined what it means for a semantic equivalence on such a model
to respect branching time. Unless causality is taken to be part of the
observable content of runs, in which case $l(e)$ could be modelled as
a {\em mixed ordering} (cf.\ {\sc Degano, De Nicola \& Montanari}
\cite{DDM89}) and the coarsest branching time equivalence would be
{\em history preserving branching bisimulation equivalence}.

Some models however, such as the {\em failures model} of {\sc Brookes,
Hoare \& Roscoe} \cite{BHR84}, can not be regarded as labelled
transition spaces. In these cases it is often difficult to associate
with a process a prefix-ordered set of runs. However, usually such a
model can be canonically interpreted as the homomorphic image of a
labelled transition space.  In that case the model can be said to {\em
respect branching time} iff the canonical homomorphism does not map two
processes which have a different branching structure to the same
element. Similarly, an equivalence on such a model respects branching
time iff no two images of processes with a different branching
structure are equivalent.

\section{What is nice about branching time?}

Semantic equivalences (and preorders) for concurrent systems are used
as criteria for determining whether implementations (say of a
protocol) meet specifications. The choice of a suitable equivalence
(or preorder) can be motivated by means of a {\em testing scenario}. Such
a scenario associates to every system a set of `observable'
properties.  These properties should be the ones that are important in
the given application. Now the equivalence should be such that two
processes are related {\bf only} if they have the same observable behaviour
(and for preorders the observable properties of the one should be
included in those of the other). But this still leaves us with an
abundance of suitable equivalences to choose from. Here one is faced
with two opposite strategies.

One strategy is to choose the unique equivalence that relates two
systems {\bf if} and only if they have the same observable behaviour.  This
equivalence is said to be {\em fully abstract} with respect to the
selected testing scenario. The advantage of a fully abstract
equivalence is that it never fails to identify two processes if they
have the same observable behaviour. For this reason it may be the best
choice if the testing scenario is known and fixed once and forever. In
practice however, there appears to be doubt and difference of opinion
concerning the observable behaviour of systems. Moreover, what is
observable may depend on the nature of the systems on which the
concept will be applied and the context in which they will be
operating. A big disadvantage of equivalences that are fully abstract
with respect to non-stable notions of observability is that whenever a
verification is carried out using a such an equivalence, and one
decides that the context in which the verified system will be working
is such that actually a little bit more can be observed that what was
originally accounted for, the verification has to be completely
redone.  Moreover, the correctness of the investigated systems keeps
depending on the completeness of the underlying testing scenario.

\pagebreak
The opposite strategy is based on a concept of `internal structure' of
processes. The internal structure of a process should be such that for
any reasonable notion of observability you can imagine, if two
processes have the same internal structure they surely have the same
observable behaviour. According to this strategy a suitable equivalence
should respect the internal structure of processes: if two processes
are equivalent they must have the same internal structure.  Preferably
the equivalence should be `fully abstract' with respect to this
structure: processes with a different internal structure should be
distinguished. This to maximize the applicability of the notion.  A
disadvantage of this strategy is that the selected equivalence may
fail to identify two processes with the same observable behaviour
merely because they have a different internal structure. But the
advantage is that verifications (of the equivalence of two processes)
based on this strategy automatically count as verifications in any
equivalence that is fully abstract with respect to a testing scenario,
and keep being valid if the insight in what is observable changes.
Moreover, when applying such an equivalence all bothersome
considerations about observability can be skipped.

In models of concurrency that abstract from divergence, true
concurrency, real-time behaviour and stochastic aspects of systems,
and represent actions by uninterpreted symbols, it appears that the
internal structure of processes can be formalized as their branching
structure. This makes branching bisimulation equivalence a preferred
tool for verifications. The internal structure strategy recommends to
try a verification first in branching bisimulation semantics, and only
when this fails move to a coarser equivalence that still seems
appropriate for the given application. In this move to a coarser
equivalence it would still be recommendable to minimize the amount of
water (linear time) in the wine. But of course in situations where the
appropriate testing scenario is beyond doubt, the full abstraction
strategy is recommendable, and would rarely yield so fine a
semantics as branching bisimulation.

One could argue that the strict branching structure would be an even
better formalization of the internal structure of processes. This would
make tree equivalence a preferred option. Although this argument by
itself has some merit, the use of tree semantics has serious
drawbacks. To name a few, the standard operational and denotational
semantics of CCS-like system description languages do not coincide
module tree equivalence, and deciding tree equivalence of regular
processes has a higher complexity than deciding branching bisimulation
equivalence. But most importantly, whereas in many verifications the
specification and implementation are actually branching bisimulation
equivalent, it rarely occurs that they are tree equivalent.

Another counterargument could be that there is an equivalence coarser
than branching bisimulation that, although not respecting the
branching structure of processes, respects their internal structure to
a sufficient degree to guarantee that any reasonable testing scenario
yields an equivalence that is at least as coarse. The most likely
candidates for such an equivalence are weak bisimulation or, as
argued in the absence of silent moves in {\sc Bloom, Istrael \&
Meyer} \cite{BIM88}, {\em ready simulation}. However, in {\sc Van
Glabbeek} \cite{vG93b} I present a testing scenario for branching
bisimulation that is arguably only twice as contrived as that of weak
bisimulation. Moreover, I argue that in the presence of silent moves
the case for ready simulation is not so compelling as in the
$\tau$-free situation, and present a situation in which a more
discriminating equivalence is called for.

In models of concurrency that do not abstract from true concurrency
etc.\ the internal structure of a process may include more than just
its branching structure. The argument presented here can just as well
be used to prefer causality respecting semantics for instance.

\pagebreak
\begin{thebibliography}{1}

\bibitem{BBKM84}
{\sc J.W.~de Bakker, J.A. Bergstra, J.W. Klop \& J.-J.Ch. Meyer} (1984):
\newblock {\em Linear time and branching time semantics for recursion with merge.}
\newblock {\sl Theoretical Computer Science} 34, pp. 135--156.

\bibitem{BIM88}
{\sc B.~Bloom, S.~Istrail \& A.R. Meyer} (1988):
\newblock {\em Bisimulation can't be traced: Preliminary report.}
\newblock In {\sl Conference Record of the $15^{th}$ ACM Symposium on Principles of Programming Languages, {\rm San Diego, California}}, pages 229--239.
\newblock Full version available as Technical Report 90-1150, Department of Computer Science, Cornell University, Ithaca, New York, August 1990. Accepted to appear in {\sl Journal of the ACM}.

\bibitem{BHR84}
{\sc S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {\sl Journal of the ACM} 31(3), pp. 560--599.

\bibitem{DDM89}
{\sc P.~Degano, R.~De~Nicola \& U.~Montanari} (1989):
\newblock {\em Partial orderings descriptions and observations of nondeterministic concurrent processes.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, {\rm Noordwijkerhout}}, {\sl \rm LNCS} 354, Springer-Verlag, pp. 438--466.

\bibitem{DMV90}
{\sc R.~De~Nicola, U.~Montanari \& F.W. Vaandrager} (1990):
\newblock {\em Back and forth bisimulations.}
\newblock In J.C.M. Baeten \& J.W. Klop, editors: {\sl Proceedings CONCUR 90, {\rm Amsterdam}}, {\sl \rm LNCS} 458, Springer-Verlag, pp. 152--165.

\bibitem{vG93b}
{\sc R.J.~van Glabbeek} (1993):
\newblock {\em The linear time -- branching time spectrum {II}; the semantics of sequential systems with silent moves.}
\newblock Preliminary version available from {\tt boole.stanford.edu}.
\newblock Extended abstract to appear in {\sl Proceedings CONCUR 93}, Hildesheim, Germany, LNCS, Springer-Verlag.

\bibitem{GW89}
{\sc R.J.~van Glabbeek \& W.P. Weijland} (1989):
\newblock {\em Branching time and abstraction in bisimulation semantics (extended abstract).}
\newblock In G.X. Ritter, editor: {\sl Information Processing 89}, North-Holland, pp. 613--618.
\newblock Full version available as Report CS-R9120, CWI, Amsterdam, 1991.

\bibitem{Mi90ccs}
{\sc R.~Milner} (1990):
\newblock {\em Operational and algebraic semantics of concurrent processes.}
\newblock In J.~van Leeuwen, editor: {\sl Handbook of Theoretical Computer Science}, chapter~19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201--1242.
\newblock Alternatively see{ \em Communication and Concurrency}, Prentice-Hall International, Englewood Cliffs, 1989, of which an earlier version appeared as{ \em A Calculus of Communicating Systems}, LNCS 92, Springer-Verlag, 1980.

\bibitem{Pn85}
{\sc A.~Pnueli} (1985):
\newblock {\em Linear and branching structures in the semantics and logics of reactive systems.}
\newblock In W.~Brauer, editor: {\sl Proceedings $\em 12^{th}$ ICALP, {\rm Nafplion}}, {\sl \rm LNCS} 194, Springer-Verlag, pp. 15--32.

\end{thebibliography}
\end{document}
