[hdrcouchot.git] / modelchecking.tex

\section{Rappels sur le langage PROMELA}
\label{sec:spin:promela}

Cette section  rappelle les éléments fondamentaux du langage PROMELA (Process Meta  Language).
On peut trouver davantage de détails dans~\cite{Hol03,Wei97}.




\begin{figure}[ht]
\begin{scriptsize}
\begin{lstlisting}
#define N 3
#define d_0 5

bool X [N]; bool Xp [N]; int mods [N];
typedef vals{bool v [N]};
vals Xd [N];  

typedef a_send{chan sent[N]=[d_0] of {bool}};
a_send channels [N];

chan unlock_elements_update=[1] of {bool};
chan sync_mutex=[1] of {bool};
\end{lstlisting}
\end{scriptsize}
\caption{Type declaration of the DDNs translation.}
\label{fig:arrayofchannels}
\end{figure}


Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
\texttt{short} et  \texttt{int}. Comme dans le langage C par exemple,
on peut declarer des tableaux à une dimension de taille constante 
ou des nouveaux types de données (introduites par le mot clef 
\verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux
dimension.

\begin{xpl}
Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des 
déclarations de variables qui serviront dans l'exemple jouet de ce chapitre. 
Il définit tout d'abord:
\begin{itemize}
\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le numbre
 $n$ d'éléments et le délais maximum $\delta_0$;
\item les deux tableaux  (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes; 
les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $X_{i+1}$
d'un systène dynamique discret 
(le décallage d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau);
Elles  memorisent les  valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour; 
il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $X$ à changé ou pas;
\item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'iteration 
en cours; cela correspond naturellement à l'ensemble des éléments $S^t$;
\item le type de données structurées \verb+vals+ et le tableau de tableaux 
 \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $X_{j+1}^{D^{t-1}_{i+1j+1}}$
 pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $X^{t}$).
\end{itemize}


Puisque le décallage d'un indices ne change pas fondamentalement 
le comportement de la version PROMELA par rapport au modèle initial
et pour des raisons de clareté, on utilisera par la suite la même 
lettre d'indice entre les deux niveaux (pour le modèle: $X_i$ et pour  PROMELA: 
\texttt{X[i]}). Cependant, ce décallage devra être conservé mémoire.

Une donnée de type \texttt{channel} permet le 
transfert de messages entre processus dans un ordre FIFO.
Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité 
(qui est constante), son nom et le type des messages qui sont stockés dans ce cannal.
Dans l'exemple précédent, on déclare successivement:
\begin{itemize}
\item un cannal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type
 \verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+
 éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $X_j$;
 Il permet donc de temporiser leur emploi par d'autres elements $i$.
\item les deux cannaux  \verb+unlock_elements_update+ et  \verb+sync_mutex+ contenant 
chacun un message booléen et utilisé ensuite comme des sémaphores.
\end{itemize}
\end{xpl}

%\subsection{PROMELA Processes} 
Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurence
au sein de systèmes. Un process est déclaréavec le mot-clef
\verb+proctype+  et est  instancié soit imédiatement (lorsque sa déclaration est préfixée 
 par le mot-clef  \verb+active+) ou bien au moment de l'exécution de l'instruction 
\texttt{run}.
Parmi tous les process,  \verb+init+ est le process  initial qui permet 
d'initialiser les variables, lancer d'autres processes\ldots


Les instructions d'affecatation sont interprétées usuellement.
Les cannaux sont cernés par des instructions particulières d'envoi et de
réception de messages. Pour un cannal  
\verb+ch+,  ces instruction sont respectivement notées
\verb+ch  !  m+ et \verb+ch  ?  m+.
L'instruction de réception consomme la valeur en tête du cannal \verb+ch+
et l'affecte à la variable \verb+m+ (pour peu que  \verb+ch+ soit initialisé et non vide).
De manière similaire,l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal
\verb+ch+ (pour peu que celui-ci soit initialisé et non rempli).
Dans les cas problématiques, canal non initialisé et vide pour une reception ou bien rempli pour un envoi,
le processus est blocké jusqu'à ce que les  conditions soient  remplies.

La structures de contrôle   \verb+if+   (resp.   \verb+do+)   définit un choix non déterministe 
 (resp.  une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle, 
si plus d'une des conditions est établie, l'ensemble des instructions correspondantes 
sera choisi aléatoirement puis exécuté.

Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init}, 
une boucle de taille $N$ initialise aléatoirement la variable  globale de type tableau \verb+Xp+.
Ceci permet par la suite de verifier si les itérations sont  convergentes pour n'importe  
quelle configuration initiale $X^{(0)}$.



Pour chaque  élément $i$, si les itérations sont asynchrones
\begin{itemize}
\item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+ 
puisque la matrice $S^0$ est égale à $(0)$,
\item puis, la valeur  de $i$ (représentée par  \verb+Xp[i]+) devrait être transmise 
  à $j$  s'il y a un arc de $i$ à   $j$ dans le graphe d'incidence. Dans ce cas,
  c'est la fonction  \verb+hasnext+ (non détaillée ici)  
  \JFC{la détailler}
  qui   memorise ce graphe
  en fixant à  \texttt{true} la variable \verb+is_succ+, naturellement et à 
  \texttt{false} dans le cas contraire. 
  Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+.
\end{itemize}

\begin{figure}[t]
 \begin{minipage}[h]{.52\linewidth}
