State space reduction based on live variables analysis

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 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.