It is well known that recursion in a language requires a model in which sufficiently many functions have fixed points. In this approach, recursion is modeled by using least fixed points, which exist because of the order structure of the space being used. An alternative approach is to use a complete metric space, where the mappings are contractions, so that the Banach fixed point theorem assures that every self-map has a unique fixed point. Both of these approaches have been used in modeling CSP. The introduction of timing into the language forced the abandonment of the partial order approach in favor of the complete metric space approach, where all operators in the language are modeled as contraction mappings on the appropriate semantic domain. Moreover, this discussion applies only when the operators of the language are n-ary for some finite n. Neither of these variants of modeling theory is applicable to languages with infinite arity operators. The method used to overcome this problem was found by G. Barrett [1] and is based on partially ordered spaces.

This paper presents a simplification and generalization of Barrett’s method for untimed CSP. The treatment involves local complete partial orders (cpo’s), which are presented well in section 2. The rest of the paper contains the application of the theory to untimed CSP (section 3) and timed CSP (section 4).