\begin{scriptsize}
\begin{lstlisting}
init{
 int i=0; int j=0; bool is_succ=0;
 do
 ::i==N->break;
 ::i< N->{
   if
   ::Xp[i]=0;
   ::Xp[i]=1;
   fi;
   j=0;
   do
   ::j==N -> break;
   ::j< N -> Xd[j].v[i]=Xp[i]; j++;
   od;
   j=0;
   do
   ::j==N -> break;
   ::j< N -> {
     hasnext(i,j);
     if
     ::(i!=j && is_succ==1) -> 
     channels[i].sent[j] ! Xp[i];
     ::(i==j || is_succ==0) -> skip; 
     fi;  
     j++;}
   od;
   i++;}
 od;
 sync_mutex ! 1;
}
\end{lstlisting}
\end{scriptsize}
\caption{PROMELA init process.}\label{fig:spin:init} 
\end{minipage}\hfill
 \begin{minipage}[h]{.42\linewidth}
\begin{scriptsize}
\begin{lstlisting}
active proctype scheduler(){ 
 do
 ::sync_mutex ? 1 -> {
   int i=0; int j=0;
   do
   :: i==N -> break;
   :: i< N -> {
     if
     ::skip;
     ::mods[j]=i; j++;
     fi;
     i++;}
   od;
   ar_len=i; 
   unlock_elements_update ! 1;
   }
 od
}
\end{lstlisting}
\end{scriptsize}
\caption{Scheduler process for common pseudo-periodic strategy.
 \label{fig:scheduler}}
\end{minipage}
\end{figure}



\section{Du système booléen au modèle PROMELA}
\label{sec:spin:translation}
Les éléments principaux des itérations asynchrones rappelées à l'équation 
(\ref{eq:async}) sont  la stratégie, la  fonctions et la gestion des délais.
Dans cette section, nous présentons successivement comment chacune de 
ces notions est traduite vers un modèle PROMELA.


\subsection{La stratégie}\label{sub:spin:strat}
Regardons comment une stratégie pseudo-périodique peut être représentée en PROMELA.
Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler}) 
est itérativement appelé pour construire chaque $S^t$ représentant 
les éléments possiblement mis à jour à l'itération $t$.

Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore
\verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis
aléatoirement  (grâce à  $n$ choix successifs) et sont mémorisés dans le tableau
\verb+mods+,  dont la taille est  \verb+ar_len+.   
Dans la séquence d'éxécution, le choix d'un élément mis à jour est directement
suivi par des mis àjour: ceci est réalisé grace à la modification de la valeur du sémaphore
 \verb+unlock_elements_updates+.

\subsection{Applying the function $F$}\label{sub:spin:update}
Updating a set $S^t=\{s_1,\ldots, s_m\}$  of elements that occur in the strategy
$(S^t)^{t \in \Nats}$ is implemented by the \verb+update_elems+ process given
in~\ref{fig:proc}.  This  active  process waits  until  it is  unlocked by  the
\verb+scheduler+  process through  the  semaphore \verb+unlock_elements_update+.
The implementation is then fivefold:

\begin{enumerate}
\item it starts with updating the variable \texttt{X} with the values of \texttt{Xp}
  thanks to the \texttt{update\_X} function (not detailed here);
  %%we recall that the variable \texttt{X} is only defined as 
\item it stores in \texttt{Xd} the current available values of the elements thanks
  to the function \texttt{fetch\_values} (see \Sec{sub:spin:vt});
\item  a loop  over the  number \texttt{ar\_len}  of elements  that have  to evolve
  iteratively updates the  value of $j$ (through the  function call \texttt{F(j)})
  provided   this  has   to   evolve,  \textit{i.e.},   it   is  referenced   by
  \texttt{mods[count]}; source code  of \texttt{F} is given in~\ref{fig:p} and is a
  direct translation of the map $F$;
\item the new components values in  \texttt{Xp} are symbolically sent to the other
  components requiring them % for future access
  thanks to the \texttt{diffuse\_values(Xp)} function (see \Sec{sub:spin:vt});
\item finally, this process informs the scheduler about the end of the task 
  (through the semaphore \texttt{sync\_mutex}).
\end{enumerate}


\begin{figure}[t]
  \begin{minipage}[h]{.475\linewidth}
\begin{scriptsize}
\begin{lstlisting}
active proctype update_elems(){
 do
 ::unlock_elements_update ? 1 ->
   {
    atomic{
     bool is_succ=0;
     update_X();
     fetch_values();
     int count = 0;
     int j = 0;
     do
     ::count == ar_len -> break;
     ::count < ar_len ->
       j = mods[count];     
       F(j);
       count++;
     od;
     diffuse_values(Xp);
     sync_mutex ! 1
    }
   }
 od
}
\end{lstlisting}
\end{scriptsize}
\caption{Updatings of the elements.}\label{fig:proc}
  \end{minipage}\hfill%
%\end{figure}
%\begin{figure}
  \begin{minipage}[h]{.45\linewidth}
\begin{scriptsize}
\begin{lstlisting}
inline F(){
 if
 ::j==0 -> Xp[0] = 
      (Xs[j].v[0] & !Xs[j].v[1]) 
     |(Xs[j].v[2])
 ::j==1 -> Xp[1] =  Xs[j].v[0] 
                 | !Xs[j].v[2]
 ::j==2 -> Xp[2] =  Xs[j].v[1] 
                 &  Xs[j].v[2]
 fi
}
\end{lstlisting}
\end{scriptsize}
\caption{Application of  function $F$.}\label{fig:p}
  \end{minipage}
