PBES Abstraction

Wieger Wesselink, Tim Willemse

Absinthe

The Absinthe algorithm takes as input a PBES $p$ , a substitution on function symbols $\sigma_F:\mathcal{F}\rightarrow\mathcal{F}$ , and a substitution on sorts $\sigma_S:\mathcal{S}\rightarrow\mathcal{S}$ , where $\mathcal{F}$ is the set of function symbols and $\mathcal{S}$ is the set of sorts. For each $s\in domain(\sigma_S)$ there is a corresponding abstraction function $h_s$ .

Definitions

We define $FunctionSymbols(p)$ as the set of function symbols that occur in the PBES $p$ . For a sort $s$ we define $ContainerConstructors(s)$ as the set of constructor functions of the sorts $List(s)$ , $Set(s)$ and $Bag(s)$ . This includes for example the functions $[]{:}List(s)$ and ${\rhd}{:}s\times List(s)\rightarrow List(s)$ .

Algorithm

The algorithm first extends and modifies the substitution $\sigma_F$ . Then a transformation to $p$ is applied.

Step 1

The algorithm first extends the substitution $\sigma_F$ . Let

$A = \left( FunctionSymbols(p) \cup \bigcup_{s\in domain(\sigma_S)} ContainerConstructors(s) \right) \setminus domain(\sigma_F).$

For each function symbol $f_1\in A$ the substitution $\sigma_F$ is extended with $\sigma_F(f_1):=f_2$ , where $f_2$ is obtained from $f_1$ using

$\begin{array}{lcl} f_1{:}s_b & \mapsto & f_2{:}s_b^{\sigma_S} \\ f_1{:}C(s) & \mapsto & f_2{:}C(s)^{\sigma_S} \\ f_1{:}s_1\times\cdots\times s_n\rightarrow s & \mapsto & f_2{:}s_1^{\sigma_S}\times\cdots\times s_n^{\sigma_S}\rightarrow Set(s^{\sigma_S}), \end{array}$

where $s_b$ is a basic sort, $s_1\times\cdots\times s_n\rightarrow s$ is a function sort, and $C(s)$ is a container sort, and where $f_2$ is a fresh identifier.

Remark

The sort of $f_1$ may not contain any element of $domain(\sigma_S)$ as a subsort.

Remark

If $f_1$ is a function update, then the domain of the updated function may not contain any element of $domain(\sigma_S)$ as a subsort.

For each of the function symbols $f\in FunctionSymbols(p)\setminus domain(\sigma_F)$ a corresponding equation is introduced:

$\begin{array}{lcl} f_2 & = & \left\{\begin{array}{ll} h_{s_b}(f_1) & \text{if } s_b\in domain(\sigma_S) \\ f^{\sigma_S} & \text{otherwise} \end{array}\right. \\[8pt] f_2 & = & f_1^{\sigma_S} \\[8pt] f_2(x) & = & \left\{\begin{array}{ll} \{h_s(f_1(x))\} & \text{if } TargetSort(s)\in domain(\sigma_S) \\ \{f_1(x)\} & \text{otherwise,} \end{array}\right. \end{array}$

where $x{:}s_1^{\sigma_S}\times\cdots\times s_n^{\sigma_S}\rightarrow s^{\sigma_S}$ , and where $TargetSort$ is recursively defined as

$\begin{array}{lcl} TargetSort(s_b) & = & s_b \\ TargetSort(C(s)) & = & C(s) \\ TargetSort(s_1\times\cdots\times s_n\rightarrow s) & = & TargetSort(s). \end{array}$

Step 2

After this the substitution $\sigma_F$ is transformed. Each $(f_1,f_2)\in\sigma_F$ is replaced by $(f_1,f_3)$ , where $f_3$ is obtained from $f_2$ as follows:

$\begin{array}{lcl} f_2{:}s_b & \mapsto & f_3{:}Set(s_b) \\ f_2{:}C(s) & \mapsto & f_3{:}Set(C(s)) \\ f_2{:}s_1\times\cdots\times s_n\rightarrow s & \mapsto & f_3{:}Set(s_1)\times\cdots\times Set(s_n)\rightarrow s, \end{array}$

where $f_3$ is a fresh name.

For each pair $(f_2,f_3)$ a corresponding equation is generated:

$\begin{array}{lcl} f_3 & = & \{f_2\} \\[8pt] f_3 & = & \{f_2\} \\[8pt] f_3(X) & = & \bigl\{ y{:}s \mid \exists_{x{:}s_1\times\cdots\times s_n\rightarrow s}.\; x\in X \wedge y\in f_2(x) \bigr\}, \end{array}$

where $X{:}Set(s_1)\times\cdots\times Set(s_n)\rightarrow s$ .

Step 3

The PBES $p$ is transformed using the transformations $T$ and $U$ , defined recursively as:

$\begin{array}{lcl} T\!\left((\sigma_1 X_1(d_1{:}D_1)=\varphi_1)\cdots(\sigma_n X_n(d_n{:}D_n)=\varphi_n)\right) & = & \begin{array}[t]{l} (\sigma_1 \widehat{X_1}(d_1{:}D_1^{\sigma_S})=T(\varphi_1))\cdots \\ (\sigma_n \widehat{X_n}(d_n{:}D_n^{\sigma_S})=T(\varphi_n)) \end{array} \\[4pt] T(\lnot\varphi) & = & \lnot T(\varphi) \\ T(\varphi\oplus\psi) & = & T(\varphi)\oplus T(\psi) \\ T(X_i(e)) & = & \left\{\begin{array}{ll} \bigvee_{d\in T(e)}\widehat{X_i}(d) & \text{if it is an under-approximation} \\[2pt] \bigwedge_{d\in T(e)}\widehat{X_i}(d) & \text{if it is an over-approximation} \end{array}\right. \\[8pt] T(\forall_{d{:}D}.\varphi) & = & \forall_{d{:}D^{\sigma_S}}.T(\varphi) \\ T(\exists_{d{:}D}.\varphi) & = & \exists_{d{:}D^{\sigma_S}}.T(\varphi) \\ T(b) & = & \left\{\begin{array}{ll} false\in U(b) & \text{if it is an under-approximation} \\[2pt] true\in U(b) & \text{if it is an over-approximation} \end{array}\right. \\[8pt] U(v) & = & \{v^{\sigma_S}\} \\ U(f) & = & \sigma_F(f) \\ U(c) & = & \{h_s(c)\} \quad\text{if } c{:}s \text{ is a ground term and } s\in domain(\sigma_S) \\ U(f(x)) & = & U(f)(U(x)) \quad\text{(N.B.\ The general case } U(y(x)) \text{ is not supported!)} \\ U(\lambda_{d{:}D}.x) & = & \{v{:}s^{\sigma_S} \mid v=U(x)\}, \text{ where } x{:}s \\ U(\forall_{d{:}D}.x) & = & \text{?} \\ U(\exists_{d{:}D}.x) & = & \text{?} \\ U(x\ \mathbf{whr}\ y{:}=z) & = & \text{?} \end{array}$

where $\oplus\in\{\wedge,\vee,\Rightarrow\}$ . Note that $T$ operates on PBES expressions, and $U$ operates on data expressions.

PBES abstraction

Let $\mathcal{E}=(\sigma_1 X_1(d_{X_1}{:}D_{X_1})=\varphi_{X_1})\cdots(\sigma_n X_n(d_{X_n}{:}D_{X_n})=\varphi_{X_n})$ be a PBES, and let $V_i$ be a subset of the parameters in $d_{X_i}$ for $i=1\cdots n$ . Let $e\in\{true,false\}$ be a data expression. Then we define the algorithm $\mathsf{abstract}$ as follows:

$\begin{array}{lll} \mathsf{abstract}(d,V,e) & = & \left\{\begin{array}{ll} d & \text{if } \mathsf{freevar}(d)\cap V=\emptyset \\ e & \text{otherwise} \end{array}\right. \\[8pt] \mathsf{abstract}(\varphi\oplus\psi,V,e) & = & \mathsf{abstract}(\varphi,V,e)\oplus\mathsf{abstract}(\psi,V,e) \\[4pt] \mathsf{abstract}(\mathsf{Q}_{d_1{:}D_1,\ldots,d_m{:}D_m}.\varphi,V,e) & = & \mathsf{Q}_{d_1{:}D_1,\ldots,d_m{:}D_m}.\mathsf{abstract}(\varphi,V\setminus\{d_1{:}D_1,\ldots,d_m{:}D_m\},e) \\[4pt] \mathsf{abstract}(\sigma X(d_1{:}D_1,\ldots,d_m{:}D_m)=\varphi,V,e) & = & \sigma X(d_1{:}D_1,\ldots,d_m{:}D_m)=\mathsf{abstract}(\varphi,V,e) \\[8pt] \mathsf{abstract}(\mathcal{E},[V_1,\ldots,V_n],e) & = & \begin{array}[t]{l} (\sigma_1 X_1(d_{X_1}{:}D_{X_1})=\mathsf{abstract}(\varphi_{X_1},V_1,e)) \\ \quad\cdots \\ (\sigma_n X_n(d_{X_n}{:}D_{X_n})=\mathsf{abstract}(\varphi_{X_n},V_n,e)) \end{array} \end{array}$

with $d$ a data expression, $\oplus\in\{\wedge,\vee,\Rightarrow\}$ , $\mathsf{Q}\in\{\forall,\exists\}$ and $V\subset\{d_1{:}D_1,\ldots,d_m{:}D_m\}$ .

Motivation

The motivation for this algorithm is that if the solution of $\mathsf{abstract}(\mathcal{E},[V_1,\ldots,V_n],false)$ is $true$ , this implies that the solution of $\mathcal{E}$ is $true$ as well, and if the solution of $\mathsf{abstract}(\mathcal{E},[V_1,\ldots,V_n],true)$ is $false$ , this implies that the solution of $\mathcal{E}$ is $false$ .