Powerdomains

Let $(A,\sqsubseteq)$ be a lattice.

Define $(A',\subseteq)$ with $A'=2^A$ .

The lattice is exponentially larger, and it can be much more precise.

Example: applying powerdomain to interval lattice means that we can represent every possible set of states from concrete execution, because each element can be represented by abstract state with exact intervals.

Given $\gamma : A \to C$ , define $\gamma{}' : A' \to C$ by

$\begin{equation*} \gamma{}'(a') = \bigcup_{a \in a'} \gamma(a) \end{equation*}$

We define

$\begin{equation*} a'_1 \sqcup' a'_2 = a'_1 \cup a'_2 \end{equation*}$

and there is no approximation in $\sqcup'$ , that is,

$\begin{equation*} \gamma(a'_1 \sqcup' a'_2) = \gamma(a'_1) \cup \gamma(a'_2) \end{equation*}$

The abstraction function can be defined for each state, for $c \in C$ , we have $c \subseteq PS$ , so

$\begin{equation*} \alpha{}'(c) = \{ \alpha(\{s\}).\ s \in c \} \end{equation*}$

Example: Abstracting set $\{1,3,9\}$ by interval gives

$\begin{equation*} \alpha(\{1,3,9\}) = [1,9] \end{equation*}$

Abstracting it by powerset of interval gives

$\begin{equation*} \alpha'(\{1,3,9\}) = \{ \alpha(\{1\}), \alpha(\{3\}), \alpha(\{9\}) \} = \{ [1,1], [3,3], [9,9] \} \end{equation*}$

Also, we can define

$\begin{equation*} {sp{}'}^\#(a',r) = \{ sp^\#(a,r).\ a \in a' \} \end{equation*}$

Example:

$\begin{equation*} {sp{}'}^\#(\{ [1,1], [3,3], [9,9] \}, x:=x*x) = \{ [1,1], [9,9], [81,81] \} \end{equation*}$

With such large domain, widening is even more important.

A natural widening is to go back to non-power domain element:

$\begin{equation*} w(a') = \{ \sqcup a' \} \end{equation*}$

Example:

$\begin{equation*} w(\{ [1,1], [9,9], [81,81] \}) = \{ [1,81] \} \end{equation*}$

We can also apply the standard interval widening (with “jumps”) on top of this.

So, we can get precision or efficiency, depending on the use of widening.