source: papers/FDL2012/abstraction_refinement.tex @ 64

\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} verified the following properties:
\begin{enumerate}
\item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$.
\item The new refinement is more concrete than the previous one:
$\widehat{M}_{i} \sqsubseteq \widehat{M}_{i+1}$.
\item The spurious counter-example in $\widehat{M}_i$ is  removed from
$\widehat{M_{i+1}}$.
\end{enumerate}
\end{definition}

Moreover, the refinement steps should be easy to compute and ensure a fast
convergence by the minimizing the number of iteration of the CEGAR loop.

Refinements based on the concretization of selected abstract variables in $\widehat{M}_i$ ensure item 2. Concretization can be performed either in modifying the AKS of $\widehat{M}_i$, by changing some abstract value to concrete ones, but this approach is rude : in order to ensure item 1, concretization needs to be coherent 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 counter-example, being easily computable and ensuring a quick convergence of the CEGAR loop.

Several proposals can be made. The most straightforward consists in building the AKS representing all possible executions except the  spurious counter-example ; 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 counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.


\subsection{Refinement by negation of the counterexample}

\TODO{Mettre la def avant ?}
\TODO{Rafinement par négation du contre-exemple}
The counterexample at a refinement step $i$, $\sigma$ is a path in the
abstract model $\widehat{M}_i$ which dissatisfy $\Phi$.  In the counterexample given by the model-checker, the variables' value in each states are boolean.
The spurious counter-example $\sigma$ is defined such that :
\begin{definition}
\textbf{\emph{The counterexample $\sigma$ :}} \\
\\
Let $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ and let the length of the
counterexample, $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
\begin{itemize}
\item All its variables are concrete: $\forall s_i$ and $\forall p\in
\widehat{AP}_i$, $p$ is either true or false
(not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
\item  $\sigma$ is a counter-example 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}

2. Negation of states in an AKS

a) An (abstract) configuration in a state of the AKS represents a (convex ?) set of states of the concrete component.

b) The negation of an configuration may be represented by a set of abstract configurations

c) building the AKS of a spurious counter-example may lead to a blow-up of the number of states of the AKS


%\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}

Before generating an abstract model to verify a global property $\phi$, the verified properties of all the components in the concrete model are ordered according to their pertinency in comparison to a global property $\phi$. In order to do so, the variable dependency of the variables present in global property $\phi$ has to be analysed. After this point, we refer to the variables present in the global property $\phi$ as \emph{primary variables}.

%\bigskip

The ordering of the properties will be based on the variable dependency graph.
The variables in the model are weighted according to their dependency level
\emph{vis-Ã -vis} primary variables and the properties will be weighted according to the sum of the weights of the variables present in it. We have decided to allocate a supplementary weight for variables which are present at the interface of a component whereas variables which do not interfere in the obtention of a primary variable will be weighted 0. Here is how we proceed:


\begin{enumerate}