\end{figure}

% \subsection{Modifying  Values of one  Element}

% Each element $i$ may modify its value through the coresponding 
% active process \verb+pi+. 
% In Fig.~\ref{fig:p4} that gives the translation of 
% modifying the element $4$, the process is waiting until it is unlocked
% and then it computes the new value of $X_4$, represented by $X'_4$ 
% and memorized as \verb+Xp[4]+. 


% \begin{ProofCr}

% First of all, the second hypothesis of the previous proof is established.

% In this part, we prove that for any time $t$,  
 
% The proof is achieved under the hypothesis that at current time $t$, 

% For $j$ in $J^t$, variables 
% \verb+v0+, \ldots \verb+vn-1+ are respectively 
% $X_0^{S_{j0}^t},\ldots, X_{n-1}^{S_{jn-1}^t}$.
% Since \verb+F+ is the direct translation of $F$, rest of the proof is obvious. 
 
  
% \end{ProofCr}

\subsection{Delays Handling}\label{sub:spin:vt}
This  section shows  how  delays are  translated  into PROMELA  through the  two
functions   \verb+fetch_values+  and   \verb+diffuse_values+,   given  in~\ref{fig:val} and~\ref{fig:broadcast}, that  respectively store and transmit the
element values.

\begin{figure}[t]
  \begin{minipage}[h]{.475\linewidth}
\begin{scriptsize}
\begin{lstlisting}
inline fetch_values(){
 int countv = 0;
 do
 :: countv == ar_len -> break ;
 :: countv < ar_len ->
    j = mods[countv];
    i = 0;       
    do
    :: (i == N) -> break;
    :: (i < N && i == j) -> {
        Xd[j].v[i] = Xp[i] ;
        i++ }   
    :: (i < N && i != j) -> {
        hasnext(i,j);
        if
        :: skip
        :: is_succ==1 &&
    nempty(channels[i].sent[j]) ->
            channels[i].sent[j] ?
                        Xd[j].v[i];
        fi; 
        i++ }
    od;
    countv++
 od
}
\end{lstlisting}
\end{scriptsize}
\caption{Fetching of the elements values\label{fig:val}}
  \end{minipage}\hfill%
  \begin{minipage}[h]{.475\linewidth}
\begin{scriptsize}
\begin{lstlisting}
inline diffuse_values(values){   
 int countb=0;
 do
 :: countb == ar_len -> break ;
 :: countb < ar_len ->
    j = mods[countb];
    i = 0 ;
    do
    :: (i == N) -> break;
    :: (i < N && i == j) -> i++;   
    :: (i < N && i != j) -> {
        hasnext(j,i);
        if
        :: skip
        :: is_succ==1 && 
     nfull(channels[j].sent[i]) ->
            channels[j].sent[i] ! 
                         values[j];
        fi;
        i++ }
    od;
    countb++
 od
}       
\end{lstlisting}
\end{scriptsize}
\caption{Diffusion of the elements values}\label{fig:broadcast}
  \end{minipage}
\end{figure}

The former potentially updates the  array \verb+Xd+ needed by elements that have
to be  modified.  For  each element in  \verb+mods+, identified by  the variable
$j$, the  function retrieves the values  of the other elements  (labeled by $i$)
whose $j$ depends on.  There are two cases:
\begin{itemize}
\item since $i$  knows its last value (\textit{i.e.},  $D^t_{ii}$ is always $t$)
  \verb+Xd[i].v[i]+ is then \verb+Xp[i]+.
\item otherwise, there are two sub-cases which potentially update the value that
  $j$ knows about $i$ (that may be chosen in a random way):
  \begin{itemize}
  \item  from the viewpoint of $j$  the value  of  $i$ may  not change  (the
    \verb+skip+  statement) or  is not  relevant; this  latter case  arises when
    there is no edge from $i$ to $j$ in the incidence graph, \textit{i.e.}, when
    the value  of \verb+is_succ+ that  is computed by \verb+hasnext(i,j)+  is 0;
    then the value of \verb+Xd[j].v[i]+ is not modified;
  \item otherwise,  \verb+Xd[j].v[i]+ is assigned  with the value stored  in the
    channel  \verb+channels[i].sent[j]+  (provided   this  one  is  not  empty).
    Element  values  are  added  into  this channel  during  the  \verb+diffuse_values+
    function as follows.
  \end{itemize}
\end{itemize}

The \verb+diffuse_values+  function aims  at storing the  values of $X$  represented by
\verb+Xp+ in the  \verb+channels+.  It allows the SPIN  model-checker to execute
the PROMELA model as if it allowed delays between processes.
% as if computation mode were asynchronous. 
%For that reason, when an iteration has to synchronize the elements $i$ and 
%$j$  (\textit{i.e.} when \verb+sync[j] == sync[i]+ is true), 
% no delay emulation is performed.
%In the asynchronous mode, 
There are two cases concerning the value of $X_{j}$:
\begin{itemize}
\item either it is left out to allow $i$ not to take into account all the values
  of  $j$; this case  occurs either  through the  \verb+skip+ statement  or when
  there is no edge from $j$ to $i$ in the incidence graph;
\item or it is stored  in the channel \verb+channels[j].sent[i]+ (provided it is
  not full).
\end{itemize}

