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.