Denotational Models for Unbounded Nondeterminism1 1Work partially supported by the Office of Naval Research

AbstractUnbounded nondeterminism has played a fundamental role in the areas of refinement between models of languages supporting real-time constructs and in the treatment of fairness. Unlike bounded nondeterminism, unbounded nondeterminism has not been amenable to a satisfactory treatment using, for instance, the techniques of domain theory. In this paper we explore this issue, and we show that only one of the three powerdomains has a suitable analogue for modeling unbounded nondeterminism. In the process, we are forced to leave the realm of directed complete partial orders and continuous maps. The theory we develop is based on the theory first presented in [7], which itself was based on work on unbounded nondeterminism in untimed and Timed CSP