\item {\emph{Establishment of primary variables' dependency and maximum graph depth}\\
Each primary variable will be examined and their dependency graph is elobarated. The maximum graph depth among the primary variable dependency graphs will be identified and used to calibrate the weight of all the variables related to the global property.
Given the primary variables of $\phi$, $V_{\phi} =  \langle v_{\phi_0}, v_{\phi_1}, ... , v_{\phi_k}, ... , v_{\phi_n} \rangle$ and $G{\_v_{\phi_k}}$ the dependency graph of primary variable $v_{\phi_k}$, we have the maximum graph depth $max_{d} = max(depth(Gv_{\phi_0}), depth(Gv_{\phi_1}), ... , depth(Gv_{\phi_k}), ... ,$\\$ depth(Gv_{\phi_n})) $.

}

\item {\emph{Weight allocation for each variables} \\
Let's suppose $max_d$ is the maximum dependency graph depth calculated and $p$ is the unit weight. We allocate the variable weight as follows:
\begin{itemize}
\item{All the variables at degree $max_d$ of every dependency graph will be allocated the weight of $p$.}
 \\ \hspace*{20mm} $Wv_{max_d} = p$
\item{All the variables at degree $max_d - 1$ of every dependency graph will be allocated the weight of $2Wv_{max_d}$.}
\\ \hspace*{20mm} $Wv_{max_d - 1} = 2Wv_{max_d}$
\item{...}
\item{All the variables at degree $1$ of every dependency graph will be allocated the weight of $2Wv_{2}$.}
 \\ \hspace*{20mm} $Wv_{1} = 2Wv_{2}$
\item{All the variables at degree $0$ (i.e. the primary variables) will be allocated the weight of $10Wv_{1}$.}
 \\ \hspace*{20mm} $Wv_{0} = 10Wv_{1}$
\end{itemize}

We can see here that the primary variables are given a considerable
ponderation due to their pertinency \emph{vis-Ã -vis} global  property. Furthermore, we will allocate a supplementary weight of $3Wv_{1}$ to variables at the interface of a component as they are the variables which assure the connection between the components if there is at least one variable in the dependency graph established in the previous step in the property. All other non-related variables have a weight equals to $0$.
}


\item {\emph{Ordering of the properties} \\
Properties will be ordered according to the sum of the weight of the variables in it. Therefore, given a property $\varphi_i$ which contains $n+1$ variables, $V_{\varphi_i} =  \langle v_{\varphi_{i0}}, v_{\varphi_{i1}}, ... , v_{\varphi_{ik}}, ... , v_{\varphi_{in}} \rangle$, the weight  of $\varphi_i$ , $W_{\varphi_i} = \sum_{k=0}^{n} Wv_{\varphi_{ik}}$ .
After this stage, we will check all the properties with weight $>0$ and allocate a supplementary weight of $3Wv_{1}$ for every variable at the interface present in the propery. After this process, the final weight of a property is obtained and the properties will be ordered in a list with the weight  decreasing (the heaviest first). We will refer to the ordered list of properties related to the global property $\phi$ as $L_\phi$.


}

\end{enumerate}

%\bigskip

\emph{\underline{Example:}}  \\

For example, if a global property $\phi$ consists of 3 variables: $ p, q, r $ where:
\begin{itemize}
\item{$p$ is dependent of $a$ and $b$}
\item{$b$ is dependent of $c$}
\item{$q$ is dependent of $x$}
\item{$r$ is independent}
\end{itemize}

Example with unit weight= 50.
The primary variables: $p$, $q$ and $r$ are weighted $100x10=1000$ each. \\
The secondary level variables : $a$, $b$ and $x$ are weighted $50x2=100$ each. \\
The tertiary level variable $c$ is weighted $50$. \\
The weight of a non-related variable is $0$.

So each verified properties available pertinency will be evaluated by adding the weights of all the variables in it. It is definitely not an exact pertinency calculation of properties but provides a good indicator of their possible impact on the global property.

\bigskip
\begin{figure}[h!]
   \centering
%   \includegraphics[width=1.2\textwidth]{Dependency_graph_weight_PNG}
%     \hspace*{-15mm}
     \includegraphics{Dependency_graph_weight_PNG}
   \caption{\label{DepGraphWeight} Example of weighting}
\end{figure}

%Dans la figure~\ref{étiquette} page~\pageref{étiquette},  



After this pre-processing phase, we will have a list of properties $L_\phi  $ ordered according to their pertinency in comparison to the global property.







\subsection{Filtering properties}

The refinement process from $\widehat{M}_i$ to $\widehat{M}_{i+1}$ can be seperated into 2 steps:

\begin{enumerate}

\item {\emph{\underline{Step 1:}} \\

As we would like to ensure the elimination of the counterexample previously found, we filter out properties that don't have an impact on the counterexample $\sigma_i$ thus won't eliminate it. In order to reach this obective, a Kripke Structure of the counterexample $\sigma_i$, $K(\sigma_i)$ is generated. $K(\sigma_i)$ is a succession of states corresponding to the counterexample path which dissatisfies the global property $\phi$.

\bigskip

\begin{definition}
\textbf{\emph{The counterexample $\sigma_i$ Kripke Structure $K(\sigma_i)$ :}} \\
Let a counterexample of length $n$, $ \sigma_i = \langle s_{\bar{a}i,0}, s_{\bar{a}i,1},\\ s_{\bar{a}i,2}, ... , s_{\bar{a}i,k}, s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\rangle $ with $ \forall k \in [0,n-1]$, we have \\
$K(\sigma_i) = (AP_{\sigma_i}, S_{\sigma_i}, S_{0\sigma_i}, L_{\sigma_i}, R_{\sigma_i})$ a 5-tuple consisting of :

\begin{itemize}
\item { $AP_{\sigma_i}$ : a finite set of atomic propositions which corresponds to the variables in the abstract model $\widehat{V}_{i}$ }      
\item { $S_{\sigma_i} = \{s_{\bar{a}i,0}, s_{\bar{a}i,1}, s_{\bar{a}i,2}, ... , s_{\bar{a}i,k}, s_{\bar{a}i,k+1}, ... , s_{\bar{a}i,n}\}$}
\item { $S_{0\sigma_i} = \{s_{\bar{a}i,0}\}$}
\item { $L_{\sigma_i}$ : $S_{\sigma_i} \rightarrow 2^{AP_{\sigma_i}}$ : a labeling function which labels each state with the set of atomic propositions true in that state. }
\item { $R_{\sigma_i}$ = $ (s_{\bar{a}i,k}, s_{\bar{a}i,k+1})$ }
\end{itemize}
\end{definition}

%\bigskip
All the properties available are then model-checked on $K(\sigma_i)$.

If:
\begin{itemize}
\item {\textbf{$K(\sigma_i) \vDash \varphi  \Rightarrow \varphi $ will not eliminate $\sigma_i$}}
\item {\textbf{$K(\sigma_i) \nvDash \varphi  \Rightarrow \varphi $ will eliminate $\sigma_i$}}
\end{itemize}

%\bigskip


\begin{figure}[h!]
   \centering
%   \includegraphics[width=1.2\textwidth]{K_sigma_i_S_PNG}
%     \hspace*{-15mm}
     \includegraphics{K_sigma_i_S_PNG}
   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
\end{figure}

%Dans la figure~\ref{étiquette} page~\pageref{étiquette},  

%\bigskip


\begin{figure}[h!]
   \centering

\begin{tikzpicture}[->,>=stealth',shorten >=1.5pt,auto,node distance=1.8cm,
                    thick]
  \tikzstyle{every state}=[fill=none,draw=blue,text=black]

  \node[initial,state] (A)                            {$s_{\bar{a}i,0}$};
  \node[state]           (B) [below of=A]     {$s_{\bar{a}i,1}$};

  \node[state]           (C) [below of=B]        {$s_{\bar{a}i,k}$};

  \node[state]           (D) [below of=C]       {$s_{\bar{a}i,n-1}$};
  \node[state]           (E) [below of=D]       {$s_{\bar{a}i,n}$};

  \path (A) edge              node {} (B)
            (B) edge       node {} (C)
            (C) edge             node {} (D)
            (D) edge             node {} (E);

\end{tikzpicture}

   \caption{\label{AKSNegCex} Kripke Structure of counterexample $\sigma_i$, $K(\sigma_i)$}
\end{figure}


Therefore all properties that are satisfied won't be chosen to be integrated in the next step of refinement. At this stage, we already have a list of potential properties that will definitely eliminate the current counterexample $\sigma_i$ and might converge the abstract model towards a model sufficient to verify the global property $\phi$.

}
%\bigskip

\item {\emph{\underline{Step 2:}} \\

The property at the top of the list (not yet selected and excluding the properties which are satisfied by $K(\sigma_i)$) is selected to be integrated in the generation of $\widehat{M}_{i+1}$.
%\bigskip

}
\end{enumerate}

$\widehat{M}_{i+1}$ is model-checked and the refinement process is repeated until the model satisfies the global property or there is no property left to be integrated in next abstraction.