Changeset 81 for papers/FDL2012/abstraction_refinement.tex
- Timestamp:
- Apr 4, 2012, 3:21:25 PM (13 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/abstraction_refinement.tex
r79 r81 9 9 \begin{definition} An efficient \emph{refinement} verifies the following properties: 10 10 \begin{enumerate} 11 \item The new refinement is an over-approximation of the concrete model: $\widehat{M}_{i+1} \sqsubseteq \widehat{M}$. 11 \item The new refinement is an over-approximation of the concrete model: 12 $\widehat{M} \sqsubseteq \widehat{M}_{i+1}$. 12 13 \item The new refinement is more concrete than the previous one: 13 $\widehat{M}_{i } \sqsubseteq \widehat{M}_{i+1}$.14 $\widehat{M}_{i+1} \sqsubseteq \widehat{M}_{i}$. 14 15 \item The spurious counterexample in $\widehat{M}_i$ is removed from 15 16 $\widehat{M_{i+1}}$. … … 17 18 \label{def:goodrefinement} 18 19 \end{definition} 19 20 20 Moreover, the refinement steps should be easy to compute and ensure a fast 21 21 convergence by minimizing the number of iterations of the CEGAR loop. 22 22 23 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. 24 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. 23 Refinements based on the concretization of selected abstract variables in 24 $\widehat{M}_i$ ensure item 2. Concretization can be performed either in 25 modifying the AKS of $\widehat{M}_i$, by changing some abstract value to 26 concrete ones, but this approach is rude : in order to ensure item 1, 27 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. 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. 25 30 26 Several proposals can be made. The most straightforward consists in building the 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$. 31 We propose to compose the abstraction with another AKS to build a good refinement 32 according to definition \ref{def:goodrefinement}. 33 We have several options. The most straightforward consists in building 34 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 counter example are determined, and then the corresponding AKS is synchronized with the one of $\widehat{M}_i$. 27 35 28 36 29 \subsection{ Refinement by negation of the counterexample}37 \subsection{Negation of the counterexample} 30 38 31 39 The counterexample at a refinement step $i$, $\sigma$, is a path in the 32 40 abstract model $\widehat{M}_i$ which dissatisfies $\Phi$. In the 33 41 counterexample given by the model-checker, the variable configuration in each 34 state is boolean. We name $\check{L_i}$ this new labeling.42 state is Boolean. We name $\widehat{L_i}$ this new labeling. 35 43 The spurious counterexample $\sigma$ is defined such that : 36 44 \begin{definition} 37 Let $\sigma$ be a \emph{ counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},45 Let $\sigma$ be a \emph{spurious counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i}, 38 46 \widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots 39 47 \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$. … … 47 55 \end{itemize} 48 56 \end{definition} 49 In the following we denote by 50 The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps. 51 \subsubsection{step 1 : Build the structure of the AKS.} 57 The construction of the AKS representing all executions except the one 58 described by the spurious counter-example is done in two steps. 59 60 \subsubsection{Step 1~:~Build the structure of the AKS.} 61 52 62 53 63 \begin{definition} 54 Let $\sigma$ be a counter-example of length $|\sigma| = n$, the \emph{ AKS of the64 Let $\sigma$ be a spurious counter-example of length $|\sigma| = n$, the \emph{ AKS of the 55 65 counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}}, 56 66 \widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, … … 59 69 \item $AP_{\overline{\sigma}} = {AP}_i$: 60 70 The set of atomic propositions coincides with the one of $\sigma$ 61 \item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i`in 71 72 \item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i\in 62 73 [0..n-2] \vee s_i\in 63 \sigma\}\cup \{\bar{s_{i}}|\forall i in [0..n-1] \vee s_i\in \sigma\}$ 64 \item $\widehat{L}_{\overline{\sigma}}$ is such that $s_i'$ represents the 65 (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all 66 configurations but the one of $s_i$. This last set may not be representable by 67 the labeling function defined in def \ref{def-aks}. State labeling is treated 68 in the second step. $s_t$ is a state where all atomic propositions are {\it unknown}. 74 \sigma\}\cup \{\bar{s_{i}}|\forall i \in [0..n-1] \vee 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_{\overline{\sigma}}(\bar{s_i}) = \bar{L_i(s_i)}, \forall i \in [0..n-1]$ 69 79 70 80 \item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$ 81 71 82 \item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in 72 83 [0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup … … 76 87 \end{itemize} 77 88 \end{definition} 78 The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels. 89 Note that in the labeling function represent (concrete) configuration of state $s_i$ and state $\bar{s_i}$ represents all 90 configurations but the one of $s_i$. This last set may not be representable by 91 the labeling function defined in def \ref{def-aks}. State labeling is treated 92 in the second step. $s_T$ is a state where all atomic propositions are {\it unknown}. 93 %The size of this structure is linear with the size of the counter-example. 79 94 80 \subsubsection{Step 2 : Expand state configurations representing the negation of a concrete configuration.} 81 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)$. 82 The set of configurations associated with a state $s"_i$ represents the negation of the one represented by ${L}_{\overline{\sigma}}(s'_i)$. This negation is not representable by the label of a single state but rather by a union of $\mid AP \mid$ labels. 95 \subsubsection{Step 2~:~Expand state configurations representing the negation of a concrete configuration.} 96 %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)$. 97 The set of configurations associated with a state $\bar{s_i}$ represents the 98 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. 83 99 84 \emph{Example}. Assume $AP = \{v_0,v_1,v_2\}$ and $\sigma = s_0 \rightarrow s_1 , \ldots$ and $\widehat{L}(s_0) = \{\mathbf{f},\mathbf{f},\mathbf{f}\}$ meaningthe 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}\}\}$.100 \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}\}\}$. 85 101 86 To build the final AKS representing all sequences but spurious counter-example $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $s"_i$ by $n = \mid AP_{\overline\sigma} \mid$ states $s"_i^k$ with $k \in [0..n-1]$ and assigns to each of them a label of $n$ variables $\{v_0, \ldots, v_{n-1}\}$ defined such that : ${L}(s"_i^k) = \{\forall l \in [0..k], v_l = \neg {L}_{i}(s'_i)[v_l], \forall l \in [k+1..n-1], v_l = \top\}$. each state $s"_i^k$ is connected to predecessor and successor states as state $s"_i$ was. 102 To build the final AKS representing all sequences but spurious counter-example 103 $\sigma$, one replaces in $AKS(\overline{\sigma})$ each state $\bar{s_i}$ by 104 $k = \mid AP_{\overline\sigma} \mid$ states $\bar{s_i^j}$ with $j\in [0..k-1]$ 105 and assigns to each of them a label of $n$ variables $\{v_0, \ldots, 106 v_{n-1}\}$ defined such that : ${L}(\bar{s_i^j} = \{\forall l \in [0..k-1], 107 v_l = \neg {L}_{i}(s_i)[v_l], \forall l \in [j+1..k-1], v_l = \top\}$. each 108 state $\bar{s_i^j}$ is connected to the same predecessor and successor states 109 as state $\bar{s_i}$. 87 110 88 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 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 prior iknow if at least one of these sequence is executable in the concrete model.111 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 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. 89 112 90 From these considerations, we are interested in removing {\em sets of behaviors encompassing the spurious counter-example} 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 adjunction of AKS of already verified local CTL properties eliminates sets of behaviors and guarantees the over-approximation 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. 113 From these considerations, we are interested in removing {\em sets of 114 behaviors encompassing the spurious counter-example} but still guaranteeing an 115 over-approximation of the set of tree-organized behaviors of the concrete 116 model. The strengthening of the abstraction $\widehat{M}_i$ with the 117 addition of AKS of already verified local CTL properties eliminates sets of 118 behaviors and guarantees the over-approximation (property 119 \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. 91 120 92 121
Note: See TracChangeset
for help on using the changeset viewer.