source: papers/FDL2012/abstraction_refinement.tex

\subsection{Properties of good refinement}
When a counterexample is found to be spurious, it means that the current abstract model $\widehat{M}_i$ is too coarse and has to be refined.
In this section, we will discuss about the refinement technique based on the integration of more verified properties of the concrete model's components in the abstract model to be generated. Moreover, the refinement step from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ respects the properties below:

%\medskip

\begin{definition} An efficient \emph{refinement} verifies the following properties:
\vspace*{-2mm}
\begin{enumerate}
\itemsep -0.3em
\item The new refinement is an over-approximation of the concrete model:
$\widehat{M} \sqsubseteq \widehat{M}_{i+1}$.
\item The new refinement is more concrete than the previous one:
$\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$.
\item The spurious counterexample in $\widehat{M}_i$ is  removed from
$\widehat{M}_{i+1}$.
\end{enumerate}
\label{def:goodrefinement}
\end{definition}
Furthermore, the refinement steps should be easy to compute and ensure a fast
convergence by minimizing the number of iterations of the CEGAR loop.

Refinements based on the concretization of selected abstract variables in
$\widehat{M}_i$ ensure item 2. Concretization can be performed by
modifying the AKS of $\widehat{M}_i$ by changing some abstract value to
concrete ones. However, this approach is rude: in order to ensure item 1,
the concretization needs to be consistent with the sequences of values in the concrete system. The difficulty resides in defining the proper abstract variable to concretize, at which precise instant, and with which Boolean value.
%Another way to concretize some variables at selected instants is to compose
%(by a synchronous product) the AKS  of $\widehat{M}_i$ with a new AKS, provided this latest represents over-approximations of the set of behaviors of $M$. By construction, this product satisfies items 1 and 2. We now have to compute an AKS eliminating the spurious counterexample, being easily computable and ensuring a quick convergence of the CEGAR loop.

We propose to compose the abstraction with another AKS to build a good refinement
according to Definition \ref{def:goodrefinement}.
We have several options. The most straightforward method consists in building
an AKS representing all possible executions except the  spurious counterexample; however the AKS representation may be huge and the process is not guaranteed to converge. A second possibility is to build an AKS with additional CTL properties of the components; the AKS remains small but item 3 is not guaranteed, hence delaying the convergence. The final proposal combines both previous ones: first local CTL properties eliminating the spurious counterexample are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.


\subsection{Negation of the counterexample}

