Probabilistic Abstract Interpretation.

PAI has been introduced in [21,22] as a probabilistic version of the classical abstract interpretation framework introduced by Cousot & Cousot. Given two probabilistic domains, $\mathcal C$ and $\mathcal D$, a probabilistic abstract interpretation is a pair of linear maps, $\bf A: \mathcal C\mapsto \mathcal D$ and $\bf G: \mathcal D\mapsto \mathcal C$, between the concrete domain $\mathcal C$ and the abstract domain $\mathcal D$, such that $\bf G$ is the Moore-Penrose pseudo-inverse of $\bf A$, and vice versa. The Moore-Penrose pseudo-inverse is defined as follows: Let $\mathcal C$ and $\mathcal D$ be two vector spaces and $\bf A: \mathcal C\mapsto \mathcal D$ a linear map between them. A linear map $\bf A^\dagger = \bf G: \mathcal D\mapsto \mathcal C$ is the Moore-Penrose pseudo-inverse of $\bf A$ iff

$$\bf A\circ \bf G= \bf P_{A} ~\mbox{ and }~ \bf G\circ \bf A= \bf P_{G}$$

where $\bf P_{A}$ and $\bf P_{G}$ denote orthogonal projections onto the ranges of $\bf A$ and $\bf G$. The projections are idempotent and self-adjoint; as a consequence, we can derive analogues of many of the properties of Galois connections that are used in the classical theory of abstract interpretation. A simple method to construct a probabilistic abstract interpretation is as follows. Given a linear operator $\Phi$ on some vector space $\mathcal V$ expressing the probabilistic semantics of a concrete system, and a linear abstraction function $\bf A:\mathcal V\mapsto\mathcal W$ from the concrete domain into an abstract domain $\mathcal W$, we compute the (unique) Moore-Penrose pseudo-inverse $\bf G=\bf A^\dagger$ of $\bf A$. The abstract semantics can then be defined as the linear operator on the abstract domain $\mathcal W$: $\Psi = \bf A\circ$ $\Phi$ $\circ \bf G$.