Introducing     non-determinism      both     in     \verb+fetch_values+     and
\verb+diffuse_values+   functions  is   necessary  in   our  context.    If  the
non-determinism would be used only  in \verb+fetch_values+, then it would not be
possible  for instance  to retrieve  the value  $X_i^{(t)}$ without  taking into
account the value  $X_i^{(t-1)}$.  On the other hand,  if the non-determinism is
only used  in \verb+diffuse_values+, then each  time a value is  pushed into the
channel, this  value is  immediately consumed, which  contradicts the  notion of
delays.

\subsection{Discussion}
A  coarse approach  could consist  in providing  one process  for  each element.
However, the  distance with  the mathematical model  given in  \Equ{eq:async} of
such a translation would be larger  than the method presented along these lines.
It induces  that it would be harder  to prove the soundness  and completeness of
such a translation.   For that reason we have developed a  PROMELA model that is
as close as possible to the mathematical one.

Notice furthermore that PROMELA is an  imperative language which
often results in generating  intermediate  states 
(to  execute  a matrix assignment  for
instance). 
The  use  of  the  \verb+atomic+  keyword  allows  the  grouping  of
instructions, making the PROMELA code and the DDN as closed as possible.

\subsection{Universal Convergence Property}
We are left to show how to formalize into the SPIN model-checker that iterations
of a DDN with $n$ elements are universally convergent.  We first recall that the
variables \verb+X+  and \verb+Xp+ respectively  contain the value of  $X$ before
and after  an update.  Then,  by applying a non-deterministic  initialization of
\verb+Xp+  and  applying  a   pseudo-periodic  strategy,  it  is  necessary  and
sufficient to establish the following Linear Temporal Logic (LTL) formula:
\begin{equation}
\diamond  (\Box  \verb+Xp+ = \verb+X+)
\label{eq:ltl:conv}
\end{equation}
where $\diamond$  and $\Box$ have the usual  meaning \textit{i.e.}, respectively
{\em eventually} and {\em always} in  the subsequent path.  It is worth noticing
that this property only ensures the stabilization of the system, but it does not
provide any information  over the way the system  converges. In particular, some
indeterminism  may still  be present  under the  form of  multiple  fixed points
accessible from some initial states.



\section{Proof of Translation Correctness}\label{sec:spin:proof}
\JFC{Déplacer les preuves en annexes}

This  section  establishes  the  soundness  and  completeness  of  the  approach
(Theorems~\ref{Theo:sound}  and ~\ref{Theo:completeness}). Technical  lemmas are
first shown to ease the proof of the two theorems.
   

% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock}
%   Let $\phi$ be a DDN model and $\psi$ be its translation.  There is no deadlock
%   in any execution of $\psi$.
% \end{Lemma}
% \begin{Proof}
%   In current  translation, deadlocks of  PROMELA may only be  introduced through
%   sending  or  receiving messages  in  channels.   Sending  (resp. receiving)  a
%   message in the  \verb+diffuse_values+ (resp.  \verb+fetch_values+) function is
%   executed  only if  the  channel is  not full  (resp.  is not  empty).  In  the
%   \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value
%   in     any     semaphore     channel    (\verb+unlock_elements_update+     and
%   \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the
%   way.
% \end{Proof}


\begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
  Let $\phi$  be a  DDN with strategy  $(S^t)^{t \in  \Nats}$ and $\psi$  be its
  translation.  There exists an execution of $\psi$ with weak fairness s.t.  the
  scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$.
\end{lemma}
\begin{Proof}
  The proof is direct  for $t=0$. Let us suppose it is  established until $t$ is
  some $t_0$.  Let  us consider pseudo-periodic strategies.  Thanks  to the weak
  fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at
  iteration $t$.
\end{Proof}

In     what     follows,     let     $Xd^t_{ji}$     be     the     value     of
\verb+Xd[+$j$\verb+].v[+$i$\verb+]+  after  the   $t^{\text{th}}$  call  to  the
function  \verb+fetch_values+.  Furthermore,  let $Y^k_{ij}$  be the  element at
index  $k$  in  the  channel  \verb+channels[i].sent[j]+ of  size  $m$,  $m  \le
\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are  respectively the head and the tail
of the  channel.  Secondly, let $(M_{ij}^t)^{t \in  \{1, 1.5, 2, 2.5,\ldots\}}$ be a
sequence such  that $M_{ij}^t$ is the  partial function that  associates to each
$k$, $0 \le k \le  m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering
into the \verb+update_elems+ at iteration $t$ where
% \begin{itemize}
% \item
 $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+
  at index $k$,
%\item 
$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and
%\item 
$c^k_{ij}$ is the  first date at which the value is  available on $j$. So,
  the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$.
%\end{itemize}
$M_{ij}^t$ has the following signature:
\begin{equation*}
\begin{array}{rrcl}
M_{ij}^t: & 
\{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\
& k  \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}).
\end{array}  
\end{equation*}

Intuitively,  $M_{ij}^t$  is  the  memory  of  \verb+channels[i].sent[j]+  while
starting the iteration $t$.  Notice that the domain of any $M_{ij}^1$ is $\{0\}$
and   $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    indeed,   the   \verb+init+   process
initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+.

