# powerdomain

## powerdomain

(theory)
The powerdomain of a domain D is a domain containing some of the subsets of D. Due to the asymmetry condition in the definition of a partial order (and therefore of a domain) the powerdomain cannot contain all the subsets of D. This is because there may be different sets X and Y such that X <= Y and Y <= X which, by the asymmetry condition would have to be considered equal.

There are at least three possible orderings of the subsets of a powerdomain:

Egli-Milner:

X <= Y iff for all x in X, exists y in Y: x <= y and for all y in Y, exists x in X: x <= y

("The other domain always contains a related element").

Hoare or Partial Correctness or Safety:

X <= Y iff for all x in X, exists y in Y: x <= y

("The bigger domain always contains a bigger element").

Smyth or Total Correctness or Liveness:

X <= Y iff for all y in Y, exists x in X: x <= y

("The smaller domain always contains a smaller element").

If a powerdomain represents the result of an abstract interpretation in which a bigger value is a safe approximation to a smaller value then the Hoare powerdomain is appropriate because the safe approximation Y to the powerdomain X contains a safe approximation to each point in X.

("<=" is written in LaTeX as \sqsubseteq).
Mentioned in ?
References in periodicals archive ?
Kwak, "Powerdomain non-orthogonal multiple access (NOMA) in 5G systems: potentials and challenges", IEEE Communications Surveys & Tutorials, vol.
The event diagram together with the set of pending messages is said to form a powerdomain which is used to describe the concurrency of Actors.
[1986, Section 4], from F one gets in the most natural way its denotational "collecting" semantics f: P([N.sub.[perpendicular to]] x [N.sub.[perpendicular to]]) [right arrow] P([Bool.sub.[perpendicular to]]), where P is the Hoare powerdomain operator and [perpendicular to] denotes undefinedness (i.e., both nontermination and error).
[1986, Section 4], the concrete domains are given by the Hoare powerdomains P([N.sub.[perpendicular to]] X [N.sub.[perpendicular to]]) and P([Bool.sub.[perpendicular to]]), ordered by set inclusion, where, for any directed-complete partial order (CPO) P with least element, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], [down arrow] S = S, (T [subset or equal to] S and T directed) ??
It provides, for any suitable domain D, the powerdomain P(D) whose elements are subsets of D.
It contains a section on powerdomains, which were originally published in [32].
Another solution is presented by Ferguson and Hughes [1989] who consider a particular collection of convex sets: the cone powerdomain. They define a cone to be a convex set that is closed under least upper bound and show that least upper bounds of cones exist.
The modeling of uniform properties of recursive data structures builds on the work by Abramsky [1991b] on characterizing powerdomains logically, which in turn is inspired by Winskel's work on the relationship between modalities and powerdomains [Winskel 1983]; see also Gunter and Scott [1990].
Powerdomains and nondeterministic recursive functions.
Dijkstra's predicate transformers and Smyth's powerdomains. In Abstract Software Specifications, LNCS, Vol.
Dijkstra's predicate transformers and Smyth's powerdomains. Lecture Notes in Computer Science, D.

Site: Follow: Share:
Open / Close