A note on powerdomains and modality

  • Glynn Winskel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 158)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AP]
    Apt, K.R. and Plotkin, G.D. A Cook's tour of Countable Nondeterminism. Lecture Notes in Comp. Sc. Vol.115, ICALP 1981.Google Scholar
  2. [D]
    Dummett, M., Elements of Intuitionism. Oxford University Press (1977).Google Scholar
  3. [Gue]
    Guessarian, I., Algebraic Semantics. Springer-Verlag LNCS Vol.99 (1981).Google Scholar
  4. [HM]
    Hennessy, M.C.B. and Milner, R., On observing nondeterminism and concurrency, Springer LNCS Vol. 85. (1979).Google Scholar
  5. [HN]
    Hennessy, M.C.B., and de Nicola, R., Testing Equivalences for Processes, Internal Report, University of Edinburgh, (July 1982).Google Scholar
  6. [HP]
    Hennessy, M.C.B. and Plotkin, G., Full Abstraction for a Simple Parallel Programming Languages, LNCS Vol 74 (1979).Google Scholar
  7. [Ho]
    Hoare, C. A. R., A Model for Communicating Sequential Processes, Technical Report PRG-22, Programming Research Group, Oxford University Computing Lab. (1981).Google Scholar
  8. [LO]
    Lamport, L., and Owicki, S., Proving Liveness Properties of Concurrent Programs, Technical Report, SRI International (1980).Google Scholar
  9. [P1]
    Plotkin, G., A powerdomain construction, SIAM J. on computing, 5, pp.452–486, 1976.CrossRefGoogle Scholar
  10. [P2]
    Plotkin, G., A Powerdomain for countable non-determinism, Springer-Verlag Lecture Notes in Comp. Sc. 140 (1982).Google Scholar
  11. [Smy]
    Smyth, M., Powerdomains. JCSS Vol.16 No.1 (1978).Google Scholar
  12. [S]
    Scott, D., Domains for Denotational Semantics, Springer-Verlag Lecture Notes in Comp. Sc. 140 (1982).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Glynn Winskel
    • 1
  1. 1.Department of Computer ScienceCarnegie-Mellon UniversityPittsburgh

Personalised recommendations