Let us  show how  to make the  indeterminism inside the  two functions\linebreak
\verb+fetch_values+  and  \verb+diffuse_values+  compliant with  \Equ{eq:async}.
The  function   $M_{ij}^{t+1}$  is  obtained   by  the  successive   updates  of
$M_{ij}^{t}$  through   the  two  functions\linebreak   \verb+fetch_values+  and
\verb+diffuse_values+.   Abusively,   let  $M_{ij}^{t+1/2}$  be   the  value  of
$M_{ij}^{t}$ after the former function during iteration $t$.

In  what follows, we  consider elements  $i$ and  $j$ both  in $\llbracket  1, n
\rrbracket$   that  are   updated.   At   iteration   $t$,  $t   \geq  1$,   let
$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of
\verb+fetch_values+.   If $t$  is  equal  to $c^0_{ij}+1$  then  we execute  the
instruction    that   assigns    $Y^0_{ij}$   (\textit{i.e.},     the   head    value   of
\verb+channels[i].sent[j]+)  to   $Xd_{ji}^t$.   In  that   case,  the  function
$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each
$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$.
Otherwise (\textit{i.e.}, when  $t < c^0_{ij}+1$ or when  the domain of $M_{ij}$
is  empty)   the  \verb+skip+  statement  is  executed   and  $M_{ij}^{t+1/2}  =
M_{ij}^{t}$.

In the function \verb+diffuse_values+, if  there exists some $\tau$, $\tau\ge t$
such that \mbox{$D^{\tau}_{ji} = t$}, let  $c_{ij}$ be defined by $ \min\{l \mid
D^{l}_{ji} =  t \} $.  In  that case, we  execute the instruction that  adds the
value   \verb+Xp[i]+   to  the   tail   of  \verb+channels[i].sent[j]+.    Then,
$M_{ij}^{t+1}$ is defined  as an extension of $M_{ij}^{t+1/2}$  in $m$ such that
$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$.  Otherwise (\textit{i.e.}, when $\forall l
\, .  \, l \ge t  \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+
statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.


\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution}
  For any sequences $(S^t)^{t  \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for
  any map $F$ there exists a SPIN  execution such that for any iteration $t$, $t
  \ge  1$, for  any $i$ and $j$ in  $\llbracket 1, n \rrbracket$  we  have the
  following properties:
   
\noindent If the domain of $M_{ij}^t$ is not empty, then
\begin{equation}
  \left\{
    \begin{array}{rcl}
      M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
      \textrm{if $t \geq 2$ then }M_{ij}^t(0) & = &
      \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
      c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
    \end{array}
  \right.
  \label{eq:Mij0}
\end{equation}
\noindent Secondly we have:
\begin{equation}
  \forall t'\, .\,   1 \le t' \le t  \Rightarrow   Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
  \label{eq:correct_retrieve}
\end{equation}
\noindent Thirdly, for any $k\in S^t$.  Then, the value of the computed variable
\verb+Xp[k]+  at  the  end  of  the  \verb+update_elems+  process  is  equal  to
$X_k^{t}$          \textit{i.e.},          $F_{k}\left(         X_1^{D_{k\,1}^{t-1}},\ldots,
  X_{n}^{D_{k\,{n}}^{t-1}}\right)$ at the end of the $t^{\text{th}}$ iteration.
\end{lemma}
\begin{Proof}
The proof is done by induction on the number of iterations.

\paragraph{Initial case:}

For the first  item, by definition of $M_{ij}^t$, we  have $M_{ij}^1(0) = \left(
  \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}},
  0,0 \right)$.

Next, the first call to  the function \verb+fetch_value+ either assigns the head
of   \verb+channels[i].sent[j]+  to   \verb+Xd[j].v[i]+  or   does   not  modify
\verb+Xd[j].v[i]+.  Thanks to  the \verb+init+ process, both cases  are equal to
\verb+Xp[i]+,  \textit{i.e.}, $X_i^0$.  The  equation (\ref{eq:correct_retrieve})  is then
established.


For  the last  item, let  $k$, $0  \le  k \le  n-1$.  At  the end  of the  first
execution\linebreak   of   the  \verb+update_elems+   process,   the  value   of
\verb+Xp[k]+       is\linebreak       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.  Thus,  by definition of $Xd$,  it is equal
to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$.  Thanks to \Equ{eq:correct_retrieve},
we can conclude the proof.



\paragraph{Inductive case:}

Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.

First,  if domain  of definition  of the  function $M_{ij}^l$  is not  empty, by
induction  hypothesis $M_{ij}^{l}(0)$  is  $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.

At iteration $l$, if  $l < c + 1$ then the  \verb+skip+ statement is executed in
the   \verb+fetch_values+  function.   Thus,   $M_{ij}^{l+1}(0)$  is   equal  to
$M_{ij}^{l}(0)$.  Since $c > l-1$  then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
is $\min\{k  | D_{ji}^k  > D_{ji}^{l-1} \}$.  Obviously, this implies  also that
$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.

We now consider that at iteration $l$, $l$ is $c + 1$.  In other words, $M_{ij}$
is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$:
\begin{itemize}
\item  if $\dom(M_{ij}^{l})=\{0\}$  and $\forall  k\,  . \,  k\ge l  \Rightarrow
  D^{k}_{ji} \neq l$  is established then $\dom(M_{ij}^{l+1})$ is  empty and the
  first item of the lemma  is established; 
