Abstract
This paper presents a simplification and generalisation of Barren's “Fixed point theory of unbounded nondeterminism (FACS 3)” for untimed CSP. The difficulties of modeling unbounded nondeterminism in the untimed world persist to the timed case, where it remains the case that there is no reasonable complete partial order over the timed infinite traces model. The fact that the timed predeterministic processes are not a complete partial order means that the untimed approach is not directly applicable to the timed setting. The approach is extended here to a general theory of locally complete partial orders and dominating spaces. If every CSP operator is dominated by some operator on the dominating space, then the fixed point theory of the dominating space may be used to guarantee the existence of fixed points in the underlying CSP model. The application of this theory to untimed CSP is reviewed. The theory is then used to underpin the fixed point theory for timed CSP with infinite nondeterminism, by employing the complete metric space of deterministic timed processes to dominate the model.