%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "glabbeekw96.ltx",
%%%     date      = "9 August 1996",
%%%     time      = "15:9:31 EDT",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "29553 112 548 4516",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 by ACM, Inc.
%%%                  Permission to make digital or hard copies of part
%%%                  or all of this work for personal or classroom use
%%%                  is granted without fee provided that copies are
%%%                  not made or distributed for profit or direct
%%%                  commercial advantage and that copies bear this
%%%                  notice and the full citation on the first page.
%%%                  Copyrights for components of this work owned by
%%%                  others than ACM must be honored. Abstracting with
%%%                  credit is permitted. To copy otherwise, to
%%%                  republish, to post on servers, or to redistribute
%%%                  to lists, requires prior specific permission
%%%                  and/or a fee. Request permissions from
%%%                  Publications Dept, ACM Inc., fax +1 (212)
%%%                  869-0481, or permissions@acm.org.
%%%
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{GlabbeekW96}

\title{Branching Time and Abstraction in Bisimulation Semantics}

\author{Rob~J. van Glabbeek \and W.~Peter Weijland}

\Pages{555--600}

\Month{May}

\Year{1996}

\Volume{43}

\Number{3}

\maketitle

\begin{abstract}

In comparative concurrency semantics, one usually distinguishes between
  \emph{linear time} and \emph{branching time} semantic equivalences. Milner's
  notion of \emph{observation equivalence} is often mentioned as the standard
  example of a branching time equivalence. In this paper we investigate whether
  observation equivalence really does respect the branching structure of
  processes, and find that in the presence of the unobservable action~$\tau$ of
  CCS this is not the case. \par Therefore, the notion of \emph{branching
  bisimulation equivalence} is introduced which strongly preserves the
  branching structure of processes, in the sense that it preserves computations
  together with the potentials in all intermediate states that are passed
  through, even if silent moves are involved. On closed CCS-terms branching
  bisimulation congruence can be completely axiomatized by the single axiom
  scheme \[ a.(\tau.(y + z) + y) = a.(y + z) \] (where $a$~ranges over all
  actions) and the usual laws for strong congruence. \par We also establish
  that for sequential processes observation equivalence is not preserved under
  refinement of actions, whereas branching bisimulation is. \par For a large
  class of processes, it turns out that branching bisimulation and observation
  equivalence are the same. As far as we know, all protocols that have been
  verified in the setting of observation equivalence happen to fit in this
  class, and hence are also valid in the stronger setting of branching
  bisimulation equivalence.

\end{abstract}

\begin{categories}

D.3.1 [\textbf{Programming Languages}]: Formal Definitions and Theory;
F.1.2 [\textbf{Computation by Abstract Devices}]: Modes of Computation;
F.3.2 [\textbf{Logics and Meanings of Programs}]: Semantics of
Programming Languages;
F.4.3 [\textbf{Mathematical Logic and Formal Languages}]: Formal Languages

\end{categories}

\begin{keywords}

Abstraction, action refinement, bisimulation, branching time, concurrency,
  process algebra, semantic equivalence

\end{keywords}

\end{document}