%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "bloomim95.ltx",
%%%     date      = "20 November 1995",
%%%     time      = "21:41:31 EST",
%%%     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  = "37086 103 404 3534",
%%%     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{BloomIM95}

\title{Bisimulation Can't Be Traced}

\author{Bard Bloom \and Sorin Istrail \and Albert~R. Meyer}

\Pages{232--268}

\Month{January}

\Year{1995}

\Volume{42}

\Number{1}

\maketitle

\begin{abstract}

In the concurrent language CCS, two programs are considered the same if they
  are \emph{bisimilar}. Several years and many researchers have demonstrated
  that the theory of bisimulation is mathematically appealing and useful in
  practice. However, bisimulation makes too many distinctions between programs.
  We consider the problem of adding operations to CCS to make bisimulation
  fully abstract. We define the class of GSOS operations, generalizing the
  style and technical advantages of CCS operations. We characterize GSOS
  congruency in as a bisimulation-like relation called \emph{ready simulation}.
  Bisimulation is strictly finer than ready simulation, and hence not a
  congruence for any GSOS language.

\end{abstract}

\begin{categories}

D.3.1[semantics]; D.3.3[concurrent programming structures]; F.3.2[algebraic
  approaches to semantics; operational semantics]; I.6.2

\end{categories}

\begin{terms}

Languages, Theory, Verification

\end{terms}

\begin{keywords}

Bisimulation, structural operational semantics, process algebra, CCS

\end{keywords}

\end{document}