The counterexample at a refinement step $i$, $\sigma$, is a path in the
abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the
counterexample given by the model-checker, the variable configuration in each
state is Boolean. We name $\widehat{L_i}$ this new labeling.
The spurious counterexample $\sigma$ is defined such that:
\begin{definition}
Let $\sigma$ be a \emph{spurious counterexample} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
%\vspace*{-2mm}
\begin{itemize}
%\topsep 0pt
\itemsep -0.3em
\item All its variables are concrete: $\forall s_i$ and $\forall p\in
\widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$.
(not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
\item  $\sigma$ is a counterexample in  $\widehat{M}_i$: $s_0\not\models \Phi$.
\item  $\sigma$ is not a path of the concrete system $M$: $\exists k \in [1..n-1]$ such
that $\forall j < k, (s_j,s_{j+1}) \in R$ and $(s_{k}, s_{k+1}) \not\in R$.
\end{itemize}
\end{definition}
The construction of the AKS representing all executions except the one
described by the spurious counterexample is done in two steps.

\subsubsection{Step 1~:~Build the structure of the AKS.}


\begin{definition}
Let $\sigma$ be a spurious counterexample of  length $|\sigma| = n$, the \emph{ AKS of the
counterexample negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
\widehat{F}_{\overline{\sigma}} \rangle$ is such that:
\vspace*{-2mm}
\begin{itemize}
%\topsep 0pt
\itemsep -0.3em
\item $AP_{\overline{\sigma}} = {AP}_i$:
The set of atomic propositions coincides with the one of $\sigma$

\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i\in
[0..n-2] \wedge s_i\in
\sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \wedge s_i\in \sigma\}$

\item $\widehat{L}_{\overline{\sigma}}$  with
$L_{\overline{\sigma}}(s_i') = L_i(s_i), \forall i \in [0..n-2]$ and
$L(s_T) = \{\top, \forall p \in AP_{\bar{\sigma}}\}$,
$L_{\overline{\sigma}}(\bar{s_i})$ is explained in the next construction step.

\item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$

\item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in
[0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup
\{(s_i',s_{i+1}',\forall  i\in[0..n-3]\}$

\item $\widehat{F}_{\overline{\sigma}} = \emptyset$
\end{itemize}
\end{definition}
The labeling function of $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
configurations {\it but} the one of $s_i$. This last set may not be representable by
the labeling function defined in Definition \ref{def-aks}. State labeling is treated
in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}.
%The size of this structure is linear with the size of the counter-example.

\subsubsection{Step 2~:~Expand state configurations representing the negation of a concrete configuration.}
%We return back to the labeling of states of $AKS(\overline{\sigma})$. As states $s'$ are associated with the same (concrete) configuration as their corresponding state in $\sigma$, their labeling is straightforward : $\forall i \in [0..n-1], {L}_{\overline{\sigma}}(s'_i) = \widehat{L}_{i}(s_i)$.
The set of configurations associated with a state $\bar{s_i}$ represents the
negation of the one represented by ${L}_i(s_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels.

\emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ the configuration associated with $s_0$ assigns false to each variable. The negation of this configuration represents a set of seven concrete configurations which are covered by three (abstract) configurations: $\{\{\mathbf{t},\top,\top\},\{\mathbf{f},\mathbf{t},\top\},\{\mathbf{f},\mathbf{f},\mathbf{t}\}\}$.

To build the final AKS representing all sequences but spurious counterexample
$\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by
$k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$
and assigns to each of them a label of $k$ variables $\{v_0, \ldots,
v_{k-1}\}$ defined such that : $\widehat{L}(\bar{s_i^j}) = \{\forall l \in [0..k-1],
v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. Each
state $\bar{s_i^j}$ is connected to the same predecessor and successor states
as state $\bar{s_i}$.

This final AKS presents a number of states in
$\cal{O}(\mid\sigma\mid\times\mid AP\mid)$. However, removing, at each
refinement step, the spurious counterexample {\em only} induces a low
convergence. Moreover, in some cases, this strategy may not converge: suppose
that all sequences of the form $a.b^*.c$ are spurious counterexamples (here
$a$, $b$ and $c$ represent concrete state configurations). Assume, at a given
refinement step $i$, a particular counterexample $\sigma_i = s_0 \rightarrow
s_1 \rightarrow \ldots s_n$ with $L(s_0) = a, \forall k \in [1, n-1], L(s_k) =
b, L(s_n) = c$. Removing this counterexample does not prevent from a new
spurious counterexample at step $i+1$ :  $\sigma_{i+1} = s_0 \rightarrow s_1
\rightarrow \ldots s_{n+1}$ with $L(s_0) = a, \forall k \in [1, n], L(s_k) =
b, L(s_{n+1}) = c$. The strategy consisting of elimination spurious
counterexample {\em one by one} diverges in this case. However, we cannot
eliminate all the sequences of the form $a.b^*.c$ in a unique refinement step
since we do not {\it a priori} know if at least one of these sequences is executable in the concrete model.

From these considerations, we are interested in removing {\em sets of
behaviors encompassing the spurious counterexample} but still guaranteeing an
over-approximation of the set of tree-organized behaviors of the concrete
model. The strengthening of the abstraction $\widehat{M}_i$ with the
addition of AKS of already verified local CTL properties eliminates sets of
behaviors and guarantees the over-approximation (Property
\ref{prop:concrete_compose}) but does not guarantee the elimination of the counterexample. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counterexample.





%\bigskip

%\begin{definition}
%\textbf{\emph{Spurious counterexample :}} \\
%\\
%Let $\sigma_c = \langle s_{c,0}, s_{c,1}, s_{c,2}, ... , s_{c,k}, s_{c,k+1}, ... , s_{c,n}\rangle$ a path of length $n$ in the concrete model $M$ and in each state of $\sigma_c$ we have $s_{c,k} = \langle v_{c,k}^1, v_{c,k}^2, ... ,  v_{c,k}^{p'}, ... , v_{c,k}^{q'} \rangle$ with $\forall p' \in [1,q'], ~v_{i,k}^{p'} \in V_{c,k}$ and $V_{c,k} \in 2^{q'}$.\\
%
%\smallskip
%
%If $\forall k$ we have $\widehat{V}_{i,k} \subseteq V_{c,k}$ and $\forall v_{\bar{a}i,k} \in \widehat{V}_{i,k}, ~s_{i,k}|_{v_{\bar{a}i,k}} = s_{c,k}|_{v_{c,k}} $ then $M \nvDash \phi$ else $\sigma_i$ is \emph{spurious}.
%
%\end{definition}



\subsection{Ordering of properties}

\input{ordering_filter_properties}