A note on powerdomains and modality

Abstract

This note shows a simple connection between powerdomains and modal assertions that can be made about nondeterministic computations. We consider three kinds of powerdomains, the Plotkin powerdomain, the Smyth powerdomain and one Christened the Hoare powerdomain by Plotkin because it captures the partial correctness of a nondeterministic program. The modal operators are □ for “inevitably” and ♦ for “possibly”. It is shown in a precise sense how the Smyth powerdomain is built up from assertions about the inevitable behaviour of a process, the Hoare powerdomain is built up from assertions about the possible behaviour of a process while Plotkin powerdomain is built up from from both kinds of assertions taken together.