查看文章

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 …