\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists  k\, . \, k\ge l \land D^{k}_{ji}
  = l$  is established then $M_{ij}^{l+1}(0)$  is $(\verb+Xp[i]+,l,c_{ij})$ that
  is  added  in  the  \verb+diffuse_values+ function  s.t.\linebreak  $c_{ij}  =
  \min\{k  \mid  D^{k}_{ji}  = l  \}  $.   Let  us  prove  that we  can  express
  $M_{ij}^{l+1}(0)$  as  $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$  where
  $c'$ is  $\min\{k |  D_{ji}^k > D_{ji}^{l-1}  \}$.  First,  it is not  hard to
  establish that  $D_{ji}^{c_{ij}}= l \geq  D_{ji}^{l} > D_{ji}^{l-1}$  and thus
  $c_{ij}  \geq   c'$.   Next,  since   $\dom(M_{ij}^{l})=\{0\}$,  then  between
  iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
  not updated $M_{ij}$.  Formally we have
$$
\forall t,k  \, .\, D_{ji}^c <  t < l \land  k \geq t  \Rightarrow D_{ji}^k \neq
t.$$

Particularly, $D_{ji}^{c'} \not  \in \{D_{ji}^{c}+1,\ldots,l-1\}$.  We can apply
the     third    item     of    the     induction    hypothesis     to    deduce
$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude.

\item  if   $\{0,1\}  \subseteq  \dom(M_{ij}^{l})$   then  $M_{ij}^{l+1}(0)$  is
  $M_{ij}^{l}(1)$.   Let  $M_{ij}^{l}(1)=  \left(\verb+Xp[i]+, a_{ij}  ,  c_{ij}
  \right)$.   By  construction $a_{ij}$  is  $\min\{t'  |  t' >  D_{ji}^c  \land
  (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k |
  D_{ji}^k = a_{ij}\}$.  Let us show  $c_{ij}$ is equal to $\min\{k | D_{ji}^k >
  D_{ji}^{l-1} \}$ further  referred as $c'$.  First we  have $D_{ji}^{c_{ij}} =
  a_{ij} >  D_{ji}^c$. Since $c$  by definition is  greater or equal to  $l-1$ ,
  then $D_{ji}^{c_{ij}}>  D_{ji}^{l-1}$ and then $c_{ij} \geq  c'$.  Next, since
  $c$ is  $l-1$, $c'$ is $\min\{k |  D_{ji}^k > D_{ji}^{c} \}$  and then $a_{ij}
  \leq  D_{ji}^{c'}$. Thus,  $c_{ij} \leq  c'$  and we  can conclude  as in  the
  previous part.
\end{itemize}


The case where  the domain $\dom(M^l_{ij})$ is empty but  the formula $\exists k
\, .\, k \geq  l \land D_{ji}^k = l$ is established  is equivalent to the second
case given above and then is omitted.


Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}).  At iteration
$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.  Two cases
have to be  considered depending on whether $D_{ji}^{l}$  and $D_{ji}^{l-1}$ are
equal or not.
\begin{itemize}
\item If  $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'}  > D_{ji}^{l-1}$, then
  $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$  is distinct from $l$. Thus, the SPIN
  execution detailed  above does not  modify $Xd_{ji}^{l+1}$.  It is  obvious to
  establish   that   $Xd_{ji}^{l+1}  =   Xd_{ji}^{l}   =  X_i^{D_{ji}^{l-1}}   =
  X_i^{D_{ji}^{l}}$.
\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$.
  According     to     \Equ{eq:Mij0}     we     have    proved,     we     have
  $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$.   Then  the SPIN  execution
  detailed above  assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$,  which ends the
  proof of (\ref{eq:correct_retrieve}).
\end{itemize}

We are left to prove the induction of  the third part of the lemma.  Let $k$, $k
\in S^{l+1}$. % and $\verb+k'+ = k-1$.
At the  end of the first  execution of the \verb+update_elems+  process, we have
$\verb+Xp[+k\verb+]+=                                   F(\verb+Xd[+k\verb+][0]+,
\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.  By  definition of $Xd$,  it is equal
to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
\Equ{eq:correct_retrieve} we have proved, we can conclude the proof.
\end{Proof}


\begin{lemma}
  Bounding the size of channels  to $\textit{max} = \delta_0$ is sufficient when
  simulating a DDN where delays are bounded by $\delta_0$.
\end{lemma}

\begin{Proof}
  For  any $i$,  $j$, at  each  iteration $t+1$,  thanks to  bounded delays  (by
  $\delta_0$),  element $i$  has to  know at  worst $\delta_0$  values  that are
  $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$.  They  can be stored into any channel
  of size $\delta_0$.
\end{Proof}


\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound}
  Let $\phi$ be  a DDN model and $\psi$ be its  translation.  If $\psi$ verifies
  the  LTL  property  (\ref{eq:ltl:conv})  under weak  fairness  property,  then
  iterations of $\phi$ are universally convergent.
\end{theorem}
\begin{Proof}
%   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
%   verification  is achieved  under  weak fairness  property.  Instructions  that
%   write or read into \verb+channels[j].sent[i]+ are continuously enabled leading
%   to  convenient  available  dates  $D_{ji}$.   It is  then  easy  to  construct
%   corresponding iterations of the DDN that are convergent.
% \ANNOT{quel sens donnes-tu a \emph{convenient} ici ?}

  Let us show the contraposition of the theorem.  The previous lemmas have shown
  that for any  sequence of iterations of the DDN, there  exists an execution of
  the PROMELA  model that  simulates them.   If some iterations  of the  DDN are
  divergent, then  they prevent  the PROMELA model  from stabilizing,  \textit{i.e.},  not
  verifying the LTL property (\ref{eq:ltl:conv}).
\end{Proof}


% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
% Let $\phi$ be a DDN model where strategy, $X^(0)$ 
% are only constrained to be pseudo-periodic and
% in $E$ respectively.
% Let $\psi$ be its translation.
% If all the executions of $\psi$ converge, 
% then  iterations of $\phi$ are universally convergent.
% \end{Corol}



\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness}
  Let $\phi$ be a  DDN model and $\psi$ be its translation.   If $\psi$ does not
  verify the LTL property  (\ref{eq:ltl:conv}) under weak fairness property then
  the iterations of $\phi$ are divergent.
