A domain for concurrent termination a generalization of Mazurkiewicz traces

Abstract

This paper generalizes the concept of Mazurkiewicz traces to a description of a concurrent process, where a known prefix is given as a trace in a first component and a second alphabetic component yields some information about future actions. This allows to define a good semantic domain where the concatenation is continuous with respect to the Scott- and to the Lawson topology. For this we define the notion of α and of δ-trace. We show various mathematical results proving thereby the soundness of our approach. Our theory is a proper generalization of the theory of finite and infinite words (with explicit termination) and of the theory of finite and infinite (real and complex) traces. We make use of trace theory, domain theory, and topology.