查看文章

Concurrent transition systems (CTS's), are ordinary nondeterministic transition systems that have been equipped with additional concurrency information. This concurrency information is specified in terms of a binary residual operation on transitions, which describes how certain pairs of transitions “commute.” The defining axioms for a CTS generate a rich algebraic theory, which we develop in detail. Each CTS C freely generates a complete CTS or computational category C^∗, whose arrows are equivalence classes of finite computation sequences, modulo a congruence induced by the residual operation. The notion “computation tree” for ordinary transition systems generalizes to computation diagram for CTS's, leading to the convenient definition of computations of a CTS as the ideals of its computation diagram. A pleasant property of this definition is that the notion of a maximal ideal in certain circumstances can …