\end{theorem}
\begin{Proof}
  For models $\psi$  that do not verify the  LTL property (\ref{eq:ltl:conv}) it
  is easy  to construct corresponding iterations  of the DDN,  whose strategy is
  pseudo-periodic since weak fairness property is taken into account.

%   i.e. iterations that  are divergent.   Executions are
%   performed under weak  fairness property; we then detail  what are continuously
%   enabled:
% \begin{itemize}
% \item if the strategy is not  defined as periodic, elements $0$, \ldots, $n$ are
%   infinitely often updated leading to pseudo-periodic strategy;
% \item  instructions  that  write  or read  into  \verb+channels[j].sent[i]+  are
%   continuously enabled leading to convenient available dates $D_{ji}$.
% \end{itemize}
% The simulated DDN does not stabilize and its iterations are divergent.
 \end{Proof}



\section{Practical Issues}
\label{sec:spin:practical}
This  section  first  gives  some  notes about  complexity  and  later  presents
experiments.
%\subsection{Complexity Analysis}
%\label{sub:spin:complexity}
\begin{theorem}[Number of states]
  Let $\phi$ be a DDN model with  $n$ elements, $m$ edges in the incidence graph
  and $\psi$ be  its translation into PROMELA.  The  number of configurations of
  the $\psi$ SPIN execution is bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
\end{theorem}
\begin{Proof}
  A configuration is a valuation  of global variables. Their number only depends
  on those that are not constant.

  The  variables  \verb+Xp+ \verb+X+  lead  to  $2^{2n}$  states.  The  variable
  \verb+Xs+ leads to $2^{n^2}$ states.  Each channel of \verb+array_of_channels+
  may  yield $1+2^1+\ldots+2^{\delta_0}=  2^{\delta_0+1}-1$  states.  Since  the
  number of  edges in  the incidence  graph is $m$,  there are  $m$ non-constant
  channels,  leading  to  approximately $2^{m\times(\delta_0+1)}$  states.   The
  number of configurations is then bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
  Notice that  this bound is tractable  by SPIN for  small values of $n$, 
  $m$ and $\delta_0$.
\end{Proof}



The  method detailed along  the line  of this  article has  been applied  on the
running example to formally prove its universally convergence.

First  of all,  SPIN only  considers  weak fairness  property between  processes
whereas  above  proofs need  such  a  behavior to  be  established  each time  a
non-deterministic choice is done.


A first attempt has consisted in building the following formula
each time an undeterministic choice between $k$ elements 
respectively labeled $l1$, \ldots $lk$ occurs:  
$$
[] <> (l == l0) \Rightarrow 
(([] <> (l== l1)) \land  \ldots \land ([] <> (l == lk)))
$$
where label $l0$ denotes the line before the choice.
This formula exactly translates the fairness property.
The negation of such a LTL formula may then be efficiently translated  
into a Büchi automata  with the tool ltl2ba~\cite{GO01}.
However due to an explosion of the size of the product 
between this automata and the automata issued from the PROMELA program 
SPIN did not success to verify whether the property is established or not. 

This problem has been practically tackled by leaving spin generating all the (not necessarily fair) computations and verifying convergence property on them.
We are then left to interpret its output with two issues.
If property is established for all the computations, 
it is particularly established for fair ones and iterations are convergent. 
In the opposite case, when facing to a counter example, an analysis of the SPIN 
output is achieved. 
\begin{xpl}
Experiments have shown that all the iterations of the running example are 
convergent for a delay equal to 1 in less than 10 min.
The example presented in~\cite{abcvs05} with five elements taking boolean 
values has been verified with method presented in this article.   
Immediately, SPIN computes a counter example, that unfortunately does not
fulfill fairness properties. Fair counter example is obtained
after few minutes.
All the experimentation have been realized in a classic desktop computer.
\end{xpl}





%However preliminary experiments have shown the interest of the approach.  



% The method detailed along the line of this article has been 
% applied on some examples to formally prove their convergence
% (Fig.~\ref{fig:async:exp}).
% In these experiments, Delays are supposed to be bounded by $\delta_0$ set to 10.
% In these arrays, 
% $P$ is true ($\top$) provided the  uniform convergence property is established, false ($\bot$) otherwise,  
% $M$ is the amount of memory usage (in MB) and 
% $T$ is the time needed on a Intel Centrino Dual Core 2 Duo @1.8GHz  with 2GB of memory, both  
% to establish or refute the property.

% RE is the running example of this article, 
% AC2D is a cellular automata with 9 elements taking boolean values
% according their four neighbors 
% and BM99 is has been proposed in~\cite{BM99} and consists of 10 process
% modifying their boolean values, but with many connected connection graph. 





