Changeset 70 for papers/FDL2012

Timestamp:

Mar 20, 2012, 11:56:30 AM (13 years ago)

Author:

ema

Message:

 

File:

• papers/FDL2012/abstraction_refinement.tex (modified) (1 diff)

papers/FDL2012/abstraction_refinement.tex

@@ -69 +69 @@
 \TODO{connexion des $s"_i^k$}
 
-This final AKS presents a number of states which is linear with the length of the counter-example and the number of atomic propositions.
-
 \TODO{Revoir notation def 3 pour f,t,top et introduire notation ${L}_{i}(s'_i)[v_l]$}
 
-Removing the spurious counter-example only has little chance to converge.
+This final AKS presents a number of states which is linear with product of the length of the counter-example and the number of atomic propositions. 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. 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 priori know if at least one of these sequence is executable in the concrete model.
+
+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.
+
+
+
+
 
 %\bigskip