True concurrency can be traced

Abstract

In this paper sets of labelled partial orders are employed as fundamental mathematical entities for modelling nondeterministic and concurrent processes thereby obtaining so-called noninterleaving semantics. Based on closures of sets of labelled partial orders, a simple algebraic language with refinement is given denotational models fully abstract w.r.t. corresponding behaviourally motivated equivalences.