% \begin{figure}
% \begin{center}
% \scriptsize
% \begin{tabular}{|*{13}{c|}}
% \cline{2-13}
% \multicolumn{1}{c|}{ }
% &\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
% \cline{2-13}
% \multicolumn{1}{c|}{ }
% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
% \cline{2-13}
% \multicolumn{1}{c|}{ }
% &P & M & T &
% P & M & T &
% P & M & T&
% P & M & T \\
% \hline %cline{2-13}
% Running Example & 
% $\top$ & 409 & 1m11s&
% $\bot$ & 370 & 0.54 &
% $\bot$ & 374 & 7.7s&
% $\bot$ & 370 & 0.51s \\
% \hline %\cline{2-13}
% AC2D 
% &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
% &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
% &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
% &$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
% \hline %\cline{2-13}
% BM99 
% &$\top$ &  &   %BM99_mixed_para.spin 
% &$\top$ &  &    % RC07_async_mixed_all.spin
% &$\bot$ &  &    % RC07_async.spin
% &$\bot$ &  &   \\ % RC07_async_all.spin 
% \hline %\cline{2-13}
% \end{tabular}
% \end{center}
% \caption{Experimentations with Asynchronous Iterations}\label{fig:async:exp}
% \end{figure} 



% The example~\cite{RC07} deals with a network composed of two genes taking their 
% values into $\{0,1,2\}$. Since parallel iterations is already diverging, 
% the same behavior is observed for all other modes.
% The Figure~\ref{fig:RC07CE} gives the trace leading to convergence property 
% violation output by SPIN.
% It corresponds to peridic strategy that repeats $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ and starts with $X=(0,0)$.
   
  
% In the example extracted from~\cite{BM99},
% we have 10 processors computing a binary value.
% Due to the huge number of  dependencies between these calculus, 
% $\delta_0$ is reduced to 1. It nevertheless leads to about $2^{100}$ 
% configurations in asynchronous iterations.

% Let us focus on checking universal convergence of asynchronous iterations 
% of example~\cite{BCVC10:ir}. 
% With a $\delta_0$ set to 5, SPIN generates an out of memory error.  
% However, it succeed to prove that the property is not established even
% with $\delta_0$ set to 1 which is then sufficient.


% \begin{figure}
% \begin{center}
% \begin{tiny}
% \begin{tabular}{|*{7}{c|}}
% \cline{2-7}
% \multicolumn{1}{c|}{ }
% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
% \cline{2-7}
% \multicolumn{1}{c|}{ }& 
% P & M & T&
% P & M & T \\
% \hline %\cline{2-7}
% Running  &
% $\top$ & 2.7 & 0.01s & 
% $\bot$ & 369.371 & 0.509s \\ 
% \hline %\cline{2-7}
% \cite{RC07} example &
% $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
% $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
% \hline
% \cite{BM99} example &
% $\top$ & 36.7 & 12s & % BM99_sync_para.spin
% $\top$ &  &  \\ % BM99_sync_chao.spin
% \hline
% \end{tabular}
% \end{tiny}
% \end{center}
% \caption{Experimentations with Synchronous Iterations}\label{fig:sync:exp}
% \end{figure} 






% \begin{tabular}{|*{}{c|}}
% % \hline 
% % e \\
% % 
% \hline
% & \multicolumn{6}{|c|}{Synchronous} & \multicolumn{12}{|c|}{Asynchronous}\\
% \cline{8-19}
% Delay &  \multicolumn{6}{|c|}{ }
% & \multicolumn{6}{|c|}
% {Only Bounded}
% & \multicolumn{6}{|c|}
% {Bounded+Mixed Mode}\\
% Strategy&
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\


% \end{tabular}

 
\section{Conclusion and Future Work}
\label{sec:spin:concl}
Stochastic based prototypes have been implemented to generate both 
strategies and delays for asynchronous iterations in first in~\cite{BM99,BCV02}.
However, since these research softwares are not exhaustive, they really give an 
formal answer when they found a counterexample. When facing convergence, they only convince 
the user about this behavior  without exhibiting a proof. 
 
As far as we know, no implemented formal method tackles the problem of
proving asynchronous iterations convergence. 
In the theoretical work~\cite{Cha06} Chandrasekaran shows that asynchronous iterations
are convergent iff we can build a decreasing Lyaponov function, 
but does not gives any automated method to compute it.  

In this work, we  have shown how convergence proof for any asynchronous
iterations of  discrete dynamical networks  with bounded delays
can be automatically achieved.
The key idea is to translate the network (map, strategy) into PROMELA and 
to leave the SPIN model checker establishing the validity 
of the temporal property corresponding to the convergence.
The correctness and completeness of the approach have been proved, notably 
by computing a SPIN execution of the PROMELA model that have the same
behaviors than initial network.
The complexity of the problem is addressed. It shows that non trivial example 
may be addressed by this technique.

Among drawbacks of the method,  one can argue that bounded delays is only 
realistic in practice for close systems. 
However, in real large scale distributed systems where bandwidth is weak, 
this restriction is too strong. In that case, one should only consider that 
matrix $S^{t}$ follows the  iterations of the system, \textit{i.e.},
for all $i$, $j$, $1 \le i \le j \le n$,  we have$
\lim\limits_{t \to \infty} S_{ij}^t = + \infty$. 
One challenge of this work should consist in weakening this constraint. 
We plan as future work to take into account other automatic approaches 
to discharge proofs notably by deductive analysis~\cite{CGK05}.