The fixed point theory of unbounded non-determinism

Abstract This paper presents a fixed point theorem for the infinite traces model of CSP. Unlike any other model of CSP, there is no complete partial order over the infinite traces model whose fixed point theory agrees with the operational semantics (A. W. Roscoe, Oxford University Computing Laboratory Technical Monograph PRG-67, 1988). This arises from the introduction of unbounded non-determinism. However, the subset of pre-deterministic processes, that is those which describe the behaviour of a process on some run of its implementation, do form a subset for which the usual order is complete. By requiring that each CSP operator has a monotonic implementation which preserves pre-determinism, it is possible to show that all CSP operators have a least fixed point. In effect, it is the requirement that all operators have a methodical implementation.