True Concurrency can be Traced

In this paper sets of labelled partial orders are employed as fundamental mathematical entities for modelling nondeterministic and concurrent pro-cesses thereby obtaining so-called noninterleaving semantics. Based on clo-sures of sets of labelled partial orders, a simple recursive algebraic language with renement is given denotational models fully abstract w.r.t. correspond-ing behaviourally motivated equivalences.