\documentclass{elsart}

\usepackage{epsfig}
\usepackage{epic,eepic}
\usepackage{amssymb,amsmath}

\newcommand{\semrule}[2]{
  \medskip \hfill
  \mbox{${\displaystyle \frac{#1}{#2}}$}
  \hfill \medskip
}

\newcommand{\arrow}[1]     {{\stackrel{#1}{\longrightarrow}}}
\newcommand{\arrowi}[2]    {{\xrightarrow[#2]{#1}}}

\newcommand{\spa}           {\hspace{1cm}}

\newcommand{\vars}         {\mbox{\it vars}}
\newcommand{\Use}          {\mbox{\it Use}}
\renewcommand{\Def}        {\mbox{\it Def}}
\newcommand{\Live}         {\mbox{\it Live}}

\newcommand{\reset}        {\mbox{\it reset}}
\newcommand{\Reset}        {\mbox{\it Reset}}
\newcommand{\Post}         {\mbox{\it Post}}

\newcommand{\sdl}          {{\sc SDL}}
\newcommand{\uml}          {{\sc UML}}
\newcommand{\cadp}         {{\sc CADP}}
\newcommand{\spin}         {{\sc SPIN}}
\newcommand{\tgv}          {{\sc TGV}}
\newcommand{\aldebaran}    {{\sc Aldebaran}}
\newcommand{\objectgeode}  {Object{\sc geode}}
\newcommand{\IF}           {{\sc IF}}

%\setlength{\parskip}{3pt}

\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{example}{Example}

\newenvironment{proof}[0]
{\par{\it Proof:}}{\rule{0.15cm}{0.15cm}\bigskip}

\sloppy
\raggedbottom

\begin{document}

\begin{frontmatter}

\title{State Space Reduction based on \\ Live Variables Analysis}

\author{Jean-Claude Fernandez}
\address{LSR/IMAG, BP 82, F-38402 Saint Martin d'H\`eres\thanksref{email}}

\author{Marius Bozga}, \author{Lucian Ghirvu\thanksref{region}}
\address{Verimag, Centre Equation, 2 avenue de Vignate, F-38610 Gi\`eres\thanksref{email}}

\thanks[email]{E-mail: \{Marius.Bozga, Jean-Claude.Fernandez, Lucian.Ghirvu\}@imag.fr}
\thanks[region]{Work partially supported by R\'{e}gion Rh\^{o}ne-Alpes, France}

\begin{abstract}
The intrinsic complexity of most protocol specifications in particular, and of asynchronous systems in general, lead us to study combinations of static analysis with classical model-checking techniques as a way to enhance the performances of automated validation tools.  In this context, we found that a non-trivial equivalence over the model states can be derived from the information on {\em live variables}.  This equivalence exploits the unused dead values stored both in process variables and in communication queues and allows to reduce the model with a rather important factor.  Furthermore, this reduction comes almost for free and is always possible to directly generate the quotient model without generating the initial one.
\end{abstract}

\begin{keyword} 
model checking \sep state space reduction \sep bisimulation \sep 
asynchronous communication \sep live variables analysis
\end{keyword}

\end{frontmatter}



%
% Introduction
%

\section{Introduction} \label{sec-introduction}

The central problem arising in the context of model based validation, model-checking and test generation, is the well known {\em state explosion problem}.  In order to tackle it, one current direction of research focuses on adapting static analysis techniques such as the ones issued from compiler design and optimization~\cite{Aho-Sethi-Ullman-86,Muchnick-97} to this specific problem.  The idea is to prevent state explosion by tacking into account as most as possible of the {\em useful} information that can be computed statically on the program under verification.

Model-checking and test generation algorithms are based on the central notion of {\em bisimulation} equivalence~\cite{Milner-80}.  In practice, both of them benefit from model minimisation modulo {\em strong bisimulation}~\cite{Park-81}.  That is, strong equivalent models do not need to be distinguished and therefore, validation can always be done on the minimal model from one equivalence class while preserving all the validation results.  This fact motivates us to consider static analysis techniques in the context of bisimulation equivalences.  In this paper, we point out that a {\em non-trivial} equivalence can be derived from the information on {\em live variables}(in some given control point, a variable is live if its value could be used before being redefined on some path starting at that point).  This equivalence, further called {\em live bisimulation}, exploits the unused {\em dead} values stored both in variables and in communication queues.  It turns out that the live bisimulation is stronger than the strong bisimulation, but still allows to simplify the models with a rather important factor.

The reduction based on live bisimulation can be obtained with almost no additional cost: live variables need to be computed once in the beginning with an algorithm operating on the control graph of the program and then are used by specialized primitives (e.g, such as \Reset\ defined in section~\ref{sec-reset-equivalence}) which operate on model states and which have a linear complexity with respect to the size of the state (the number of variables plus the number of messages in the communication queues).  In fact, in the context of exhaustive state space exploration algorithms such primitives can be viewed as having constant operation time, similar to operations like state copying or state comparison.

Live bisimulation reduction is fully {\em orthogonal} to other techniques applied to deal with the state-explosion problem.  For instance, enumerative simulation is at the basis of most of the validation algorithms.  It is always possible to directly generate the quotient model with respect to live bisimulation, thus preserving all the relevant behaviours, without constructing the initial, complete model.  This can be easily done for instance by considering every time a new model state is encountered some canonical representative from its equivalence class.  In this way, equivalent states will be automatically identified as equals and explored once by the generation algorithm.

On-the-fly verification techniques such as~\cite{Fernandez-Jard-Jeron-92} rely on enumerative depth-first traversals of the model and the meantime evaluation of the property (e.g., temporal logic formula, observer automaton, test purpose).  In this case too, the property can be directly evaluated on the reduced model, if it is not explicitly dependent on variables or communication queue contents but only on the observable actions of the program.  Nevertheless, if such dependencies exist, they can be normally removed by introducing auxiliary observable actions and by modifying the property accordingly.  In addition, live bisimulation can be safely combined with partial order techniques~\cite{Godefroid-96} which reduce the model by avoiding to explore interleaving of independent actions.

In the symbolic model checking context~\cite{McMillan-93} the information on live variables can be used to simplify the BDDs representing the transition relation and the sets of states.  In fact, dead variables for a given control point provide non-trivial {\em don't care} conditions which can be exploited either directly to simplify any final or intermediate result, or even better, to improve primitives like successors or predecessor computation on symbolic representations.  In particular, live bisimulation reduction can also be applied at each step of the minimal model generation algorithm~\cite{Fernandez-Kerbrat-Mounier-93} which involves the (backward) computation of predecessor states.  This must be very important as the predecessor computation usually gives a lot of spurious unreachable states and which could be equivalent w.r.t. the live equivalence.

% related work

The idea of using static analysis to improve model checking was already investigated in different situations.  In particular, live variables are currently used by almost all model-checkers (such as \spin~\cite{Holzmann-91} or \cadp~\cite{Fernandez-Garavel-Kerbrat-96}) in order to simplify the models during exhaustive simulations.  Nevertheless, at the best of our knowledge, the current practice is limited to define some equivalence with respect to program variables, and none of them take into account the communication queue contents, when applicable.  Related work was done also by~\cite{Daws-Yovine-96} who propose a method to reduce the number of clocks in timed automata using live clocks and clocks equality analysis. Furthermore, in~\cite{Kurshan-Levin-98} was given a method which combines partial order reductions and static analysis of independent actions for \sdl\ programs.  Another interesting direction consists to find efficient representations of possible infinite queue contents and to exploit the static control structure when performing reachability analysis~\cite{Boigelot-Godefroid-96,Abdulla-Annichini-Bouajjani-98}.

% organisation

The paper is structured as follows.  Section~\ref{sec-model} presents the underlying model which is parallel processes asynchronous communicating via queues.  Section~\ref{sec-live-analysis} briefly remember the notion of live variables and some basic properties about them.  In section~\ref{sec-live-equivalence} we introduce the {\em live equivalence} relation on states and show that is a bisimulation.  An efficient way to identify live equivalent states using a canonical form is then presented in section~\ref{sec-reset-equivalence}.  Some practical results obtained on a small example are given in section~\ref{sec-example}.



%
% The model
%

\section{The model} \label{sec-model}

\subsection{Syntax}

We consider systems consisting of asynchronous parallel composition of a number of {\em processes} that communicate through {\em parameterised signal} passing via a set of unbounded {\em FIFO queues} and operate on a set of shared {\em variables}.  Formally, a system is a tuple: 

\spa \( P ~::=~ (S,X,C,\prod\limits_{i=1}^n p_i) \)

where $S$ is the set of signals, $X$ is the set of variables, $C$ is the set of queues and $\{p_i\}_{i=1,n}$ are processes.  Processes perform {\em actions} on queues and variables.  They are described by {\em terms} of a simplified value-passing process algebra with the following syntax:

\spa \( p ~::=~ nil ~|~ \alpha . p ~|~ p + p ~|~ Z(e) \)

This syntax contains the usual operators from process algebra: $nil$ denotes the empty process, $\alpha . p$ denotes $p$ prefixed with action $\alpha$, $p_1+p_2$ is the nondeterministic choice between $p_1$ and $p_2$, and finally $Z(e)$ stands for recursion with the value passing of the expression $e$.  To give semantics for terms we assume also the existence of a set of declarations: 

\spa \( Z(y) ~\triangleleft_{def}~ p \)

for each name $Z$ which occurs in terms.
%Note that in our algebra such declaration binds the occurrences 
%of the variable $y$ inside $p$ to $Z$
As usual, $y$ is a {\em parameter} of the definition of $Z$.  The actions are simple {\em guarded commands} defined by the following syntax:

\spa \( \alpha~  ~::=~  [~b~]~\alpha_1 \) 

\spa \( \alpha_1 ~::=~  x:=e ~|~ c!s(e) ~|~ c?s(x) \)

where $[~b~]$ with $b$ a boolean expression denotes the {\em guard},  $x:=e$ denotes an {\em assignment} of the variable $x$ to the expression $e$, $c!s(e)$ denotes the {\em output} to the queue $c$ of the signal $s$ with parameter the expression $e$ and finally, $c?s(x)$ denotes the {\em input} from the queue $c$ of the signal $s$ and store of its parameter in the variable $x$.

\begin{example}
Using the above syntax, a {\em counter} process which provides initialisation, consultation, increment and decrement primitives could be described as follows:

\spa \( \begin{array}{r c l} 
Z_{counter}(x) & ~\triangleleft_{def}~ & c?init(y).Z_{conter}(y) + \\
& & c!val(x).Z_{conter}(x) + \\
& & c!incr.Z_{counter}(x + 1) + \\
& & c!decr.Z_{counter}(x - 1) \end{array} \)
\end{example}


\subsection{Semantics}

We give the semantics of systems in terms of {\em labelled transition systems}.  We proceed in two steps: we start with the interpretation of the control part only, then we give the interpretation of control combined with data i.e, queue contents and variables.  

The control semantics is described by the following rules which give a way to build the {\em control graph} of the system, from the parallel composition of processes.  The states in this graph are tuples of terms $\prod\limits_{i=1}^n p_i$, and the transitions are labelled by actions, as follows:

\begin{center} \begin{tabular} {c c c}

\semrule{-}
        {\alpha.p \arrow{\alpha} p} &

\semrule{p \arrow{\alpha} p'}
        {p+q \arrow{\alpha} p'} & 

\semrule{q \arrow{\alpha} q'}
        {p+q \arrow{\alpha} q'} \\ 

\semrule{p[e/y] \arrow{\alpha} p' ~~ Z(y) \triangleleft_{def} p}
        {Z(e) \arrow{\alpha} p'} & &

\semrule{p_j \arrow{\alpha} p_j'  ~~~\forall i.~i\not=j~~p_i = p_i' ~}
        {\prod\limits_{i=1}^n p_i \arrow{\alpha} \prod\limits_{i=1}^n p_i'}

\end{tabular} \end{center}

In this paper we restrict our attention to systems where the control graph is finite i.e, they contain only a finite number of states and transitions.

In order to interpret the data part we assume the existence of the universal domain $D$ which contains the values of variables and signal parameters.  We suppose that the boolean values $\{true,false\}$ and also the special {\em undefined} $\bot$ value are contained in $D$.  We define {\em variable contexts} as being total mappings $\rho:X\rightarrow D$ which associate to each variable $x$ a value $v$ from the domain.  We extend these mappings to expressions in the usual way.  We define {\em queue contexts} as being also total mappings $\delta:C\rightarrow (S\times D)^*$ which associate to each queue $c$ a sequence $(s_1,v_1),...,(s_k,v_k)$ of {\em messages}, which are pairs $(s,v)$ noted also by $s(v)$, where $s$ is a signal and $v$ is the carried parameter value.  We assume also the existence of some special {\em unconsumable} message $\sigma$.  This notion will be used in section~\ref{sec-reset-equivalence} in order to undistinguish non-empty queues from which no signal could be consumed.  The empty sequence is noted with $\epsilon$.

The semantics of a system is now completed by the following rules which give a way to build a labelled transition system based on the control graph.  States of this system are triples of the form $(\rho,\delta,p)$, where $\rho$ is a variable context, $\delta$ is a queue context and $p$ is a control state.  Transitions are either {\em internal} and labelled with $\tau$, when derived from assignments or signal inputs, either {\em visible} and labelled with $c!s(v)$ when derived from signal outputs:

\begin{center} \begin{tabular} {c}

\semrule{p\arrow{[b]~x:=e}p' ~~ \rho(b) = true ~~ \rho(e) = v}
        { (\rho, \delta, p) \arrow{\tau} (\rho[v/x], \delta, p') } \\

\semrule{p\arrow{[b]~c!s(e)}p' ~~ \rho(b) = true ~~ \rho(e) = v ~~ \delta(c) = w}
        { (\rho, \delta, p) \arrow{c!s(v)} (\rho,\delta[w.s(v) / c], p')} \\

\semrule{p\arrow{[b]~c?s(x)}p' ~~ \rho(b) = true ~~ \delta(c) = s(v).w}
        { (\rho, \delta, p) \arrow{\tau} (\rho[v/x], \delta[w/c], p')} 

\end{tabular} \end{center}

\subsection{Notations}

Let us fix some set of queues $C_0\subseteq C$.

Given control states $p$, $p'$ we write $p\arrowi{}{C_0}p'$ if and only if $p'$ can be reached from $p$ in the control graph by a path which does not contain inputs from queues $c_0\in C_0$.  $\arrowi{}{C_0}$ is the reflexive and transitive closure of the transition relation including all the transition except those labelled with inputs from a queue of $C_0$.  We note with $\Post[\arrowi{}{C_0}]$ the post image function defined over sets of control states $Q$ by the relation above i.e, $\Post[\arrowi{}{C_0}](Q) = \{~ p' ~|~ \exists p.~p\in Q ~\wedge~ p\arrowi{}{C_0}p'~\}$.

Given action $\alpha$ and control states $p$, $p'$ we write $p\arrowi{\alpha}{C_0}p'$ if and only if it is possible to reach $p'$ from $p$ in the control graph by a path ending with $\alpha$ and which does not contain prior inputs from queues $c_0\in C_0$ i.e, there exists $p''$ such that $p\arrowi{}{C_0}p''$ and $p''\arrow{\alpha}p'$.

Finally, for queue $c\in C$ and signal $s\in S$ fixed, we define the post image function $\Post[\arrowi{c?s}{C_0}]$ over sets of control states $Q$ as follows $\Post[\arrowi{c?s}{C_0}](Q) = \{~ p' ~|~ \exists p~\exists b~\exists x.~p\in Q ~\wedge~ p\arrowi{[b]~c?s(x)}{C_0}p' \}$.  That is, it gives all the states which can be reached from $Q$ by paths containing no inputs from queues $c_0\in C_0$, and which end with the consumption of the signal $s$ from the queue $c$.  When $C_0$ is reduced to $\{c\}$, we use $p\arrowi{}{c}p'$ to stand for $p\arrowi{}{\{c\}}p'$.


%
% Live variables analysis
%

\section{Live variables analysis} \label{sec-live-analysis}

In this section we briefly remember the definition of live variables and some general properties about them.  We consider the sets of variables {\em used} and respectively {\em defined} by some action $\alpha$.  Intuitively, a variable is used either in the guards, in the right hand side of assignments or in outputs.  A variable is defined either in the left-hand side of assignments or in inputs.  Formally, the sets $\Use(\alpha)$ and $\Def(\alpha)$ are defined as follows:

\[ \begin{array} {c c c} 

\alpha & \Use(\alpha) & \Def(\alpha) \\ \hline

[~b~]~x:=e & \spa\vars(b) \cup \vars(e)\spa & \{x\} \\

[~b~]~c!s(e) & \vars(b) \cup \vars(e) & \emptyset \\

[~b~]~c?s(x) & \vars(b) & \{x\}

\end{array} \]

We consider now the set of {\em live} variables for some term $p$.  Intuitively it is the smallest set of variables that might be used before they are redefined when interpreting the term.  Formally, the sets $\Live(p)$ are defined as the least fixpoint solution of the following equation system over sets of variables (the subscript $\mu$ indicates that we are interested in the least solution, which exists since we consider only finite-control systems):

\[ \left\{ \spa \begin{array} {r c l} 

\Live(nil)         & =_{\mu} & \emptyset \\

\Live(\alpha . p)  & =_{\mu} & \Use(\alpha) \cup \Live(p) \setminus \Def(\alpha) \\

\Live(p + q)       & =_{\mu} & \Live(p) \cup \Live(q) \\

\Live(Z(e)) & =_{\mu} & \Live(p[e/x]) ~\mbox{where}~ Z(y) \triangleleft_{def} p \\

\Live(\prod\limits_{i=1}^n p_i) & =_{\mu} & \bigcup\limits_{i=1}^n \Live(p_i)

\end{array} \right. \]

An equivalent characterisation for the sets of live variables based on the control graph transitions and some basic properties are given by the following lemma.

\begin{lemma} \label{lemma-1} ~

{\it (i)} \( \Live(p) = \bigcup\limits_{p\arrow{\alpha}p'} \Use(\alpha) \cup \Live(p') \setminus \Def(\alpha) \).

{\it (ii)} \( p\arrow{\alpha}p' ~~\Rightarrow~~ \Use(\alpha) \subseteq \Live(p), ~\Live(p') \setminus \Def(\alpha) \subseteq \Live(p) \). 

\end{lemma}

\begin{proof} 
{\it (i)} Structural induction over term structure.  
{\it (ii)} Immediate from {\it (i)}.
\end{proof}

\begin{example}
If we consider the system described in figure~\ref{fig-first}, the variable $x$ is live in state $p_1$ and dead in state $p_2$, while the variable $y$ is dead in both of them.

\begin{figure}[htbp]
  \begin{center}
    \framebox{ \input{fig-first.eepic} }
    \caption{A first example.}
    \label{fig-first}
  \end{center}
\end{figure}
\end{example}

%
% Live equivalence
%

\section{Live equivalence} \label{sec-live-equivalence}

First, we consider the variable context equivalence relation induced by the set of live variables: two variable contexts are equivalent if and only if the values assigned to each one of the live variables are pairwise identical. Formally, for each state $p$ we define the {\em variable context equivalence} $\sim_p^{live}$ as follows:

\spa \( \rho_1 \sim^{live}_p \rho_2 
   ~~\Leftrightarrow~~ 
   \forall x\in\Live(p). ~\rho_1(x) = \rho_2(x)  \)

\begin{example}
If consider the system described in figure~\ref{fig-first} we have that contexts $[3/x,5/y]$ and $[2/x,7/y]$ are equivalent in state $p_2$, and not equivalent in state $p_1$ given that $x$ is live in this state.
\end{example}

We consider similar equivalence relations defined for queue contexts.  Intuitively two queue contexts are equivalent if and only if they enable the same paths of transitions and if for each executed input the parameter values are identical if the receiving variable is live at the next state.  Formally, we define the {\em queue context equivalences} $\approx_p^{live}$ to be the greatest fixpoint solution of the following equation system where for each state $p$ we have (the subscript $\nu$ indicates that we are interested in the greatest solution):

\( \delta_1 \approx_p \delta_2
   ~\Leftrightarrow_{{\nu}} ~
   \left\{ \begin{array} {l}
   \bigwedge\limits_{p\arrow{[b]~x:=e}p'} \delta_1 \approx_{p'} \delta_2 ~\wedge \\ 
   \bigwedge\limits_{p\arrow{[b]~c!s(e)}p'} \delta_1 \approx_{p'} \delta_2 ~\wedge \\
   \bigwedge\limits_{p\arrow{[b]~c?s(x)}p'} 
      \left\{ \begin{array} {l}
      \delta_1(c) = \epsilon ~\wedge~ \delta_2(c) = \epsilon ~\wedge~ 
      \delta_1 \approx_{p'} \delta_2 \\
      \vee \\
      \delta_1(c) = s(v_1).w_1 ~\wedge~ \delta_2(c) = s(v_2).w_2 ~\wedge~  \\
      ~~ ( x\in\Live(p') \Rightarrow v_1 = v_2 ) ~\wedge~ 
      \delta_1[w_1/c] \approx_{p'} \delta_2[w_2/c] \\
      \vee \\
      \delta_1(c) = s_1(v_1).w_1 ~\wedge~ \delta_2(c) = s_2(v_2).w_2 ~\wedge~ \\
      ~~ s_1 \not= s ~\wedge~ s_2 \not= s  
      \end{array} \right.
   \end{array} \right.
\)

If the control graph is finite, the existence of the greatest fixpoint satisfying the equations above is ensured by the Tarski's fixpoint theorem given the monotonicity with respect to the relation inclusion at each state.

\begin{example}
To illustrate the definition above, consider again the example from figure~\ref{fig-first}.  For instance, we have that queue contexts $[s_1(2).s_2(3)/c_1, s_1(4)/c_2]$ and $[s_1(2).s_2(5)/c_1, s_1(4)/c_2]$, or $[s_1(3)/c_1, \epsilon/c_2]$ and $[s_1(3)/c_1, s_1(3)/c_2]$ are live equivalent in both states $p_1$ and $p_2$.  Conversely, queue contexts $[s_2(1).s_1(2)/c_1,\epsilon/c_2]$ and $[s_1(2)/c_1,\epsilon/c_2]$ are not live equivalent neither in $p_1$ or $p_2$.
\end{example}

Some interesting properties of the live equivalence on queue contexts are given by the following lemmas.

\begin{lemma} \label{lemma-2}
\( \delta_1\approx_p^{live}\delta_2 ~\Leftrightarrow~\)

\spa \(\forall p'.~p\arrowi{[b]~c?s(x)}{C}p' ~\Rightarrow~ 
      \left\{ \begin{array} {l}
      \delta_1(c) = \epsilon ~\wedge~ \delta_2(c) = \epsilon ~\wedge~ 
      \delta_1 \approx_{p'} \delta_2 \\
      \vee \\
      \delta_1(c) = s(v_1).w_1 ~\wedge~ \delta_2(c) = s(v_2).w_2 ~\wedge~  \\
      ~~ ( x\in\Live(p') \Rightarrow v_1 = v_2 ) ~\wedge~ 
      \delta_1[w_1/c] \approx_{p'} \delta_2[w_2/c] \\
      \vee \\
      \delta_1(c) = s_1(v_1).w_1 ~\wedge~ \delta_2(c) = s_2(v_2).w_2 ~\wedge~ \\
      ~~ s_1 \not= s ~\wedge~ s_2 \not= s  
      \end{array} \right. \)
\end{lemma}
\begin{proof} The proof is immediate from the definition of the live equivalence.
\end{proof}

Furthermore, it can be proven inductively that, two equivalent queue contents at some state $p$, are still equivalent after adding the same message to the same queue in both of them.

\begin{lemma} \label{lemma-3} ~

\( \delta_1\approx_p^{live}\delta_2,~ \delta_1(c)=w_1,~ \delta_2(c)=w_2 ~\Rightarrow \)

\spa \( \forall s~\forall v.~~ \delta_1[w_1.s(v)/c]\approx_p^{live}\delta_2[w_2.s(v)/c]\).
\end{lemma}
\begin{proof}
%---- The proof can be done by induction on the size of queue contexts.
Because $\delta_1\approx_p^{live}\delta_2$ the queue contexts $\delta_1$ and $\delta_2$ should satisfy the $\wedge$ clauses in the lemma \ref{lemma-2}~:

{\it 1}:
If $w_1 = \epsilon$ and $w_2 = \epsilon$ then the contexts $w_1.s(v) = w_2.s(v) = s(v)$ will fulfill the conditions of the second $\wedge$ clause so $\delta_1[w_1.s(v)/c]\approx_p^{live}\delta_2[w_2.s(v)/c]$.

{\it 2}:
If $w_1$ and $w_2$ satisfy both the second or the third $\wedge$ clause then adding them $s(v)$ does not change the fact they fulfill the second or the third $\wedge$ clause so $\delta_1[w_1.s(v)/c]\approx_p^{live}\delta_2[w_2.s(v)/c]$.
\end{proof}

In general, the property above does not hold for input actions: two equivalent queue contents do not remain necessary equivalent when taking away the same message in the same queue from both of them.

\begin{example}
Consider the system $p_1~\arrow{c_1?s_1(x)}~p_2~\arrow{c_2!s_2(x)}~p_3$.
The queue context \([s_1(2) .   s_1(3)/c_1,\epsilon/c_2]\) and \([s_1(2)/c_1,\epsilon/c_2]\) are equivalent in $p_1$, but if we remove $s_1(2)$ then the resulting queue contexts are not equivalent in $p_1$.
\end{example}
We define now the {\em live equivalence} $\approx^{live}$ relation over global states: two states are equivalent if the control states are identical and both the variable context and the queue context are equivalent:

\spa \( (\rho_1,\delta_1,p) \approx^{live} (\rho_2,\delta_2,p) 
   ~~\Leftrightarrow~~ 
\rho_1 \sim^{live}_p \rho_2 ~~\wedge~~ \delta_1 \approx^{live}_p \delta_2 \)

The next theorem gives the central result of the paper: the live equivalence is also a bisimulation relation over the global states.  By definition, for all pairs $(\rho_1,\delta_1,p) \approx^{live} (\rho_2,\delta_2,p)$ we have:

\( \forall a~\forall(\rho_1',\delta_1',p').~(\rho_1,\delta_1,p)\arrow{a}(\rho_1',\delta_1',p') \Rightarrow \)

\spa \( \exists(\rho_2',\delta_2',p').~(\rho_2,\delta_2,p)\arrow{a}(\rho_2',\delta_2',p') \wedge 
   (\rho_1',\delta_1',p')\approx^{live}(\rho_2',\delta_2',p') \)

\( \forall a~\forall(\rho_2',\delta_2',p').~(\rho_2,\delta_2,p)\arrow{a}(\rho_2',\delta_2',p') \Rightarrow \)

\spa \( \exists(\rho_1',\delta_1',p').~(\rho_1,\delta_1,p)\arrow{a}(\rho_1',\delta_1',p') \wedge 
   (\rho_1',\delta_1',p')\approx^{live}(\rho_2',\delta_2',p') \)

%%%

\begin{theorem}

The live equivalence $\approx^{live}$ is a bisimulation.

\end{theorem}

\begin{proof} 

Let $(\rho_1,\delta_1,p) \approx^{live} (\rho_2,\delta_2,p)$ and let $p\arrow{\alpha} p'$. We distinguish three different cases, depending on the type of $\alpha$.

{\it (1)}  $\alpha = [~b~]~x:=e$

From $\rho_1 \sim^{live}_p \rho_2$, we deduce that
$\rho_1(b)=\rho_2(b)$ and $~ \rho_1(e)=\rho_2(e)=v$.
Suppose that
%\( \forall i=1,2.~~\rho_i(e)=v_i,~\rho_i(b)=true ~\Rightarrow \)
\(\rho_1(b)=\rho_2(b)=true \).
Thus, for each $i=1,2$ we have 
\( (\rho_i,\delta_i,p) \arrow{\tau} (\rho_i',\delta_i,p')\) where \(\rho_i' = \rho_i[v/x] \).
We have to show that 
%\(\rho_1 \sim^{live}_p \rho_2 ~\Rightarrow~ \rho_1(b)=\rho_2(b),~ \rho_1(e)=\rho_2(e),~ \rho_1[v_1/x] \sim^{live}_{p'} \rho_2[v_2/x] \)
\( \rho_1[v/x] \sim^{live}_{p'} \rho_2[v/x] \) and
\( \delta_1 \approx^{live}_{p'} \delta_2 \)
%\( \delta_1 \approx_{p}^{live} \delta_2 ~\Rightarrow~ \delta_1 \approx^{live}_{p'} \delta_2 \)

From lemma~\ref{lemma-1}, if $y \in \Live(p')$ and $y\neq x$ then
$y \in \Live(p)$. Because $\rho_1(y)=\rho_2(y)$ 
we have that $\rho'_1(y)=\rho'_2(y)$.
Also, we have that $\rho'_1(x)=\rho'_2(x)=v$.
In conclusion, $\forall z \in \Live(p')$, $\rho'_1(z)=\rho'_2(z)$ and
thus \( \rho'_1 \sim^{live}_{p'} \rho'_2 \).
Finally, by definition of live equivalence on 
queue contexts, we have \( \delta_1 \approx^{live}_{p'} \delta_2 \).  

{\it (2)} $\alpha = [~b~]~c!s(e)$

Let us assume that, for each $i=1,2$ we have 
$\delta_i(c)=w_i$, $\rho_i(e)=v_i$, 
$\rho_i(b)=true$.  As before, we have that
\( (\rho_i,\delta_i,p) \arrow{c!s(v_i)} (\rho_i,\delta_i',p') \) 
where \( \delta_i' = \delta_i[w_i.s(v_i)/c] \).

Because
\( \rho_1 \sim^{live}_p \rho_2 \) we deduce respectively 
\( \rho_1(b) = \rho_2(b)\), \(\rho_1(e)=\rho_2(e)\) and 
\(\rho_1 \sim^{live}_{p'} \rho_2 \). 
Furthermore, 
from definition of $\approx_{p}^{live}$,
\( \delta_1 \approx_{p}^{live} \delta_2\) implies 
\(\delta_1 \approx^{live}_{p'} \delta_2\).
Now, given that live equivalence is closed under output operations
(see lemma~\ref{lemma-3}) it results 
\( \delta_1[w_1.s(v_1)/c] \approx^{live}_{p'} \delta_2[w_2.s(v_2)/c] \).

%Note that the last implication comes from the more general property 
%of queue content equivalence to be {\em closed} under output operations.

{\it (3)} $\alpha = [~b~]~c?s(x)$

Again, let us consider that for each $i=1,2$ we have 
\(~\delta_i(c)=s(v_i).w_i\) and \( \rho_i(b)=true \).  Then, 
\( (\rho_i,\delta_i,p) \arrow{\tau} (\rho_i',\delta_i',p') \) where
\( \rho_i' = \rho_i[v_i/x]\) and \( \delta_i' = \delta_i[w_i/c] \) 

As before, because \( \rho_1 \sim^{live}_p \rho_2 \) 
we have that \( \rho_1(b) = \rho_2(b) \) and 
\(~\rho_1[v_1/x] \sim^{live}_{p'} \rho_2[v_2/x] \).  By definition 
\( \delta_1 \approx^{live}_p \delta_2 \) implies \( v_1=v_2 \) if 
\(x\in\Live(p')\) and 
\( \delta_1[w_1/c] \approx^{live}_{p'} \delta_2[w_2/c] \).
\end{proof}

An immediate consequence of the previous theorem is the following one, stating that the live equivalence is stronger than the strong bisimulation.  Clearly, we do not have equality because strong bisimulation might identify global states as bisimilar even if they have distinct control states.

\begin{theorem}

\( \approx^{live} ~\subseteq~ \approx^{strong} \).

\end{theorem}



%
% Reset equivalence
%

\section{Reset equivalence} \label{sec-reset-equivalence}

We would like to have a more efficient way to check that two contexts are live equivalent than to directly check the definition.  Here we investigate the possibility to transform contexts into some {\em canonical form} preserving the live equivalence.  One way to do this is using the family of \Reset\ functions, defined below.

The \Reset$^v$ function on variable contexts $\rho$ basically sets the value of the dead variables to the fixed {\em undefined} $\bot$ value, depending on the current control state $p$.  A {\em reset equivalence} can be defined over variable contexts as follows: two contexts are reset equivalent if they give the same result when reset.  Formally, we have:


\spa \( \Reset^v(p, \rho) = \rho^* \spa\rho^*(x) = \left\{ \begin{array} {l l}  

\rho(x) & \mbox{if}~~x\in\Live(p) \\ 

\bot & \mbox{otherwise} 

\end{array} \right. \)

\spa \( \rho_1\sim^{reset}_p\rho_2 ~~\Leftrightarrow~~ \Reset^v(p,\rho_1)=\Reset^v(p,\rho_2) \)

It is straightforward to prove that the live equivalence and 
the reset equivalence on variable contexts are identical,  
i.e, the following lemma holds.

\begin{lemma} \label{lemma-4} 

\( \forall p. ~ \sim^{reset}_p ~=~ \sim^{live}_p \).

\end{lemma}

In order to define a similar \Reset$^q$ function for queue contexts we start by introducing some auxiliary definitions.  We define the local \reset\ function for the queue $c$ given an initial non-empty set of control states $Q$.  Given the content $w$ of the queue $c$, this function basically rewrites it and {\em forgets} the signal parameters which are detected statically to be unused, when execution starts somewhere in $Q$.  With $\sigma$ denoting the {\em unconsumable} message, the function is recursively defined as follows:

\spa \( \begin{array} {r c l} 

\reset(Q,c,\epsilon) & = & \left\{ \begin{array} {l}

    \sigma ~~~ \mbox{if} ~~ \forall s~~ \Post[\arrowi{c?s}{c}](Q) = \emptyset \\ \\

    \epsilon ~~~ \mbox{otherwise}

    \end{array} \right. \\ \\

\reset(Q,c,s(v).w) & = & \left\{ \begin{array} {l} 

    \sigma ~~~ \mbox{if} ~~ \Post[\arrowi{c?s}{c}](Q) = \emptyset \\ \\

    s(v).\reset(\Post[\arrowi{c?s}{c}](Q),c,w) \\ 
    \spa~ \mbox{if} ~~ \exists p\in Q.~p\arrowi{[b]~c?s(x)}{c}p' ~\wedge~ x \in\Live(p') \\ \\

    s(\bot).\reset(\Post[\arrowi{c?s}{c}](Q),c,w) \\
    \spa~ \mbox{if} ~~ \forall p\in Q.~p\arrowi{[b]~c?s(x)}{c}p' ~\Rightarrow~ x \not\in\Live(p') 

    \end{array} \right.

\end{array} \)

Some interesting properties about the local \reset\ function are given by the following lemma.

\begin{lemma} \label{lemma-5} For any $Q$, $Q_1$, $Q_2$, $c$, $w$, $w_1$, $w_2$ the following statements hold~:

{\it (i)} \( \reset(Q,c,w) = \reset(\Post[\arrowi{}{c}](Q),c,w) \).

{\it (ii)} \( \reset(Q,c,w_1) = \reset(Q,c,w_2) ~\Rightarrow~ \)

\spa \( \forall Q'\subseteq Q~~\reset(Q',c,w_1)=\reset(Q',c,w_2) \).

{\it (iii)} \( \reset(Q_1,c,w_1)=\reset(Q_1,c,w_2), \reset(Q_2,c,w_1)=\reset(Q_2,c,w_2) ~\Rightarrow \) 

\spa \( \reset(Q_1\cup Q_2,c,w_1) = \reset(Q_1\cup Q_2, c, w_2) \)

\end{lemma}

\begin{proof} 
{\it (i)} The proof is immediate from the fact that for any set of control 
states $Q$, channel $c$ and signal $s$ we have
\( Q\subseteq \Post[\arrowi{}{c}](Q) \) and 
\( \Post[\arrowi{c?s}{c}](Q) = \Post[\arrowi{c?s}{c}](\Post[\arrowi{}{c}](Q)) \).
{\it (ii), (iii)} The proof can be done by induction on the maximal size of the 
sequences $w_1$ and $w_2$.
\end{proof}

We define the \Reset$^q$ function and the {\em reset equivalence} on queue contexts 
using local \reset\ functions defined before.  For a given control state $p$
we consider:

\spa \( \Reset^q(p,\delta) = \delta^* \spa\delta^*(c) = \reset(\{p\}, c, \delta(c)) \)

\spa \( \delta_1 \approx^{reset}_p \delta_2 ~~\Leftrightarrow~~ \Reset^q(p,\delta_1) = \Reset^q(p,\delta_2) \)

\begin{example}
For the example given in figure~\ref{fig-first} we can check that
queue contexts $\delta_1=[s_1(2).s_2(3)/c_1, s_1(4)/c_2]$ 
and $\delta_2=[s_1(2).s_2(5)/c_1, s_1(4)/c_2]$, which are live equivalent, 
are also reset equivalent in both states $p_1$ and $p_2$.
We have for both $i=1,2$ that 
$\Reset^q(p_i,\delta_1)=\Reset^q(p_i,\delta_2)=[s_1(2).s_2(\bot), \sigma]$.
\end{example}

The following lemma gives the relation between the live equivalence and the reset equivalence on queue contexts.  In general, the reset equivalence is stronger than the live equivalence.  This is explained by the fact that local resets are based on a conservative assumption about other queues: {\em the inputs from other queues are always considered enabled}.  However, in the special case when the input actions from a queue do not enable input actions from other queues, the live equivalence and the reset equivalence become identical.

Recall that $C$ is the set of all queues defined in the system 
(see section~\ref{sec-model}).
We define queue $c$ to be {\em reset-independent} from queue 
$c'$ if and only if~:

\spa \( \forall p~\forall q~\forall q'.~~ p\arrowi{[b'] c'?s'(x')}{C} q,~ q\arrowi{[b] c?s(x)}{C} q' ~\Rightarrow \)

\spa \spa \( \exists p'.~~ p\arrowi{[b] c?s(x)}{C} p',~ p'\arrowi{[b'] c'?s'(x')}{C} q',~ x\in\Live(p') \Leftrightarrow x\in Live(q') \)

~

\begin{figure}[htbp]
  \begin{center}
    \framebox{ \input{fig-independence.eepic} }
    \label{fig-independence}
    \caption{Reset-independent queues.} 
  \end{center}
\end{figure}

\begin{lemma} \label{lemma-6}~

{\it (i)} \( \forall p. ~~ \approx^{reset}_p ~\subseteq~ \approx^{live}_p \).

{\it (ii)} if the queues are reset-independent then 
\( \forall p. ~~ \approx^{reset}_p ~=~ \approx^{live}_p \).

\end{lemma}

\begin{proof} 
{\it (i)} The proof consists of checking that the reset equivalences 
$\approx^{reset}_p$ satisfies the fixpoint equations 
defining the live equivalence.  This can be easily done given 
the results established by lemma~\ref{lemma-5}.  
Then because the live equivalences are the greatest fixpoint it is 
clear that $\approx^{reset}_p \subseteq \approx^{live}_p$ for 
all control states $p$.
{\it (ii)} The proof is done by induction on the maximal size 
of queue contexts.  The initial step is straightforward: empty
queue contexts are both live and reset equivalent.  The induction
step is proven by contradiction.  Let consider 
$\delta_1\approx^{live}_p\delta_2$, some queue $c$ fixed and
let assume that $\reset(\{p\},c,\delta_1(c))\not=\reset(\{p\},c,\delta_2(c))$.
We distinguish the following cases:

{\it (1)} \( \delta_1(c)=\epsilon, ~\delta_2(c)=\epsilon ~\Rightarrow~
\reset(\{p\},c,\delta_1(c)) = \reset(\{p\},c,\delta_2(c)) \)
which is a contradiction with the reset hypothesis.

{\it (2)} \( \delta_1(c)=\epsilon, ~\delta_2(c)=s_2(v_2).w_2 \)

{\it (2.1)} \( \forall s.~~ \Post[\arrowi{c?s}{c}](\{p\})=\emptyset ~\Rightarrow~ 
\reset(\{p\},c,\delta_1(c)) = \reset(\{p\},c,\delta_2(c)) = \sigma \)  
which is a contradiction with the reset hypothesis.

{\it (2.2)} \( \exists s.~~ \Post[\arrowi{c?s}{c}](\{p\})\not=\emptyset ~\Rightarrow 
~~ \Post[\arrowi{c?s}{C}](\{p\}) \not=\emptyset \)
  
Because the queues are reset-independent we can choose the path ending with an 
input of the form $c?s$ such that it does not contain inputs from other queues.
But, in such case we have a contradiction with the live equivalence hypothesis 
\( \delta_1\approx^{live}_p\delta_2 \).

{\it (3)} \( \delta_1(c)=s_1(v_1).w_1, ~\delta_2(c)=s_2(v_2).w_2 \)

{\it (3.1)} \( \Post[\arrowi{c?s_1}{c}](\{p\}) = \emptyset, ~\Post[\arrowi{c?s_2}{c}](\{p\}) = \emptyset ~\Rightarrow \) 
 \( \reset(\{p\},c,\delta_1(c)) = \reset(\{p\},c,\delta_2(c)) = \sigma \)
which is a contradiction with the reset hypothesis.

{\it (3.2)} \( \Post[\arrowi{c?s_1}{c}](\{p\}) \not= \emptyset, ~\Post[\arrowi{c?s_2}{c}](\{p\}) = \emptyset \) leads to a contradiction with the live equivalence hypothesis, as in the case {\it (2.2)}.

{\it (3.3)} \( \Post[\arrowi{c?s_1}{c}](\{p\}) \not= \emptyset, ~\Post[\arrowi{c?s_2}{c}](\{p\}) \not= \emptyset \)

{\it (3.3.1)} \( s_1 \not= s_2 \) leads to a contradiction with the live equivalence 
hypothesis, as before.

{\it (3.3.2)} \( s_1 = s_2 = s\) and \( v_1 \not= v_2 \) and \( \exists p\arrowi{[b]~c?s(x)}{c}p'~~x\in \Live(p') \) 
leads to a contradiction with the live equivalence hypothesis, as before.

{\it (3.3.3)} \( s_1 = s_2 = s\) and \( v_1 = v_2 = v \) or \( \forall p\arrowi{[b]~c?s(x)}{c}p'~~x\not\in \Live(p') ~\Rightarrow \)

\spa \( \reset(\{p\},c,s_1(v_1).w_1) = s(v).\reset(\Post[\arrowi{c?s}{c}](\{p\}),c,w_1) \) and

\spa \( \reset(\{p\},c,s_2(v_2).w_2) = s(v).\reset(\Post[\arrowi{c?s}{c}](\{p\}),c,w_2) \)

From the reset hypothesis we must have that \( \reset(\Post[\arrowi{c?s}{c}](\{p\}),c,w_1)
\not=\reset(\Post[\arrowi{c?s}{c}](\{p\}),c,w_2) \).  Moreover, from lemma~\ref{lemma-5} we can 
infer that there exists  $p'\in \Post[\arrowi{c?s}{c}](\{p\})$ such that 
\( \reset(\{p'\},c,w_1) \not= \reset(\{p'\},c,w_2) \).

So, there exists a path starting in $p$ and ending in $p'$ 
by an input of the form $c?s$ and which does not contain any prior input from the 
queue $c$ (see figure below).  
Now, given the reset-independence hypothesis we can find another 
path from $p$ leading to $p'$, containing exactly the same inputs, reordered such that 
the one of form $c?s$ is the now the first in the path.  Let $p''$ be the state
after executing the $c?s$ input in this new path.  

\begin{figure}[htbp]
  \begin{center}
    \framebox{ \input{fig-proof.eepic} }
    \label{fig-proof}
  \end{center}
\end{figure}

In state $p''$, given the live hypothesis we have 
\( \delta_1[w_1/c]\approx_{p''}^{live}\delta_2[w_2/c] \).  
Also, from \( \reset(\{p'\},c,w_1) \not= \reset(\{p'\},c,w_2) \) and 
because there is a path from $p''$ to $p'$ which does not contain inputs from the 
queue $c$ we have also that \( \reset(\{p''\},c,w_1)\not=\reset(\{p''\},c,w_2) \) 
(see also lemma\ref{lemma-5}).  So we end up with the 
induction hypotheses at state $p''$, now for contexts smaller 
with one message.  The proof is complete. 
\end{proof}

\begin{example}
Let consider the example given in figure~\ref{fig-second}.
Following the definition, queues $c_1$ and $c_2$ are not 
reset-independent.  Thus, there exist queue contents such as
$\delta_1=[s_2(1)/c_1,s_2(2)/c_2]$ and 
$\delta_2=[s_2(3)/c_1,s_2(7)/c_2]$ which are live 
equivalent in state $p_1$ but not reset equivalent at that state.  
That is, $\Reset^q(p_1,\delta_1)=[\sigma/c_1,s_2(2).\sigma/c_2]\not=
[\sigma/c_1,s_2(7).\sigma/c_2]=\Reset^q(p_1,\delta_2)$.

\begin{figure}[htbp]
 \begin{center}
  \framebox{ \input{fig-second.eepic} }
  \caption{A second example}
  \label{fig-second}
 \end{center}
\end{figure}

\end{example}

Finally, we define the {\em reset equivalence} over global states as follows:

\spa \( (\rho_1,\delta_1,p) \approx^{reset} (\rho_2,\delta_2,p) 
   ~~\Leftrightarrow~~ 
  \rho_1 \sim^{reset}_p \rho_2 ~~\wedge~~ \delta_1 \approx^{reset}_p \delta_2 \)

The link between the live and reset equivalence over global states is
established by the following theorem.

\begin{theorem}~

{\it (i)} \(\approx^{reset} ~\subseteq~ \approx^{live} \)

{\it (ii)} if the queues are reset-independent then 
\( \approx^{reset} ~=~ \approx^{live} \)

\end{theorem}

Finally, note that \sdl\ systems satisfy the independence hypothesis, as they are composed from parallel processes, each one having its own unique input queue.  Thus, performing signal input in a process does not interfere with other possible inputs in other processes.






%
% Example
%

\section{Example} \label{sec-example}

We illustrate the potential reduction obtained using the live equivalence on a small example.  We consider two simple processes communicating through a queue as shown in figure~\ref{fig-example}.  The first process only send arbitrarily $request$ and $switch$ messages.  It is described by $Z_{dummy}$ and the following equation:


\spa \( \begin{array} {r c l}

Z_{dummy} & \triangleleft_{def} & (in!switch + in!request(*)).Z_{dummy}

\end{array} \)

The second process is more interesting.  It has two functioning modes, a $normal$ one and a $fault$ one.  Basically, it inputs $requests$ from the $in$ queue and delivers them, when normal, and loses them otherwise.  The mode changes from $normal$ to $fault$ (and backward) when the input is a $switch$ signal.  Formally, we consider this process described by $Z_{normal}$ and the following equations:


\spa \( \begin{array} {r c l}

Z_{normal}(y) & \triangleleft_{def} & in?request(x).Z_{deliver}(x) + in?switch.Z_{fault}(y) \\ 

Z_{deliver}(x) & \triangleleft_{def} & out!request(x).Z_{normal}(x) \\ 

Z_{fault}(y) & \triangleleft_{def} & in?request(x).Z_{fault}(x) + in?switch.Z_{normal}(y)

\end{array} \)


\begin{figure}

\begin{center}

\epsfig{figure=fig-example.eps,width=0.8\linewidth}

\end{center}

\caption{The client/server example.}

\label{fig-example}

\end{figure}

We can easily check that the variable $x$ is live only at the $deliver$ state.  Thus, the value of $x$ must not be used to distinguish between states when somewhere else than the state $deliver$.  Furthermore, it can be seen that when at the $fault$ state, the parameters of the incoming $requests$ are not {\em live} too.  $request$ signals are only consumed, without using the carried values.  It can be seen also that signals of the $out$ queue are never consumed so we don't distinguish states which differs on the $out$ content.  Such cases are all captured by the live equivalence as defined in section~\ref{sec-live-equivalence}.

Figure~\ref{fig-reduction} shows the reduction obtained for this example with respect to two parameters: $m$, the size of the domain of $x$ and $n$, the maximal allowed size of queue $in$.  The continuous lines give the real number of states and the dotted lines give the number of states obtained after considering live equivalence reduction and please notice that a logarithmic scale was used for the {\em number-of-states} axis.  Also, to better illustrate the reduction obtained, when $m=6$ and $n=5$ the initial number of states is $352944$ and it is reduced at $89824$, so with a factor up to $75$\%.  Furthermore, this reduction depends on both variables and queue contents equivalences.  For example, when each one is applied in isolation the number of states generated is respectively $156864$ when considering only the variable context equivalence, and $164304$ when consider only the queue context equivalence.

\begin{figure}

   \begin{tabular} {c c}

   \epsfig{figure=3n.ps,width=5.5cm} & \epsfig{figure=m3.ps,width=5.5cm}

   \end{tabular}

   \caption{Live equivalence reduction}

   \label{fig-reduction}

\end{figure}



%
% Conclusions
%

\section{Conclusion and future work} \label{sec-conclusion}

In the context of model-based validation, the main interest of static analysis is to reduce the state space, which is crucial in practice to deal with complex specifications.  Model checking and automatic test generation for conformance testing are based on the same algorithmic techniques: given a specification and a property, they compute, in the first case the validity of the property and, in the second case, the test case with respect to either the specification and the property.

The essence of this work is to show that using the live variable analysis ones can define a {\em live bisimulation} equivalence stronger than the strong bisimulation. The live bisimulation allows to simplify the models exploiting unused dead values stored both in process variables and in communication queues.  This idea was already experimented for the industrial case studies SSCOP~\cite{Bozga-Fernandez-Ghirvu-98a} where we have obtained impressive reductions of the state space up to 200 times and MASCARA~\cite{Jia-Graf-00} where the reductions not only have been important~(by 96\%), but the live variables analysis was also essential in order to generate the model. 

We are currently developing \IF~\cite{Bozga-Fernandez-Ghirvu-99c}, a toolbox for a high level representation of asynchronous systems, especially for real-time specification languages such as \sdl\ and \uml.  In this toolbox, static analysis is intensively used in the earlier stages of validation in order to reduce the memory costs of the next ones.  This lead us to consider two classes of analysis: {\em property independent} analysis: (such as live variable analysis or constant propagation) without regarding any particular property, the analysis is implemented by a module which takes as input and output a intermediate program, {\em property dependent} analysis: the analysis takes into account some information extracted from the property or from the environment and propagate them over the static control structure of the program (such as {\em uncontrollable variables} abstraction~\cite{Colby-Godefroid-Jagadeesan-98} or the {\em slicing}~\cite{Weiser-84} in the context of test case generation~\cite{Bozga-Fernandez-Ghirvu-00a}).  We envisage to experiment more sophisticated analysis, such as general constraint propagation. We also want to exploit a connection with the tool {\sc InVeSt}~\cite{Bensalem-Lakhnech-Owre-98}, which computes abstractions and invariants on communicating processes.

\bibliographystyle{elsart-num}
\bibliography{biblio}

\end{document}

