source: papers/FDL2012/abstraction_refinement.tex @ 87

Last change on this file since 87 was 82, checked in by cecile, 13 years ago

correction label AKS(cex)

File size: 10.0 KB
Line 
1
2
3\subsection{Properties of good refinement}
4When 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.
5In 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:
6
7%\medskip
8
9\begin{definition} An efficient \emph{refinement} verifies the following properties:
10\begin{enumerate}
11\item The new refinement is an over-approximation of the concrete model:
12$\widehat{M} \sqsubseteq \widehat{M}_{i+1}$.
13\item The new refinement is more concrete than the previous one:
14$\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$.
15\item The spurious counterexample in $\widehat{M}_i$ is  removed from
16$\widehat{M_{i+1}}$.
17\end{enumerate}
18\label{def:goodrefinement}
19\end{definition}
20Moreover, the refinement steps should be easy to compute and ensure a fast
21convergence by minimizing the number of iterations of the CEGAR loop.
22
23Refinements based on the concretization of selected abstract variables in
24$\widehat{M}_i$ ensure item 2. Concretization can be performed either in
25modifying the AKS of $\widehat{M}_i$, by changing some abstract value to
26concrete ones, but this approach is rude : in order to ensure item 1,
27concretization 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.
28%Another way to concretize some variables at selected instants is to compose
29%(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.
30
31We propose to compose the abstraction with another AKS to build a good refinement
32according to definition \ref{def:goodrefinement}.
33We have  several options. The most straightforward consists in building
34an 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 counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$.
35
36
37\subsection{Negation of the counterexample}
38
39The counterexample at a refinement step $i$, $\sigma$, is a path in the
40abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the
41counterexample given by the model-checker, the variable configuration in each
42state is Boolean. We name $\widehat{L_i}$ this new labeling.
43The spurious counterexample $\sigma$ is defined such that :
44\begin{definition}
45Let $\sigma$ be a \emph{spurious counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
46\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
47\rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
48\begin{itemize}
49\item All its variables are concrete: $\forall s_i$ and $\forall p\in
50\widehat{AP}_i$, $p$ is either true or false according to $\widehat{L_i}$.
51(not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
52\item  $\sigma$ is a counterexample in  $\widehat{M}_i$: $s_0\not\models \Phi$.
53\item  $\sigma$ is not a path of the concrete system $M$: $\exists k \in [1..n-1]$ such
54that $\forall j < k, (s_j,s_{j+1}) \in R$ and $(s_{k}, s_{k+1}) \not\in R$.
55\end{itemize}
56\end{definition}
57The construction of the AKS representing all executions except the one
58described by the spurious counter-example is done in two steps.
59
60\subsubsection{Step 1~:~Build the structure of the AKS.}
61
62
63\begin{definition}
64Let $\sigma$ be a spurious counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
65counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
66\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
67\widehat{F}_{\overline{\sigma}} \rangle$ is such that :
68\begin{itemize}
69\item $AP_{\overline{\sigma}} = {AP}_i$:
70The set of atomic propositions coincides with the one of $\sigma$
71
72\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i\in
73[0..n-2] \wedge s_i\in
74\sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \wedge s_i\in \sigma\}$
75
76\item $\widehat{L}_{\overline{\sigma}}$  with
77$L_{\overline{\sigma}}(s_i') = L_i(s_i), \forall i \in [0..n-2]$ and
78$L(s_T) = \{\top, \forall p \in AP_{\bar{\sigma}}\}$,
79$L_{\overline{\sigma}}(\bar{s_i})$ is explained in the next construction step.
80
81\item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$
82
83\item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in
84[0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup
85\{(s_i',s_{i+1}',\forall  i\in[0..n-3]\}$
86
87\item $\widehat{F}_{\overline{\sigma}} = \emptyset$
88\end{itemize}
89\end{definition}
90The labeling function fo $s_i'$ represents (concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
91configurations {\it but} the one of $s_i$. This last set may not be representable by
92the labeling function defined in def \ref{def-aks}. State labeling is treated
93in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}.
94%The size of this structure is linear with the size of the counter-example.
95
96\subsubsection{Step 2~:~Expand state configurations representing the negation of a concrete configuration.}
97%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)$.
98The set of configurations associated with a state $\bar{s_i}$ represents the
99negation 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.
100
101\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}\}\}$.
102
103To build the final AKS representing all sequences but spurious counter-example
104$\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by
105$k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$
106and assigns to each of them a label of $k$ variables $\{v_0, \ldots,
107v_{k-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1],
108v_l = \neg  {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each
109state $\bar{s_i^j}$ is connected to the same predecessor and successor states
110as state $\bar{s_i}$.
111
112This 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 counter-example {\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 counter-examples (here $a$, $b$ and $c$ represent concrete state configurations). At a given refinement step $i$, a particular counter example $\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 counter-example does not prevent from a new spurious counter-example 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 counter-example {\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 a priors know if at least one of these sequence is executable in the concrete model.
113
114From these considerations, we are interested in removing {\em sets of
115behaviors encompassing the spurious counter-example} but still guaranteeing an
116over-approximation of the set of tree-organized behaviors of the concrete
117model. The strengthening of the abstraction $\widehat{M}_i$ with the
118addition of AKS of already verified local CTL properties eliminates sets of
119behaviors and guarantees the over-approximation (property
120\ref{prop:concrete_compose}) but does not guarantee the elimination of the counter example. We present in the following section a strategy to select sets of CTL properties eliminating the spurious counter example.
121
122
123
124
125
126%\bigskip
127
128%\begin{definition}
129%\textbf{\emph{Spurious counterexample :}} \\
130%\\
131%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'}$.\\
132%
133%\smallskip
134%
135%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}.
136%
137%\end{definition}
138
139
140
141\subsection{Ordering of properties}
142
143\input{ordering_filter_properties}
Note: See TracBrowser for help on using the repository browser.