BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/connections.dvi
       ENTRY:: July 24, 1994
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Connections between a Concrete and an Abstract Model of
                   Concurrent Systems
        TYPE:: Preprint
      AUTHOR:: Stark, Eugene W.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 516-632-8444 <stark@cs.sunysb.edu>
	DATE:: November, 1989
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~stark/REPORTS/connections.ps.gz
       NOTES:: A version of this paper appeared as:
                   "Connections Between a Concrete and an Abstract Model
                   of Concurrent Systems,"
                   Fifth Conference on the Mathematical Foundations of
                   Programming Semantics,
                   M. Main, A. Melton, M. Melton, D. Schmidt (eds.)
                   pp. 53-79,
                   Volume 442 of Lecture Notes in Computer Science,
                   Springer-Verlag, 1989.

ABSTRACT::

We define a concrete operational model of concurrent systems, called
*trace automata*.  For such automata, there is a natural notion of
*permutation equivalence* of computation sequences, which holds
between two computation sequences precisely when they represent two
interleaved views of the ``same concurrent computation.''
Alternatively, permutation equivalence can be characterized in terms
of a *residual operation* on transitions of the automaton, and
many interesting properties of concurrent computations can be
expressed with the help of this operation.  In particular, concurrent
computations, ordered by ``prefix,'' form a Scott domain whose
structure we characterize up to isomorphism.

By axiomatizing the properties of the residual operation, we obtain a
more abstract formulation of automata, which we call *concurrent
transition systems* (CTS's).  By exploiting a correspondence between
concurrent alphabets and certain CTS's, we are able to use the rich
algebraic structure of CTS's to obtain results in trace theory.
Finally, we connect CTS's and trace automata by obtaining a
characterization of those CTS's that correspond in a natural way to
trace automata, and we show how the correspondence suggests an
interesting notion of morphism of trace automata.

END:: SBCS//stark/connections.dvi