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.
The goal of this paper is to point out that an equivalence on our model derived from the information on live variables is
stronger than the strong bisimulation. This equivalence, further called live bisimulation, exploits the unused dead values
stored either in variables or in queue contents and allow to simplify the state space 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.
Keywords model checking - state space reduction - bisimulation - asynchronous communication - live variables analysis
This work was partially supported by Région Rhône Alpes
VERIMAG is a joint laboratory of CNRS, UJF and INPG Grenoble